← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow_independence {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (i : Fin m) (v : ↑unitInterval) : patchworkRow A (fun (x : Fin m) (x_1 : Fin n) => independence 2) i v =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => checkerboardRow A i v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboard_conditional_energy {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), A.checkerboard.conditionalCDF u v ^ 2 = ∑ i : Fin m, P.width i * checkerboardRow A i v ^ 2

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalEnergy (C : Copula 2) (v : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalEnergy C v = ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalEnergy_measurable (C : Copula 2) : Measurable (conditionalEnergy C)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalEnergy_mem (C : Copula 2) (v : ↑unitInterval) : conditionalEnergy C v ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.conditionalEnergy_integrable_comp (C : Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => conditionalEnergy C (f v)) MeasureTheory.volume