← Mathematical handbook

Elementary integral lemmas for Lemma 5.2

Areas under the maximum of two lines (the triangles of the source's inequality (5.4)), and vanishing of continuous nonnegative functions with zero integral.

theorem Papers.OrendayLaresRockel2026XiBeta.int_lin (α β a b : ℝ) : ∫ (u : ℝ) in a..b, α + β * u = α * (b - a) + β * (b ^ 2 - a ^ 2) / 2

theorem Papers.OrendayLaresRockel2026XiBeta.eq_zero_of_integral_eq_zero {f : ℝ → ℝ} (hf : Continuous f) {a b : ℝ} (hab : a < b) (h0 : ∀ x ∈ Set.Icc a b, 0 ≤ f x) (hint : ∫ (x : ℝ) in a..b, f x = 0) (x : ℝ) : x ∈ Set.Icc a b → f x = 0

A continuous nonnegative function with vanishing integral vanishes.

theorem Papers.OrendayLaresRockel2026XiBeta.integral_max_lines {q m : ℝ} (hq : 0 ≤ q) (hm : 0 < 1 + m) (hqm : 2 * q ≤ 1 + m) : ∫ (u : ℝ) in 0..1 / 2, max (1 / 2 - u) (q + m * (u - 1 / 2)) = 1 / 8 + q ^ 2 / (2 * (1 + m))

The area under max (1/2 - u) (q + m (u - 1/2)) on [0, 1/2].

theorem Papers.OrendayLaresRockel2026XiBeta.area_left {f : ℝ → ℝ} (hf : Continuous f) {q m : ℝ} (hq : 0 ≤ q) (hm : 0 < 1 + m) (hqm : 2 * q ≤ 1 + m) (h1 : ∀ u ∈ Set.Icc 0 (1 / 2), 1 / 2 - u ≤ f u) (h2 : ∀ u ∈ Set.Icc 0 (1 / 2), q + m * (u - 1 / 2) ≤ f u) : 1 / 8 + q ^ 2 / (2 * (1 + m)) ≤ ∫ (u : ℝ) in 0..1 / 2, f u ∧ (∫ (u : ℝ) in 0..1 / 2, f u = 1 / 8 + q ^ 2 / (2 * (1 + m)) → ∀ u ∈ Set.Icc 0 (1 / 2), f u = max (1 / 2 - u) (q + m * (u - 1 / 2)))

The lower area bound of (5.4) on the left half, with its equality case.

theorem Papers.OrendayLaresRockel2026XiBeta.area_right {f : ℝ → ℝ} (hf : Continuous f) {q m : ℝ} (hq : 0 ≤ q) (hm : 0 < 1 - m) (hqm : 2 * q ≤ 1 - m) (h1 : ∀ u ∈ Set.Icc (1 / 2) 1, u - 1 / 2 ≤ f u) (h2 : ∀ u ∈ Set.Icc (1 / 2) 1, q + m * (u - 1 / 2) ≤ f u) : 1 / 8 + q ^ 2 / (2 * (1 - m)) ≤ ∫ (u : ℝ) in 1 / 2..1, f u ∧ (∫ (u : ℝ) in 1 / 2..1, f u = 1 / 8 + q ^ 2 / (2 * (1 - m)) → ∀ u ∈ Set.Icc (1 / 2) 1, f u = max (u - 1 / 2) (q + m * (u - 1 / 2)))

The mirror image of area_left on the right half.