Source indexedlemma · leanprover/lean4:v4.32.0

distribution_carlesonOperatorReal_le'

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:129 to 147

Mathematical statement

Exact Lean statement

lemma distribution_carlesonOperatorReal_le' {δ ε : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε) {g : ℝ → ℂ}
  (hmg : Measurable g) (hg : ∀ x, ‖g x‖ ≤ C_distribution_carlesonOperatorReal_le' δ ε) :
    distribution (T g) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ ε

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma distribution_carlesonOperatorReal_le' {δ ε : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε) {g : ℝ → ℂ}  (hmg : Measurable g) (hg : ∀ x, ‖g x‖ ≤ C_distribution_carlesonOperatorReal_le' δ ε) :    distribution (T g) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ ε := by  rw [distribution_eq_measure_superlevelSet, Measure.restrict_apply' measurableSet_Ioc]  convert rcarleson_exceptional_set_estimate_specific'' (δ := δ)    (C_distribution_carlesonOperatorReal_le'_pos δpos εpos) hmg hg ?_ ?_ ?_  · exact C_distribution_carlesonOperatorReal_le'_property δpos  · apply MeasurableSet.inter _ measurableSet_Ioc    apply measurableSet_superlevelSet    apply carlesonOperatorReal_measurable hmg.aestronglyMeasurable    intro x    apply Measure.integrableOn_of_bounded _ hmg.aestronglyMeasurable    · filter_upwards      exact hg    · rw [Real.volume_Ioo]      finiteness  · exact Set.inter_subset_right.trans Set.Ioc_subset_Icc_self  · intro x hx    exact hx.1.le