Source indexedtheorem · leanprover/lean4:v4.32.0

partialFourierSum'_comp_equivAddCircle

Carleson.Classical.Basic · Carleson/Classical/Basic.lean:32 to 43

Mathematical statement

Exact Lean statement

theorem partialFourierSum'_comp_equivAddCircle {p q : ℝ} [hp : Fact (0 < p)] [hq : Fact (0 < q)]
  {f : AddCircle q → ℂ} {N : ℕ} {x : AddCircle q} :
    partialFourierSum' N (fun x ↦ f ((AddCircle.equivAddCircle p q hp.out.ne' hq.out.ne') x))
      ((AddCircle.equivAddCircle q p hq.out.ne' hp.out.ne') x)
        = partialFourierSum' N f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem partialFourierSum'_comp_equivAddCircle {p q : ℝ} [hp : Fact (0 < p)] [hq : Fact (0 < q)]  {f : AddCircle q → ℂ} {N : ℕ} {x : AddCircle q} :    partialFourierSum' N (fun x ↦ f ((AddCircle.equivAddCircle p q hp.out.ne' hq.out.ne') x))      ((AddCircle.equivAddCircle q p hq.out.ne' hp.out.ne') x)        = partialFourierSum' N f x := by  unfold partialFourierSum'  simp only [Int.ofNat_eq_natCast, ContinuousMap.coe_sum, ContinuousMap.coe_smul,    Finset.sum_apply, Pi.smul_apply, smul_eq_mul]  congr with n  congr 1  · apply fourierCoeff_comp_equivAddCircle  · apply fourier_comp_equivAddCircle