SincMaskFourier.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The bandwidth of the actual sinc masks. Multiplication by an affine sinc is an average of frequency translations. Repeated multiplication therefore enlarges a spectral annulus by the sum of the individual bandwidths, with the explicit Mathlib 2π normalization.

theorem OAI.LipschitzHilbert.integrable_affine_modulation line 17

theorem OAI.LipschitzHilbert.fourier_affine_modulation line 24

Source documentation

Frequency translation, with an arbitrary affine constant phase.

theorem fourier_affine_modulation (f : ℝ → ℂ) (a b xi : ℝ) :
    𝓕 (fun x : ℝ => Complex.exp (↑(a*x+b : ℝ)*Complex.I)*f x) xi =
      Complex.exp (b*Complex.I)*𝓕 f (xi-a/(2*Real.pi)) := by
…

theorem OAI.LipschitzHilbert.fourier_const_mul line 39
theorem OAI.LipschitzHilbert.fourier_add_integrable line 48
theorem OAI.LipschitzHilbert.affine_cos_identity line 66
theorem OAI.LipschitzHilbert.fourier_affine_cos_mul line 73

theorem OAI.LipschitzHilbert.integrable_affine_sinc_mul line 98

Source documentation

Multiplication by an affine sinc preserves integrability.

theorem integrable_affine_sinc_mul {f : ℝ → ℂ} (hf : Integrable f) (a b : ℝ) :
    Integrable (fun x : ℝ => (Real.sinc (a*x+b):ℂ)*f x) := by
…

theorem OAI.LipschitzHilbert.fourier_affine_sinc_mul line 107

Source documentation

The sinc multiplier is the actual cosine average, including at its zeros and at the origin; Fubini uses only integrability of the packet.

theorem fourier_affine_sinc_mul {f : ℝ → ℂ} (hf : Integrable f) (a b xi : ℝ) :
    𝓕 (fun x : ℝ => (Real.sinc (a*x+b):ℂ)*f x) xi =
      ∫ t in Ioc (0:ℝ) 1, 𝓕 (fun x : ℝ => (Real.cos (t*(a*x+b)):ℂ)*f x) xi := by
…

theorem OAI.LipschitzHilbert.fourier_affine_sinc_mul_eq_zero line 146

Source documentation

No Fourier mass is introduced except translations by at most |a|/(2π). The offset b has no effect on the bandwidth.

theorem fourier_affine_sinc_mul_eq_zero {f : ℝ → ℂ} (hf : Integrable f)
    (a b xi : ℝ)
    (hzero : ∀ eta : ℝ, |eta-xi| ≤ |a|/(2*Real.pi) → 𝓕 f eta = 0) :
    𝓕 (fun x : ℝ => (Real.sinc (a*x+b):ℂ)*f x) xi = 0 := by
…