← Mathematical handbook

Splitting a uniform predictor into two affine blocks

theorem Verification.volume_unit_split (a : ↑unitInterval) : MeasureTheory.volume = ENNReal.ofReal ↑a • MeasureTheory.Measure.map (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a) MeasureTheory.volume + ENNReal.ofReal (1 - ↑a) • MeasureTheory.Measure.map (ProbabilityTheory.Copula.OrdinalSum.upperEmbed a) MeasureTheory.volume

theorem Verification.integral_unit_split (a : ↑unitInterval) (f : ↑unitInterval → ℝ) (hf : Measurable f) (hL : MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a u)) MeasureTheory.volume) (hU : MeasureTheory.Integrable (fun (u : ↑unitInterval) => f (ProbabilityTheory.Copula.OrdinalSum.upperEmbed a u)) MeasureTheory.volume) : ∫ (u : ↑unitInterval), f u = (↑a * ∫ (u : ↑unitInterval), f (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a u)) + (1 - ↑a) * ∫ (u : ↑unitInterval), f (ProbabilityTheory.Copula.OrdinalSum.upperEmbed a u)

noncomputable def Verification.unitJoin (a : ↑unitInterval) (f g : ↑unitInterval → ℝ) (u : ↑unitInterval) : ℝ

Equations

• Verification.unitJoin a f g u = if u ≤ a then f (ProbabilityTheory.Copula.OrdinalSum.lowerCoord a u) else g (ProbabilityTheory.Copula.OrdinalSum.upperCoord a u)

theorem Verification.measurable_unitJoin (a : ↑unitInterval) {f g : ↑unitInterval → ℝ} (hf : Measurable f) (hg : Measurable g) : Measurable (unitJoin a f g)

theorem Verification.unitJoin_lower (a : ↑unitInterval) (ha : 0 < a) (f g : ↑unitInterval → ℝ) (u : ↑unitInterval) : unitJoin a f g (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a u) = f u

theorem Verification.unitJoin_upper (a : ↑unitInterval) (ha : a < 1) (f g : ↑unitInterval → ℝ) : (fun (u : ↑unitInterval) => unitJoin a f g (ProbabilityTheory.Copula.OrdinalSum.upperEmbed a u)) =ᵐ[MeasureTheory.volume] g

theorem Verification.integral_unitJoin (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) : ∫ (u : ↑unitInterval), unitJoin a f g u = (↑a * ∫ (u : ↑unitInterval), f u) + (1 - ↑a) * ∫ (u : ↑unitInterval), g u

theorem Verification.integral_lowerCoord (a : ↑unitInterval) (ha : 0 < a) (f : ↑unitInterval → ℝ) (hf : Measurable f) (hi : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (u : ↑unitInterval), f (ProbabilityTheory.Copula.OrdinalSum.lowerCoord a u) = (↑a * ∫ (u : ↑unitInterval), f u) + (1 - ↑a) * f 1

theorem Verification.integral_upperCoord (a : ↑unitInterval) (ha : a < 1) (f : ↑unitInterval → ℝ) (hf : Measurable f) (hi : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (u : ↑unitInterval), f (ProbabilityTheory.Copula.OrdinalSum.upperCoord a u) = ↑a * f 0 + (1 - ↑a) * ∫ (u : ↑unitInterval), f u