Source indexedlemma · leanprover/lean4:v4.32.0

integrable_annulus

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:125 to 134

Mathematical statement

Exact Lean statement

lemma integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}
    (hf : IntervalIntegrable f volume (-π) (3 * π)) {r : ℝ} (r_nonneg : 0 ≤ r) (rle1 : r < 1) :
    Integrable (fun x ↦ f x) (volume.restrict {y | dist x y ∈ Set.Ioo r 1})

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}    (hf : IntervalIntegrable f volume (-π) (3 * π)) {r : ℝ} (r_nonneg : 0 ≤ r) (rle1 : r < 1) :    Integrable (fun x ↦ f x) (volume.restrict {y | dist x y ∈ Set.Ioo r 1}) := by  rw [← IntegrableOn, annulus_real_eq r_nonneg]  apply IntegrableOn.union <;>  · rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)]    apply hf.mono_set    rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [pi_pos])]    intro y hy    constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]