← Mathematical handbook

Lemma 5.2: a sharp inequality for convex functions

A convex function w : [0,1] → ℝ with w(0) = w(1) = 1/2 and w ≥ |u - 1/2| is 1-Lipschitz, hence of the form w(u) = 1/2 + ∫₀ᵘ d for a nondecreasing slope d with |d| ≤ 1 (its one-sided derivative) and ∫₀¹ d = 0. We encode w through this slope (SlopeData); the gap function of a median section is of this form with d = 1 - 2p. The functional is J(w) = ∫₀¹ w (1 - w'²).

Main results: two_q_sq_le_J (J(w) ≥ 2 q², q = w(1/2)) and J_eq_two_q_sq_iff (equality iff w = max {|u - 1/2|, q}).

structure Papers.OrendayLaresRockel2026XiBeta.SlopeData : Type

The slope d = w' of a convex function w on [0,1] with w(0) = w(1) = 1/2 that lies in [-1,1].

• d : ℝ → ℝ

  the (nondecreasing) derivative

• mono : Monotone self.d
• bdd (u : ℝ) : u ∈ Set.Icc 0 1 → |self.d u| ≤ 1
• integral_zero : ∫ (u : ℝ) in 0..1, self.d u = 0

noncomputable def Papers.OrendayLaresRockel2026XiBeta.SlopeData.w (S : SlopeData) (u : ℝ) : ℝ

The convex function w(u) = 1/2 + ∫₀ᵘ w'.

Equations

• S.w u = 1 / 2 + ∫ (t : ℝ) in 0..u, S.d t

noncomputable def Papers.OrendayLaresRockel2026XiBeta.SlopeData.J (S : SlopeData) : ℝ

The functional J(w) = ∫₀¹ w (1 - w'²) of Lemma 5.2.

Equations

• S.J = ∫ (u : ℝ) in 0..1, S.w u * (1 - S.d u ^ 2)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.SlopeData.q (S : SlopeData) : ℝ

q = w(1/2).

Equations

• S.q = S.w (1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.ii (S : SlopeData) (a b : ℝ) : IntervalIntegrable S.d MeasureTheory.volume a b

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.w_sub (S : SlopeData) (a b : ℝ) : S.w b - S.w a = ∫ (t : ℝ) in a..b, S.d t

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.continuous_w (S : SlopeData) : Continuous S.w

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.w_zero (S : SlopeData) : S.w 0 = 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.w_one (S : SlopeData) : S.w 1 = 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.d_ge (S : SlopeData) {u : ℝ} (hu : u ∈ Set.Icc 0 1) : -1 ≤ S.d u

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.d_le (S : SlopeData) {u : ℝ} (hu : u ∈ Set.Icc 0 1) : S.d u ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.w_sub_le (S : SlopeData) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) : |S.w b - S.w a| ≤ b - a

w is 1-Lipschitz on [0,1].

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.w_support (S : SlopeData) {u : ℝ} : S.q + S.d (1 / 2) * (u - 1 / 2) ≤ S.w u

Supporting line of w at 1/2 with slope m = d(1/2).

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.integral_w_mul_d (S : SlopeData) {a b : ℝ} (hab : a ≤ b) : ∫ (t : ℝ) in a..b, S.w t * S.d t = (S.w b ^ 2 - S.w a ^ 2) / 2

d is integrable against continuous functions, and ∫ w w' = [w²/2].

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.w_nonneg (S : SlopeData) {u : ℝ} (hw : ∀ u ∈ Set.Icc 0 1, |u - 1 / 2| ≤ S.w u) (hu : u ∈ Set.Icc 0 1) : 0 ≤ S.w u

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.q_nonneg (S : SlopeData) (hw : ∀ u ∈ Set.Icc 0 1, |u - 1 / 2| ≤ S.w u) : 0 ≤ S.q

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.abs_m_le (S : SlopeData) : |S.d (1 / 2)| ≤ 1 - 2 * S.q

The slope at 1/2 satisfies |m| ≤ 1 - 2q; in particular 2q ≤ 1.

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.two_q_le_one (S : SlopeData) : 2 * S.q ≤ 1

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.ii_sq (S : SlopeData) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) : IntervalIntegrable (fun (u : ℝ) => S.d u ^ 2) MeasureTheory.volume a b

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.ii_F (S : SlopeData) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) : IntervalIntegrable (fun (u : ℝ) => S.w u * (1 - S.d u ^ 2)) MeasureTheory.volume a b

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.J_nonneg (S : SlopeData) (hw : ∀ u ∈ Set.Icc 0 1, |u - 1 / 2| ≤ S.w u) : 0 ≤ S.J

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.J_ge (S : SlopeData) (hw : ∀ u ∈ Set.Icc 0 1, |u - 1 / 2| ≤ S.w u) : (1 - S.d (1 / 2)) * ((∫ (u : ℝ) in 0..1 / 2, S.w u) + S.q ^ 2 / 2 - 1 / 8) + (1 + S.d (1 / 2)) * ((∫ (u : ℝ) in 1 / 2..1, S.w u) - 1 / 8 + S.q ^ 2 / 2) ≤ S.J

