SincMaskSpectrum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite powers of the exact sinc mask preserve a Fourier annulus with its explicitly accumulated bandwidth.

theorem OAI.LipschitzHilbert.integrable_affine_sinc_pow_mul line 13

theorem OAI.LipschitzHilbert.fourier_affine_sinc_pow_mul_eq_zero line 24

Source documentation

The radius adds once for each factor; the affine offset never contributes to the support radius.

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

theorem OAI.LipschitzHilbert.fourier_sinc_pair_pow_mul_eq_zero line 50

theorem OAI.LipschitzHilbert.sincProductMask_fourier_annulus line 73

Source documentation

An explicit annulus statement for the even sinc product.

theorem sincProductMask_fourier_annulus {f : ℝ → ℂ} (hf : Integrable f)
    (n : ℕ) (a b c d lo hi : ℝ)
    (hlow : ∀ xi, |xi| < lo → 𝓕 f xi = 0)
    (hhigh : ∀ xi, hi < |xi| → 𝓕 f xi = 0) :
    let B := (2*(n:ℝ))*((|a|+|c|)/(2*Real.pi))
…