← Mathematical handbook

Two-bin Jensen inequality as an exact squared-distance identity

noncomputable def Verification.twoBin (v : ↑unitInterval) (a b : ℝ) (u : ↑unitInterval) : ℝ

Equations

• Verification.twoBin v a b u = b + (a - b) * Verification.lowerStep v u

theorem Verification.twoBin_eq (v : ↑unitInterval) (a b : ℝ) (u : ↑unitInterval) : twoBin v a b u = if u ≤ v then a else b

theorem Verification.integrable_twoBin (v : ↑unitInterval) (a b : ℝ) : MeasureTheory.Integrable (twoBin v a b) MeasureTheory.volume

theorem Verification.integral_twoBin_Iic (v : ↑unitInterval) (a b : ℝ) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, twoBin v a b t = b * ↑u + (a - b) * min ↑u ↑v

theorem Verification.integral_twoBin (v : ↑unitInterval) (a b : ℝ) : ∫ (u : ↑unitInterval), twoBin v a b u = ↑v * a + (1 - ↑v) * b

theorem Verification.twoBin_sq (v : ↑unitInterval) (a b : ℝ) : (fun (u : ↑unitInterval) => twoBin v a b u ^ 2) = twoBin v (a ^ 2) (b ^ 2)

theorem Verification.integrable_mul_twoBin {g : ↑unitInterval → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (v : ↑unitInterval) (a b : ℝ) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => g u * twoBin v a b u) MeasureTheory.volume

theorem Verification.integral_mul_twoBin {g : ↑unitInterval → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (v : ↑unitInterval) (a b : ℝ) : ∫ (u : ↑unitInterval), g u * twoBin v a b u = (b * ∫ (u : ↑unitInterval), g u) + (a - b) * ∫ (u : ↑unitInterval) in Set.Iic v, g u

theorem Verification.twoBin_projection {g : ↑unitInterval → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hs : MeasureTheory.Integrable (fun (u : ↑unitInterval) => g u ^ 2) MeasureTheory.volume) (v : ↑unitInterval) (a b : ℝ) (hm : ∫ (u : ↑unitInterval), g u = ↑v * a + (1 - ↑v) * b) (hl : ∫ (u : ↑unitInterval) in Set.Iic v, g u = ↑v * a) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => (g u - twoBin v a b u) ^ 2) MeasureTheory.volume ∧ ∫ (u : ↑unitInterval), (g u - twoBin v a b u) ^ 2 = (∫ (u : ↑unitInterval), g u ^ 2) - (↑v * a ^ 2 + (1 - ↑v) * b ^ 2)

theorem Verification.twoBin_jensen {g : ↑unitInterval → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hs : MeasureTheory.Integrable (fun (u : ↑unitInterval) => g u ^ 2) MeasureTheory.volume) (v : ↑unitInterval) (a b : ℝ) (hm : ∫ (u : ↑unitInterval), g u = ↑v * a + (1 - ↑v) * b) (hl : ∫ (u : ↑unitInterval) in Set.Iic v, g u = ↑v * a) : ↑v * a ^ 2 + (1 - ↑v) * b ^ 2 ≤ ∫ (u : ↑unitInterval), g u ^ 2

theorem Verification.twoBin_jensen_eq_iff {g : ↑unitInterval → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hs : MeasureTheory.Integrable (fun (u : ↑unitInterval) => g u ^ 2) MeasureTheory.volume) (v : ↑unitInterval) (a b : ℝ) (hm : ∫ (u : ↑unitInterval), g u = ↑v * a + (1 - ↑v) * b) (hl : ∫ (u : ↑unitInterval) in Set.Iic v, g u = ↑v * a) : ∫ (u : ↑unitInterval), g u ^ 2 = ↑v * a ^ 2 + (1 - ↑v) * b ^ 2 ↔ g =ᵐ[MeasureTheory.volume] twoBin v a b