← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (v u : ↑unitInterval) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkKernel {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (v u : ↑unitInterval) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow_measurable {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (v : ↑unitInterval) : Measurable (patchworkRow A C i v)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow_integrable {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (v : ↑unitInterval) : MeasureTheory.Integrable (patchworkRow A C i v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkKernel_integrable {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (v : ↑unitInterval) : MeasureTheory.Integrable (patchworkKernel A C v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkKernel_nonneg {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (v u : ↑unitInterval) : 0 ≤ patchworkKernel A C v u

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_patchworkRow_Iic {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (v t : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic t, patchworkRow A C i v u = ∑ j : Fin n, A.mass i j / P.width i * (C i j).cdf ![t, Q.coord j v]

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchwork_conditionalCDF {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (A.patchwork C).conditionalCDF u v) =ᵐ[MeasureTheory.volume] patchworkKernel A C v