OAI/NumberTheory/Ostmann/Arithmetic/LeafFrequencySupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Frequency support forced by the actual leaf Fourier factor

  1. theorem OAI.Ostmann.archimedeanLeaf_frequency_le line 12
  2. theorem OAI.Ostmann.archimedeanLeaf_frequency_window line 35

    Source documentation

    The square-root margin in E_0 eventually covers the fixed Fourier support radius and all bounded errors in the leaf modulus.

    theorem archimedeanLeaf_frequency_window (C K : ℝ) :
    ∀ᶠ m : ℝ in atTop, ∀ X M s cutoff Δ : ℝ, ∀ ψhat : ℝ → ℂ,
      0 < X → 0 < M → M ≤ X * Real.exp (Δ + C) →
      (∀ t, ψhat t ≠ 0 → |t| ≤ Real.exp K) →
      archimedeanLeafFactor X M s cutoff ψhat ≠ 0 →
      |s| ≤ Real.exp (Δ + Real.sqrt m) := by
…

    Mentions: OAI.Ostmann.archimedeanLeafFactor