UniformInitialAmplitude.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform lower bound for the actual initial graph amplitude

theorem OAI.Ostmann.uniform_initial_amplitude line 16

Source documentation

All hypotheses here concern the selected prime sets, their ordinary harmonic masses, the tested endpoints and the sampled product window. The conclusion is the manuscript's level-zero amplitude, with a rate independent of the gap and of the number of fixed cell roles.

theorem uniform_initial_amplitude (r : ℕ) (a b z A C c₀ δ γ Aₑ Bₑ B_D E₀ H : ℝ)
    (ha : 0 < a) (hb : 0 < b) (hz : 1 ≤ z) (hA : 0 ≤ A) (hC : 0 ≤ C)
    (hc₀ : 0 < c₀) (hδ : 0 < δ) (hγ : 0 < γ) (hAₑ : 0 ≤ Aₑ) (hBₑ : 0 ≤ Bₑ)
    (hroles : 4 * r * A ≤ z)
    (hgap : 2 * ((2 * Real.log (3 / a) + 3 + 2 * C) +
      (2 * (Aₑ + 3 * Bₑ) - 2 * Real.log δ + 1) + 2) ≤ B_D)
    (hH : 0 ≤ H) (ψ : 𝓢(ℝ, ℂ))
    (hψ : ∀ x, 0 ≤ (ψ x).re) (hψreal : ∀ x, (ψ x).im = 0)
    (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
    ∀ᶠ m : ℕ in atTop, ∀ (L X J : ℝ), 0 < L → 0 < X →
      (m : ℝ) ≤ z * L → z * L ≤ 2 * m → J ≤ A * L →
      ∀ (P U T : Finset ℕ) (R : Fin r → Finset ℕ) (hP : ∀ p ∈ P, p.Prime),
…