← Mathematical handbook

Inverting the clamped mean on its effective parameter interval

theorem Verification.quadraticMean_mem (b a : ℝ) : quadraticMean b a ∈ Set.Icc 0 1

theorem Verification.quadraticMean_strictMonoOn {b : ℝ} (hb : 0 ≤ b) : StrictMonoOn (quadraticMean b) (Set.Icc (-b) 1)

Strictness holds on the entire effective intercept range, including its endpoints.

theorem Verification.quadraticIntercept_mem (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : quadraticIntercept b hb v ∈ Set.Icc (-b) 1

noncomputable def Verification.quadraticMeanUnit (b a : ℝ) : ↑unitInterval

Equations

• Verification.quadraticMeanUnit b a = ⟨Verification.quadraticMean b a, ⋯⟩

theorem Verification.continuous_quadraticMeanUnit (b : ℝ) : Continuous (quadraticMeanUnit b)

theorem Verification.quadraticIntercept_quadraticMean (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc (-b) 1) : quadraticIntercept b hb (quadraticMeanUnit b a) = a

theorem Verification.quadraticMean_le_iff (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc (-b) 1) (v : ↑unitInterval) : quadraticMean b a ≤ ↑v ↔ a ≤ quadraticIntercept b hb v