UniformSupportedInitialAmplitude.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform exponential lower bound for the actual mixed initial amplitude

theorem OAI.Ostmann.uniform_supported_initial_amplitude line 13

Source documentation

The cell count affects the threshold but not the final exponential rate. All product restrictions are imposed only on the live original prior.

theorem uniform_supported_initial_amplitude (r : ℕ) (z A B Bs a c δ : ℝ)
    (hz : 1 ≤ z) (ha : 0 < a) (hc : 0 < c) (hδ : 0 < δ)
    (hBs : 2 * (A + B + 2 * Real.log 4 +
      (4 * (Real.log 2 + 2) + 2 * Real.log 2 + 4) + 3) ≤ Bs)
    (ψ : 𝓢(ℝ, ℂ)) (T : ℝ)
    (hψ : ∀ x, 0 ≤ (ψ x).re) (hsupp : ∀ t : ℝ, T < |t| → 𝓕 ψ t = 0) :
    ∀ᶠ m : ℕ in atTop, ∀ (L Y X Δ R : ℝ),
      0 < L → L ≤ m → (m : ℝ) ≤ z * L →
      0 < Y → Y ≤ Real.exp L → 0 < X → 0 < R →
      (Bs + 8 * Real.log z) * m ≤ Δ →
      ∀ (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (_hP : ∀ q ∈ P, q.Prime),
      ∀ (S : (q : P) → Finset (ZMod (q : ℕ))) (favorable : P → Bool)
…