← Copula mathematical handbook

def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionCellMap {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) (i : Fin m) (j : Fin n) (x : Fin 2 → ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionCellMap_continuous {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) (i : Fin m) (j : Fin n) : Continuous (partitionCellMap P Q i j)

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

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionCellLaw P Q i j C = MeasureTheory.Measure.map (ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionCellMap P Q i j) C.toMeasure

instance ProbabilityTheory.Copula.RankRegion.XiBlest.Support.instIsProbabilityMeasureForallFinOfNatNatElemRealUnitIntervalPartitionCellLaw {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) (i : Fin m) (j : Fin n) (C : Copula 2) : MeasureTheory.IsProbabilityMeasure (partitionCellLaw P Q i j C)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.partitionCellLaw_Iic {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) (i : Fin m) (j : Fin n) (C : Copula 2) (u : Fin 2 → ↑unitInterval) : (partitionCellLaw P Q i j C) (Set.Iic u) = ENNReal.ofReal (C.cdf ![P.coord i (u 0), Q.coord j (u 1)])

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