Source indexedtheorem · leanprover/lean4:v4.32.0

fourierCoeff_eq_fourierCoeff_of_aeeq

Carleson.Classical.Basic · Carleson/Classical/Basic.lean:17 to 27

Mathematical statement

Exact Lean statement

theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} {f g : AddCircle T → ℂ}
    (hf : AEStronglyMeasurable f haarAddCircle) (hg : AEStronglyMeasurable g haarAddCircle)
    (h : f =ᵐ[haarAddCircle] g) : fourierCoeff f n = fourierCoeff g n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fourierCoeff_eq_fourierCoeff_of_aeeq {T : ℝ} [hT : Fact (0 < T)] {n : ℤ} {f g : AddCircle T → ℂ}    (hf : AEStronglyMeasurable f haarAddCircle) (hg : AEStronglyMeasurable g haarAddCircle)    (h : f =ᵐ[haarAddCircle] g) : fourierCoeff f n = fourierCoeff g n := by  unfold fourierCoeff  apply integral_congr_ae  change @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * f =ᶠ[ae haarAddCircle] @DFunLike.coe C(AddCircle T, ℂ) (AddCircle T) (fun x ↦ ℂ) ContinuousMap.instFunLike (fourier (-n)) * g  have fourier_measurable : AEStronglyMeasurable (⇑(@fourier T (-n))) haarAddCircle := (ContinuousMap.measurable _).aestronglyMeasurable  rw [← AEEqFun.mk_eq_mk (hf := fourier_measurable.mul hf) (hg := fourier_measurable.mul hg),      ← AEEqFun.mk_mul_mk _ _ fourier_measurable hf, ← AEEqFun.mk_mul_mk _ _ fourier_measurable hg]  congr 1  rwa [AEEqFun.mk_eq_mk]