← Copula mathematical handbook

Probability measures and integration for binary ordinal sums

The ordinal-sum measure is the weighted sum of the two component measures pushed into their respective squares. This representation also covers singular copulas and zero-length blocks.

theorem ProbabilityTheory.Copula.OrdinalSum.continuous_lowerEmbed (a : ↑unitInterval) : Continuous (lowerEmbed a)

theorem ProbabilityTheory.Copula.OrdinalSum.continuous_upperEmbed (a : ↑unitInterval) : Continuous (upperEmbed a)

theorem ProbabilityTheory.Copula.OrdinalSum.measurable_lowerEmbed (a : ↑unitInterval) : Measurable (lowerEmbed a)

theorem ProbabilityTheory.Copula.OrdinalSum.measurable_upperEmbed (a : ↑unitInterval) : Measurable (upperEmbed a)

theorem ProbabilityTheory.Copula.OrdinalSum.lowerEmbed_le_iff (a x u : ↑unitInterval) (ha : 0 < a) : lowerEmbed a x ≤ u ↔ x ≤ lowerCoord a u

theorem ProbabilityTheory.Copula.OrdinalSum.upperEmbed_le_iff (a x u : ↑unitInterval) (ha : a < 1) (hu : a ≤ u) : upperEmbed a x ≤ u ↔ x ≤ upperCoord a u

theorem ProbabilityTheory.Copula.OrdinalSum.measureReal_map_lowerEmbed_Iic (C : Copula 2) (a : ↑unitInterval) (ha : 0 < a) (u : Fin 2 → ↑unitInterval) : (MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) (i : Fin 2) => lowerEmbed a (x i)) C.toMeasure).real (Set.Iic u) = C.cdf fun (i : Fin 2) => lowerCoord a (u i)

theorem ProbabilityTheory.Copula.OrdinalSum.measureReal_map_upperEmbed_Iic (C : Copula 2) (a : ↑unitInterval) (ha : a < 1) (u : Fin 2 → ↑unitInterval) : (MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) (i : Fin 2) => upperEmbed a (x i)) C.toMeasure).real (Set.Iic u) = C.cdf fun (i : Fin 2) => upperCoord a (u i)

theorem ProbabilityTheory.Copula.toMeasure_eq_of_measureReal_Iic {d : ℕ} (C : Copula d) (μ : MeasureTheory.Measure (Fin d → ↑unitInterval)) [hprob : MeasureTheory.IsProbabilityMeasure μ] (hμ : ∀ (u : Fin d → ↑unitInterval), μ.real (Set.Iic u) = C.cdf u) : C.toMeasure = μ

Identify a candidate probability law by its lower-orthant probabilities.

theorem ProbabilityTheory.Copula.toMeasure_ordinalSum (C D : Copula 2) (a : ↑unitInterval) : (C.ordinalSum D a).toMeasure = ENNReal.ofReal ↑a • MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) (i : Fin 2) => OrdinalSum.lowerEmbed a (x i)) C.toMeasure + ENNReal.ofReal (1 - ↑a) • MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) (i : Fin 2) => OrdinalSum.upperEmbed a (x i)) D.toMeasure

theorem ProbabilityTheory.Copula.integral_ordinalSum (C D : Copula 2) (a : ↑unitInterval) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(C.ordinalSum D a).toMeasure = ↑a * ∫ (x : Fin 2 → ↑unitInterval), f fun (i : Fin 2) => OrdinalSum.lowerEmbed a (x i) ∂C.toMeasure + (1 - ↑a) * ∫ (x : Fin 2 → ↑unitInterval), f fun (i : Fin 2) => OrdinalSum.upperEmbed a (x i) ∂D.toMeasure

Integrate a continuous observable by integrating over each component square.