Source indexedtheorem · leanprover/lean4:v4.32.0

C_distribution_carlesonOperatorReal_le'_property

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:115 to 126

Mathematical statement

Exact Lean statement

theorem C_distribution_carlesonOperatorReal_le'_property {δ ε : ℝ≥0} (δpos : 0 < δ) :
    ↑ε = ↑(C_distribution_carlesonOperatorReal_le' δ ε) ^ (2 : ℝ)
          * ↑(C10_0_1 4 2) ^ (2 : ℝ) * ENNReal.ofReal (2 * π + 2) / ↑δ ^ (2 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem C_distribution_carlesonOperatorReal_le'_property {δ ε : ℝ≥0} (δpos : 0 < δ) :    ↑ε = ↑(C_distribution_carlesonOperatorReal_le' δ ε) ^ (2 : ℝ)          * ↑(C10_0_1 4 2) ^ (2 : ℝ) * ENNReal.ofReal (2 * π + 2) / ↑δ ^ (2 : ℝ) := by  unfold C_distribution_carlesonOperatorReal_le'  rw [ENNReal.coe_rpow_of_nonneg _ (by simp), ENNReal.rpow_inv_rpow (by simp),    ENNReal.coe_div (by positivity [C10_0_1_pos one_lt_two (a := 4)]),    ENNReal.coe_div (by positivity), ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by simp),    ENNReal.coe_rpow_of_nonneg _ (by simp), ENNReal.ofReal,    mul_assoc, mul_div_assoc, ENNReal.div_mul_cancel _ (ENNReal.div_ne_top      (ENNReal.mul_ne_top (by simp) (by simp)) (by positivity))]  apply ENNReal.div_ne_zero.mpr  use by positivity [C10_0_1_pos one_lt_two (a := 4)], by norm_num