The section formulas in Lemma 4.1 #
theorem
Papers.Rockel2026XiBlest.section_formulas
(b q : ℝ)
(hb : 0 < b)
(hq : q ∈ Set.Icc (-1 / b) 1)
:
have r := Verification.quadraticLower q;
have s := Verification.quadraticUpper b q;
∫ (t : ↑unitInterval), Verification.unitClamp (b * ((1 - ↑t) ^ 2 - q)) = 1 - s + b * (Verification.quadraticT q s - Verification.quadraticT q r) ∧ ∫ (t : ↑unitInterval), Verification.unitClamp (b * ((1 - ↑t) ^ 2 - q)) ^ 2 = 1 - s + b ^ 2 * (Verification.quadraticF q s - Verification.quadraticF q r) ∧ ∫ (t : ↑unitInterval), (1 - ↑t) ^ 2 * Verification.unitClamp (b * ((1 - ↑t) ^ 2 - q)) = (1 - s ^ 3) / 3 + b * (Verification.quadraticS q s - Verification.quadraticS q r)
Equations (20)-(22); s is X_a and r is X_s, so the plateau length is 1-s.