Source indexedlemma · leanprover/lean4:v4.32.0

rcarleson_exceptional_set_estimate_specific

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:50 to 68

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 * C10_0_1 4 2 * ENNReal.ofReal (2 * π + 2) ^ (2 : ℝ)⁻¹ * volume E ^ (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 * C10_0_1 4 2 * ENNReal.ofReal (2 * π + 2) ^ (2 : ℝ)⁻¹ * volume E ^ (2 : ℝ)⁻¹ := by  set F := (Set.Ioo (0 - 1) (2 * π + 1))  set h := F.indicator f with hdef  have hh : ∀ x, ‖h x‖ ≤ C * F.indicator 1 x := by    intro x    rw [hdef, norm_indicator_eq_indicator_norm, Set.indicator, Set.indicator]    split_ifs with hx    · simp only [Pi.one_apply, mul_one]; exact hf x    · simp  convert rcarleson_exceptional_set_estimate Cpos (hmf.indicator measurableSet_Ioo)    measurableSet_Ioo hh measurableSetE ?_  · rw [Real.volume_Ioo]    ring_nf  · intro x hx    rw [← carlesonOperatorReal_eq_of_restrict_interval (E_subset hx)]    exact hE x hx