Source indexedlemma · leanprover/lean4:v4.32.0

partialFourierSum_aeeq_partialFourierSumLp

Carleson.Classical.Basic · Carleson/Classical/Basic.lean:114 to 120

Mathematical statement

Exact Lean statement

lemma partialFourierSum_aeeq_partialFourierSumLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (N : ℕ) (f : ℝ → ℂ) (h_mem_Lp : MemLp (liftIoc (2 * π) 0 f) 2 haarAddCircle) :
    liftIoc (2 * π) 0 (partialFourierSum N f) =ᶠ[ae haarAddCircle] ↑↑(partialFourierSumLp p N (MemLp.toLp (liftIoc (2 * π) 0 f) h_mem_Lp))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma partialFourierSum_aeeq_partialFourierSumLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (N : ℕ) (f : ℝ → ℂ) (h_mem_Lp : MemLp (liftIoc (2 * π) 0 f) 2 haarAddCircle) :    liftIoc (2 * π) 0 (partialFourierSum N f) =ᶠ[ae haarAddCircle] ↑↑(partialFourierSumLp p N (MemLp.toLp (liftIoc (2 * π) 0 f) h_mem_Lp)) := by  rw [partialFourierSupLp_eq_partialFourierSupLp_of_aeeq (Lp.aestronglyMeasurable _)      h_mem_Lp.aestronglyMeasurable (MemLp.coeFn_toLp h_mem_Lp),    partialFourierSum'_eq_partialFourierSumLp, partialFourierSum_eq_partialFourierSum']  symm  apply MemLp.coeFn_toLp