← Copula mathematical handbook

Exhaustion of all xi levels by the constructed Blest family

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_coefficients_monotone {b d : ℝ} (hb : 0 ≤ b) (hd : 0 ≤ d) (hbd : b ≤ d) : (extremalCopula b hb).chatterjeeXi ≤ (extremalCopula d hd).chatterjeeXi ∧ blestNu (extremalCopula b hb) ≤ blestNu (extremalCopula d hd)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_xi_continuous : Continuous fun (b : ↑(Set.Ici 0)) => (extremalCopula ↑b ⋯).chatterjeeXi

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.extremalSequence (n : ℕ) : Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.extremalSequence n = ProbabilityTheory.Copula.RankRegion.XiBlest.extremalCopula ((↑n + 1) ^ 2) ⋯

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremalSequence_cdf (u v : ↑unitInterval) : Filter.Tendsto (fun (n : ℕ) => (extremalSequence n).cdf ![u, v]) Filter.atTop (nhds ((comonotonic 2).cdf ![u, v]))

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremalSequence_xi : Filter.Tendsto (fun (n : ℕ) => (extremalSequence n).chatterjeeXi) Filter.atTop (nhds 1)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremalSequence_blest : Filter.Tendsto (fun (n : ℕ) => blestNu (extremalSequence n)) Filter.atTop (nhds 1)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.extremal_parameter_exists (x : ℝ) (hx : x ∈ Set.Ioo 0 1) : ∃ (b : ℝ) (hb : 0 < b), (extremalCopula b ⋯).chatterjeeXi = x

Every nontrivial xi below one has an actual member of the extremal family.