← Mathematical handbook

theorem Verification.partition_indicator_embed {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i r : Fin n) (f : ↑unitInterval → ℝ) : (fun (u : ↑unitInterval) => (Set.Ioc (P.point i.castSucc) (P.point i.succ)).indicator f (partitionEmbed P r u)) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => if r = i then f (partitionEmbed P i u) else 0

theorem Verification.integral_partition_cell {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) {f : ↑unitInterval → ℝ} (hf : Measurable f) (hi : MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (partitionEmbed P i u)) MeasureTheory.volume) : ∫ (u : ↑unitInterval) in Set.Ioc (P.point i.castSucc) (P.point i.succ), f u = P.width i * ∫ (u : ↑unitInterval), f (partitionEmbed P i u)

theorem Verification.conditionalCDF_embed_integrable {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (i : Fin n) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => C.conditionalCDF (partitionEmbed P i u) v) MeasureTheory.volume

theorem Verification.conditionalCDF_embed_sq_integrable {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (i : Fin n) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => C.conditionalCDF (partitionEmbed P i u) v ^ 2) MeasureTheory.volume

noncomputable def Verification.copulaRowMean {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (i : Fin n) (v : ↑unitInterval) : ℝ

Equations

• Verification.copulaRowMean P C i v = (C.cdf ![P.point i.succ, v] - C.cdf ![P.point i.castSucc, v]) / P.width i

theorem Verification.copulaRowMean_integral {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (i : Fin n) (v : ↑unitInterval) : copulaRowMean P C i v = ∫ (u : ↑unitInterval), C.conditionalCDF (partitionEmbed P i u) v

theorem Verification.copulaRowMean_energy_le {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : ∑ i : Fin n, P.width i * copulaRowMean P C i v ^ 2 ≤ ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2