Source indexedlemma · leanprover/lean4:v4.32.0

rcarleson_exceptional_set_estimate_specific''

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:90 to 101

Mathematical statement

Exact Lean statement

lemma rcarleson_exceptional_set_estimate_specific'' {δ C : ℝ≥0} (Cpos : 0 < C) {f : ℝ → ℂ}
  (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ C) {E : Set ℝ} (measurableSetE : MeasurableSet E)
  (E_subset : E ⊆ Set.Icc 0 (2 * π)) (hE : ∀ x ∈ E, δ ≤ T f x) :
    volume E ≤ C ^ (2 : ℝ) * C10_0_1 4 2 ^ (2 : ℝ) * ENNReal.ofReal (2 * π + 2) / δ ^ (2 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rcarleson_exceptional_set_estimate_specific'' {δ C : ℝ≥0} (Cpos : 0 < C) {f : ℝ → ℂ}  (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ C) {E : Set ℝ} (measurableSetE : MeasurableSet E)  (E_subset : E ⊆ Set.Icc 0 (2 * π)) (hE : ∀ x ∈ E, δ ≤ T f x) :    volume E ≤ C ^ (2 : ℝ) * C10_0_1 4 2 ^ (2 : ℝ) * ENNReal.ofReal (2 * π + 2) / δ ^ (2 : ℝ) := by  rw [ENNReal.le_div_iff_mul_le (by right; positivity [C10_0_1_pos one_lt_two (a := 4)]) (by simp),    mul_comm]  have : 0 < (2 : ℝ)⁻¹ := by positivity  rw [← ENNReal.rpow_le_rpow_iff this, ENNReal.mul_rpow_of_nonneg _ _ this.le,    ENNReal.mul_rpow_of_nonneg _ _ this.le, ENNReal.mul_rpow_of_nonneg _ _ this.le,    ENNReal.rpow_rpow_inv (by simp), ENNReal.rpow_rpow_inv (by simp),    ENNReal.rpow_rpow_inv (by simp)]  exact rcarleson_exceptional_set_estimate_specific' Cpos hmf hf measurableSetE E_subset hE