Source indexedlemma · leanprover/lean4:v4.32.0

CH2.fourier_scale_div_noscalar

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:72 to 80

Mathematical statement

Exact Lean statement

lemma fourier_scale_div_noscalar (φ : ℝ → ℂ) (T u : ℝ) (hT : 0 < T) :
    𝓕 (fun t : ℝ ↦ φ (t / T)) u = (T : ℂ) * 𝓕 φ (T * u)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma fourier_scale_div_noscalar (φ : ℝ → ℂ) (T u : ℝ) (hT : 0 < T) :    𝓕 (fun t : ℝ ↦ φ (t / T)) u = (T : ℂ) * 𝓕 φ (T * u) := by  rw [Real.fourier_real_eq, Real.fourier_real_eq]  have hcomp : (fun v : ℝ ↦ 𝐞 (-(v * u)) • φ (v / T)) =      fun v : ℝ ↦ (fun z : ℝ ↦ 𝐞 (-(z * (T * u))) • φ z) (v / T) := by    ext v; congr 2; simp [show (v / T) * (T * u) = v * u from by field_simp [hT.ne']]  rw [hcomp]  simpa [abs_of_pos hT, smul_eq_mul, mul_assoc, mul_comm, mul_left_comm] using    Measure.integral_comp_div (g := fun z : ℝ ↦ 𝐞 (-(z * (T * u))) • φ z) T