← Mathematical handbook

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

Equations

• Verification.partitionCellMap P Q i j x = ![Verification.partitionEmbed P i (x 0), Verification.partitionEmbed Q j (x 1)]

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

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

Equations

• Verification.partitionCellLaw P Q i j C = MeasureTheory.Measure.map (Verification.partitionCellMap P Q i j) C.toMeasure

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

theorem Verification.partitionCellLaw_Iic {m n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin m) (j : Fin n) (C : ProbabilityTheory.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 Verification.integral_partitionCellLaw {m n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin m) (j : Fin n) (C : ProbabilityTheory.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