← Mathematical handbook

Prefix integration for tagged predictor blocks

theorem Verification.upperEmbed_le_iff_ae (a r : ↑unitInterval) (ha : a < 1) : ∀ᵐ (u : ↑unitInterval), ProbabilityTheory.Copula.OrdinalSum.upperEmbed a u ≤ r ↔ u ≤ ProbabilityTheory.Copula.OrdinalSum.upperCoord a r

theorem Verification.integral_unitJoin_prefix (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (f g : ↑unitInterval → ℝ) (hf : Measurable f) (hg : Measurable g) (hi : MeasureTheory.Integrable f MeasureTheory.volume) (hj : MeasureTheory.Integrable g MeasureTheory.volume) (r : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic r, unitJoin a f g u = (↑a * ∫ (u : ↑unitInterval) in Set.Iic (ProbabilityTheory.Copula.OrdinalSum.lowerCoord a r), f u) + (1 - ↑a) * ∫ (u : ↑unitInterval) in Set.Iic (ProbabilityTheory.Copula.OrdinalSum.upperCoord a r), g u