The first two lower bounds in the proof of Lemma 5.2.

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.areas (S : SlopeData) (hw : ∀ u ∈ Set.Icc 0 1, |u - 1 / 2| ≤ S.w u) (hq : 0 < S.q) : (1 / 8 + S.q ^ 2 / (2 * (1 + S.d (1 / 2))) ≤ ∫ (u : ℝ) in 0..1 / 2, S.w u ∧ (∫ (u : ℝ) in 0..1 / 2, S.w u = 1 / 8 + S.q ^ 2 / (2 * (1 + S.d (1 / 2))) → ∀ u ∈ Set.Icc 0 (1 / 2), S.w u = max (1 / 2 - u) (S.q + S.d (1 / 2) * (u - 1 / 2)))) ∧ 1 / 8 + S.q ^ 2 / (2 * (1 - S.d (1 / 2))) ≤ ∫ (u : ℝ) in 1 / 2..1, S.w u ∧ (∫ (u : ℝ) in 1 / 2..1, S.w u = 1 / 8 + S.q ^ 2 / (2 * (1 - S.d (1 / 2))) → ∀ u ∈ Set.Icc (1 / 2) 1, S.w u = max (u - 1 / 2) (S.q + S.d (1 / 2) * (u - 1 / 2)))

The two triangle-area bounds (5.4) of Lemma 5.2, with their equality cases.

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.J_slack (S : SlopeData) (hw : ∀ u ∈ Set.Icc 0 1, |u - 1 / 2| ≤ S.w u) (hq : 0 < S.q) : ∃ (ΔX : ℝ) (ΔY : ℝ) (E : ℝ), 0 ≤ ΔX ∧ 0 ≤ ΔY ∧ 0 ≤ E ∧ ΔX = (∫ (u : ℝ) in 0..1 / 2, S.w u) - (1 / 8 + S.q ^ 2 / (2 * (1 + S.d (1 / 2)))) ∧ ΔY = (∫ (u : ℝ) in 1 / 2..1, S.w u) - (1 / 8 + S.q ^ 2 / (2 * (1 - S.d (1 / 2)))) ∧ E = 2 * S.q ^ 2 * S.d (1 / 2) ^ 2 / ((1 + S.d (1 / 2)) * (1 - S.d (1 / 2))) ∧ (1 - S.d (1 / 2)) * ΔX + (1 + S.d (1 / 2)) * ΔY + E + 2 * S.q ^ 2 ≤ S.J

Everything Lemma 5.2 extracts from the two triangle areas when q > 0: slacks ΔX, ΔY ≥ 0 and the AM-GM defect E ≥ 0, with c ΔX + a ΔY + E ≤ J - 2 q².

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.two_q_sq_le_J (S : SlopeData) (hw : ∀ u ∈ Set.Icc 0 1, |u - 1 / 2| ≤ S.w u) : 2 * S.q ^ 2 ≤ S.J

Lemma 5.2, inequality: J(w) ≥ 2 q².