Source indexedlemma · leanprover/lean4:v4.32.0

rcarleson_exceptional_set_estimate_specific'

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:71 to 87

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 ^ (2 : ℝ)⁻¹ ≤ C * C10_0_1 4 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 ^ (2 : ℝ)⁻¹ ≤ C * C10_0_1 4 2 * ENNReal.ofReal (2 * π + 2) ^ (2 : ℝ)⁻¹ := by  by_cases E_zero : volume E = 0  · rw [E_zero]    simp  have E_pow_ne_zero : volume E ^ (2 : ℝ)⁻¹ ≠ 0 := by positivity  have E_pow_finite : volume E ^ (2 : ℝ)⁻¹ < ⊤ := by    rw [ENNReal.rpow_lt_top_iff_of_pos (by simp)]    apply (measure_mono E_subset).trans_lt    rw [Real.volume_Icc]    finiteness  rw [← ENNReal.mul_le_mul_iff_left E_pow_ne_zero E_pow_finite.ne, mul_assoc,    ← ENNReal.rpow_add_of_pos _ _ _ (by simp) (by simp), ← two_mul, mul_inv_cancel₀ (by simp),    ENNReal.rpow_one]  exact rcarleson_exceptional_set_estimate_specific Cpos hmf hf measurableSetE E_subset hE