Source indexedlemma · leanprover/lean4:v4.32.0

partialFourierSum'_eq_partialFourierSumLp

Carleson.Classical.Basic · Carleson/Classical/Basic.lean:104 to 112

Mathematical statement

Exact Lean statement

lemma partialFourierSum'_eq_partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ℝ≥0∞) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) :
    partialFourierSumLp p N f = MemLp.toLp (partialFourierSum' N f) ((partialFourierSum' N f).memLp haarAddCircle ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma partialFourierSum'_eq_partialFourierSumLp {T : ℝ} [hT : Fact (0 < T)] (p : ℝ≥0∞) [Fact (1 ≤ p)] (N : ℕ) (f : AddCircle T → ℂ) :    partialFourierSumLp p N f = MemLp.toLp (partialFourierSum' N f) ((partialFourierSum' N f).memLp haarAddCircle ℂ)  := by  unfold partialFourierSumLp partialFourierSum'  unfold fourierLp  simp_rw [ContinuousMap.coe_sum, ContinuousMap.coe_smul]  rw [MemLp.toLp_sum _ (by      intro n hn; apply MemLp.const_smul (ContinuousMap.memLp haarAddCircle ℂ (fourier n))),    Finset.univ_eq_attach, ← Finset.sum_attach]  rfl