← Mathematical handbook

Exact section moments for clamped quadratics

noncomputable def Verification.quadraticLower (q : ℝ) : ℝ

Equations

• Verification.quadraticLower q = √(max 0 q)

noncomputable def Verification.quadraticUpper (b q : ℝ) : ℝ

Equations

• Verification.quadraticUpper b q = min 1 √(q + 1 / b)

theorem Verification.quadratic_switch_bounds (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) : 0 ≤ quadraticLower q ∧ quadraticLower q ≤ quadraticUpper b q ∧ quadraticUpper b q ≤ 1

theorem Verification.quadratic_section_moment (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) (m k : ℕ) (hk : k ≠ 0) : ∫ (x : ℝ) in 0..1, x ^ m * unitClamp (b * (x ^ 2 - q)) ^ k = (b ^ k * ∫ (x : ℝ) in quadraticLower q..quadraticUpper b q, x ^ m * (x ^ 2 - q) ^ k) + ∫ (x : ℝ) in quadraticUpper b q..1, x ^ m

noncomputable def Verification.quadraticT (q x : ℝ) : ℝ

Equations

• Verification.quadraticT q x = x ^ 3 / 3 - q * x

noncomputable def Verification.quadraticF (q x : ℝ) : ℝ

Equations

• Verification.quadraticF q x = x ^ 5 / 5 - 2 * q / 3 * x ^ 3 + q ^ 2 * x

noncomputable def Verification.quadraticS (q x : ℝ) : ℝ

Equations

• Verification.quadraticS q x = x ^ 5 / 5 - q / 3 * x ^ 3

theorem Verification.integral_quadratic_polynomials (q a c : ℝ) : ∫ (x : ℝ) in a..c, x ^ 2 - q = quadraticT q c - quadraticT q a ∧ ∫ (x : ℝ) in a..c, (x ^ 2 - q) ^ 2 = quadraticF q c - quadraticF q a ∧ ∫ (x : ℝ) in a..c, x ^ 2 * (x ^ 2 - q) = quadraticS q c - quadraticS q a