Continuous coefficient paths along copula mixtures #
The quadratic identities make continuity explicit without imposing a density or continuity assumption on the conditional distributions of a copula.
theorem
ProbabilityTheory.Copula.RankRegion.XiBeta.continuous_xi_mix
(C D : Copula 2)
:
Continuous fun (a : ↑unitInterval) => (C.mix D a).chatterjeeXi
theorem
ProbabilityTheory.Copula.RankRegion.XiBeta.exists_unitInterval_eq
{f : ↑unitInterval → ℝ}
(hf : Continuous f)
{z : ℝ}
(hz0 : f 0 ≤ z)
(hz1 : z ≤ f 1)
:
∃ (a : ↑unitInterval), f a = z
A continuous real-valued function on the closed unit interval attains every value between its endpoint values.