Source indexedtheorem · leanprover/lean4:v4.32.0

fourier_comp_equivAddCircle

Carleson.ToMathlib.Analysis.Fourier.AddCircle · Carleson/ToMathlib/Analysis/Fourier/AddCircle.lean:7 to 18

Mathematical statement

Exact Lean statement

theorem fourier_comp_equivAddCircle {p q : ℝ} [hp : Fact (0 < p)] [hq : Fact (0 < q)]
  {x : AddCircle p} {n : ℤ} :
    fourier n (AddCircle.equivAddCircle p q hp.out.ne' hq.out.ne' x) = fourier n x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fourier_comp_equivAddCircle {p q : ℝ} [hp : Fact (0 < p)] [hq : Fact (0 < q)]  {x : AddCircle p} {n : ℤ} :    fourier n (AddCircle.equivAddCircle p q hp.out.ne' hq.out.ne' x) = fourier n x := by  simp only [fourier_apply, SetLike.coe_eq_coe]  rw [AddCircle.toCircle_zsmul, AddCircle.toCircle_zsmul]  congr 1  rw [AddCircle.equivAddCircle_eq]  have : ↑↑((AddCircle.equivIco p 0) x) = x := AddCircle.coe_equivIco  nth_rw 2 [← this]  rw [AddCircle.toCircle_apply_mk, AddCircle.toCircle_apply_mk]  congr 1  field [hq.out.ne']