Source indexedlemma · leanprover/lean4:v4.32.0

partialFourierSum'_eq_partialFourierSum_apply

Carleson.Classical.Basic · Carleson/Classical/Basic.lean:79 to 92

Mathematical statement

Exact Lean statement

lemma partialFourierSum'_eq_partialFourierSum_apply (N : ℕ) (f : AddCircle (2 * π) → ℂ)
  {x : ℝ} (hx : x ∈ Set.Ioc 0 (2 * π)) :
    partialFourierSum' N f x
    = (partialFourierSum N (fun x ↦ f x)) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma partialFourierSum'_eq_partialFourierSum_apply (N : ℕ) (f : AddCircle (2 * π) → ℂ)  {x : ℝ} (hx : x ∈ Set.Ioc 0 (2 * π)) :    partialFourierSum' N f x    = (partialFourierSum N (fun x ↦ f x)) x := by  have : partialFourierSum' N f = partialFourierSum' N (liftIoc (2 * π) 0 fun x ↦ f ↑x) := by    unfold partialFourierSum'    congr with n x    congr 2    rw [fourierCoeff_congr_ae (g := (fun x ↦ liftIoc (2 * π) 0 (fun x ↦ f ↑x) ↑x))]    rw [Filter.EventuallyEq]    filter_upwards with x    unfold liftIoc    simp  rw [this, ← partialFourierSum_eq_partialFourierSum' N _, liftIoc_coe_apply (by simpa)]