PositiveFourierCutoff.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

A positive band-limited Schwartz cutoff

A narrow real even smooth bump has a real Fourier transform bounded away from zero on the unit interval. Squaring this transform gives the required cutoff; its Fourier support is controlled by the convolution of the original bumps.

def OAI.Ostmann.narrowBump line 21
def OAI.Ostmann.narrowSchwartz line 24
theorem OAI.Ostmann.narrowSchwartz_apply line 27
theorem OAI.Ostmann.narrowSchwartz_even line 29
theorem OAI.Ostmann.narrow_fourier_real line 32
theorem OAI.Ostmann.narrow_fourier_lower line 45
theorem OAI.Ostmann.narrow_integral_pos line 89
theorem OAI.Ostmann.schwartz_fourier_twice line 98
theorem OAI.Ostmann.narrow_convolution_zero line 103

theorem OAI.Ostmann.exists_positive_even_fourier_cutoff line 119

Source documentation

The cutoff needed by the original amplified moment argument exists.

theorem exists_positive_even_fourier_cutoff :
    ∃ (c : ℝ) (ψ : 𝓢(ℝ, ℂ)), 0 < c ∧
      (∀ x, conj (ψ x) = ψ x) ∧ (∀ x, 0 ≤ (ψ x).re) ∧
      (∀ x ∈ Set.Icc (0 : ℝ) 1, c ≤ (ψ x).re) ∧
      (∀ x : ℝ, (3 : ℝ) ^ 2 < |x| → 𝓕 ψ x = 0) ∧
      (∀ x : ℝ, 𝓕 ψ (-x) = 𝓕 ψ x) := by
…

theorem OAI.Ostmann.exists_positive_fourier_cutoff line 172

Source documentation

A positive Fourier cutoff with bounded derivatives and compact Fourier support.

theorem exists_positive_fourier_cutoff :
    ∃ (c : ℝ) (ψ : 𝓢(ℝ, ℂ)), 0 < c ∧
      (∀ x, conj (ψ x) = ψ x) ∧ (∀ x, 0 ≤ (ψ x).re) ∧
      (∀ x ∈ Set.Icc (0 : ℝ) 1, c ≤ (ψ x).re) ∧
      (∀ x : ℝ, (3 : ℝ) ^ 2 < |x| → 𝓕 ψ x = 0) := by
…

theorem OAI.Ostmann.exists_density_localizer line 182

Source documentation

The compact bump itself localizes a Dirichlet polynomial while its Fourier transform is bounded below throughout the unit height window.

theorem exists_density_localizer :
    ∃ (c : ℝ) (W : 𝓢(ℝ, ℂ)), 0 < c ∧
      (∀ x, 1 ≤ |x| → W x = 0) ∧ (∀ x, ‖W x‖ ≤ 1) ∧
      (∀ t, |t| ≤ 1 → c ≤ ‖𝓕 W t‖) := by
…