← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkLaw {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

The patchwork is a weighted sum of affine images of the actual local copula laws.

Equations

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

instance ProbabilityTheory.Copula.RankRegion.XiBlest.Support.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalHSMulENNRealMeasureOfRealMassPartitionCellLaw {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (j : Fin n) : MeasureTheory.IsFiniteMeasure (ENNReal.ofReal (A.mass i j) • partitionCellLaw P Q i j (C i j))

instance ProbabilityTheory.Copula.RankRegion.XiBlest.Support.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalPatchworkLaw {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) : MeasureTheory.IsFiniteMeasure (patchworkLaw A C)

instance ProbabilityTheory.Copula.RankRegion.XiBlest.Support.instIsProbabilityMeasureForallFinOfNatNatElemRealUnitIntervalPatchworkLaw {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) : MeasureTheory.IsProbabilityMeasure (patchworkLaw A C)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkLaw_Iic {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (u : Fin 2 → ↑unitInterval) : (patchworkLaw A C) (Set.Iic u) = ENNReal.ofReal ((A.patchwork C).cdf u)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.toMeasure_patchworkLaw {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) : (A.patchwork C).toMeasure = patchworkLaw A C

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_patchwork {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(A.patchwork C).toMeasure = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * ∫ (x : Fin 2 → ↑unitInterval), f (partitionCellMap P Q i j x) ∂(C i j).toMeasure