Source indexedlemma · leanprover/lean4:v4.32.0

C_control_approximation_effect_property

Carleson.Classical.ControlApproximationEffect · Carleson/Classical/ControlApproximationEffect.lean:136 to 148

Mathematical statement

Exact Lean statement

lemma C_control_approximation_effect_property {δ ε p : ℝ≥0} (hp : 1 ≤ p) :
    C_control_approximation_effect δ ε p * (2 * ENNReal.ofReal π) ^ (1 - p.toReal⁻¹) ≤ 2 * (↑δ / 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma C_control_approximation_effect_property {δ ε p : ℝ≥0} (hp : 1 ≤ p) :    C_control_approximation_effect δ ε p * (2 * ENNReal.ofReal π) ^ (1 - p.toReal⁻¹) ≤ 2 * (↑δ / 2) := by  calc _    _ ≤ 2 * (↑δ / 2) * ((2 * Real.toNNReal π) ^ (1 - p.toReal⁻¹))⁻¹ * (2 * ENNReal.ofReal π) ^ (1 - p.toReal⁻¹) := by      gcongr      norm_cast      exact min_le_left _ _    _ = 2 * (↑δ / 2) := by      rw [ENNReal.coe_inv (by simp [Real.pi_pos]), ENNReal.coe_rpow_of_nonneg _        (by simp only [sub_nonneg]; exact inv_le_one_of_one_le₀ hp),        ENNReal.coe_mul, ENNReal.coe_ofNat, ENNReal.ofNNReal_toNNReal,        ENNReal.inv_mul_cancel_right (by positivity) (ENNReal.rpow_ne_top' (by positivity)        (ENNReal.mul_ne_top (by simp) (by simp)))]