← Mathematical handbook

noncomputable def Verification.partitionPiece {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) (f : ↑unitInterval → ℝ) (u : ↑unitInterval) : ℝ

Equations

• Verification.partitionPiece P i f u = if P.point i.castSucc < u ∧ u ≤ P.point i.succ then f (P.coord i u) else 0

theorem Verification.partition_coord_continuous {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) : Continuous (P.coord i)

theorem Verification.partitionPiece_measurable {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) {f : ↑unitInterval → ℝ} (hf : Measurable f) : Measurable (partitionPiece P i f)

theorem Verification.partitionEmbed_strict_lower {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) (u : ↑unitInterval) (hu : 0 < u) : P.point i.castSucc < partitionEmbed P i u

theorem Verification.partitionPiece_embed {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i r : Fin n) (f : ↑unitInterval → ℝ) (u : ↑unitInterval) (hu : 0 < u) : partitionPiece P i f (partitionEmbed P r u) = if r = i then f u else 0

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

theorem Verification.partitionPiece_integrable {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) {f : ↑unitInterval → ℝ} (hf : Measurable f) (hi : MeasureTheory.Integrable f MeasureTheory.volume) : MeasureTheory.Integrable (partitionPiece P i f) MeasureTheory.volume

theorem Verification.partitionPiece_prefix_embed {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i r : Fin n) (f : ↑unitInterval → ℝ) (t : ↑unitInterval) : (fun (u : ↑unitInterval) => (Set.Iic t).indicator (partitionPiece P i f) (partitionEmbed P r u)) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => if r = i then (Set.Iic (P.coord i t)).indicator f u else 0

theorem Verification.integral_partitionPiece_Iic {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin n) {f : ↑unitInterval → ℝ} (hf : Measurable f) (hi : MeasureTheory.Integrable f MeasureTheory.volume) (t : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic t, partitionPiece P i f u = P.width i * ∫ (u : ↑unitInterval) in Set.Iic (P.coord i t), f u

theorem Verification.partitionSum_embed_ae {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (f : Fin n → ↑unitInterval → ℝ) (r : Fin n) : (fun (u : ↑unitInterval) => ∑ i : Fin n, partitionPiece P i (f i) (partitionEmbed P r u)) =ᵐ[MeasureTheory.volume] f r

theorem Verification.integral_partitionSum_sq {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (f : Fin n → ↑unitInterval → ℝ) (hf : ∀ (i : Fin n), Measurable (f i)) (hi : ∀ (i : Fin n), MeasureTheory.Integrable (fun (u : ↑unitInterval) => f i u ^ 2) MeasureTheory.volume) : ∫ (u : ↑unitInterval), (∑ i : Fin n, partitionPiece P i (f i) u) ^ 2 = ∑ i : Fin n, P.width i * ∫ (u : ↑unitInterval), f i u ^ 2