← Mathematical handbook

Lemma 5.2: the equality case

J(w) = 2 q² holds iff w = max {|u - 1/2|, q} on [0,1].

theorem Papers.OrendayLaresRockel2026XiBeta.integral_eq_of_eq_on_Ioo {f : ℝ → ℝ} {c d k : ℝ} (hcd : c ≤ d) (h : ∀ t ∈ Set.Ioo c d, f t = k) : ∫ (t : ℝ) in c..d, f t = (d - c) * k

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

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

Lemma 5.2, equality: J(w) = 2 q² forces w = max {|u - 1/2|, q}.

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.d_left (S : SlopeData) (hg : ∀ u ∈ Set.Icc 0 1, S.w u = max |u - 1 / 2| S.q) (hq0 : 0 ≤ S.q) (hq1 : 2 * S.q ≤ 1) {c : ℝ} (hc0 : 0 ≤ c) (hc : c < 1 / 2 - S.q) : S.d c = -1

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.d_mid (S : SlopeData) (hg : ∀ u ∈ Set.Icc 0 1, S.w u = max |u - 1 / 2| S.q) (hq0 : 0 ≤ S.q) (hq1 : 2 * S.q ≤ 1) {c : ℝ} (hc : c ∈ Set.Ioo (1 / 2 - S.q) (1 / 2 + S.q)) : S.d c = 0

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.d_right (S : SlopeData) (hg : ∀ u ∈ Set.Icc 0 1, S.w u = max |u - 1 / 2| S.q) (hq0 : 0 ≤ S.q) (hq1 : 2 * S.q ≤ 1) {c : ℝ} (hc : 1 / 2 + S.q < c) (hc1 : c ≤ 1) : S.d c = 1

theorem Papers.OrendayLaresRockel2026XiBeta.SlopeData.J_eq_of_eq_max (S : SlopeData) (hg : ∀ u ∈ Set.Icc 0 1, S.w u = max |u - 1 / 2| S.q) (hq0 : 0 ≤ S.q) (hq1 : 2 * S.q ≤ 1) : S.J = 2 * S.q ^ 2

Lemma 5.2, equality (converse): w = max {|u - 1/2|, q} gives J(w) = 2 q².

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

Lemma 5.2: J(w) = 2 q² if and only if w = max {|u - 1/2|, q} on [0,1].