← Mathematical handbook

Inverting the clamped mean on its effective parameter interval

theorem Verification.clampedMean_mem (b a : ℝ) : clampedMean b a ∈ Set.Icc 0 1

theorem Verification.clampedMean_strictMonoOn {b : ℝ} (hb : 0 ≤ b) : StrictMonoOn (clampedMean b) (Set.Icc 0 (b + 1))

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

theorem Verification.bandIntercept_mem (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : bandIntercept b hb v ∈ Set.Icc 0 (b + 1)

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

Equations

• Verification.clampedMeanUnit b a = ⟨Verification.clampedMean b a, ⋯⟩

theorem Verification.continuous_clampedMeanUnit (b : ℝ) : Continuous (clampedMeanUnit b)

theorem Verification.bandIntercept_clampedMean (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc 0 (b + 1)) : bandIntercept b hb (clampedMeanUnit b a) = a

theorem Verification.clampedMean_le_iff (b : ℝ) (hb : 0 ≤ b) {a : ℝ} (ha : a ∈ Set.Icc 0 (b + 1)) (v : ↑unitInterval) : clampedMean b a ≤ ↑v ↔ a ≤ bandIntercept b hb v