← Mathematical handbook

Differentiating the clamped quadratic normalization map

theorem Verification.unitClamp_lipschitz : LipschitzWith 1 unitClamp

theorem Verification.hasDerivAt_unitClamp (x : ℝ) (hx0 : x ≠ 0) (hx1 : x ≠ 1) : HasDerivAt unitClamp (if 0 < x ∧ x < 1 then 1 else 0) x

theorem Verification.square_ae_ne (a : ℝ) : ∀ᵐ (x : ↑unitInterval), ↑x ^ 2 ≠ a

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

Equations

• Verification.clampedSquareMean b q = ∫ (x : ↑unitInterval), Verification.unitClamp (b * (↑x ^ 2 - q))

theorem Verification.clampedSquareMean_hasDerivAt_integral (b q : ℝ) (hb : 0 < b) : HasDerivAt (clampedSquareMean b) (∫ (x : ↑unitInterval), if 0 < b * (↑x ^ 2 - q) ∧ b * (↑x ^ 2 - q) < 1 then -b else 0) q

theorem Verification.clampedSquareMean_hasDerivAt (b q : ℝ) (hb : 0 < b) (hq : q ∈ Set.Icc (-1 / b) 1) : HasDerivAt (clampedSquareMean b) (-b * (quadraticUpper b q - quadraticLower q)) q