← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.volume_partition {n : ℕ} (P : IntervalPartition n) : MeasureTheory.volume = ∑ i : Fin n, ENNReal.ofReal (P.width i) • MeasureTheory.Measure.map (partitionEmbed P i) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integrable_partition {n : ℕ} (P : IntervalPartition n) {f : ↑unitInterval → ℝ} (hf : Measurable f) (hi : ∀ (i : Fin n), MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (partitionEmbed P i u)) MeasureTheory.volume) : MeasureTheory.Integrable f MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.integral_partition {n : ℕ} (P : 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)