theorem
Verification.volume_partition
{n : ℕ}
(P : ProbabilityTheory.Copula.IntervalPartition n)
:
MeasureTheory.volume = ∑ i : Fin n, ENNReal.ofReal (P.width i) • MeasureTheory.Measure.map (partitionEmbed P i) MeasureTheory.volume
theorem
Verification.integrable_partition
{n : ℕ}
(P : ProbabilityTheory.Copula.IntervalPartition n)
{f : ↑unitInterval → ℝ}
(hf : Measurable f)
(hi :
∀ (i : Fin n), MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (partitionEmbed P i u)) MeasureTheory.volume)
:
theorem
Verification.integral_partition
{n : ℕ}
(P : ProbabilityTheory.Copula.IntervalPartition n)
(f : ↑unitInterval → ℝ)
(hf : Measurable f)
(hi :
∀ (i : Fin n), MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (partitionEmbed P i u)) MeasureTheory.volume)
:
∫ (u : ↑unitInterval), f u = ∑ i : Fin n, P.width i * ∫ (u : ↑unitInterval), f (partitionEmbed P i u)