OriginalLiftProbability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A positive family of simultaneous lifts from the original tail data

theorem OAI.Ostmann.eventual_original_lift_probability line 16

Source documentation

This combines the physical amplification, Poisson, fixed-family moments, and inverse phase argument. No Fourier moment or witness event is assumed.

theorem eventual_original_lift_probability (hBonami : PublishedBonamiBound)
    (cψ a c C B : ℝ) (hcψ : 0 < cψ) (ha : 0 < a) (hc : 0 < c)
    (hC : 500 ≤ C) (hB : 3 ≤ B) (ψ : 𝓢(ℝ, ℂ))
    (hreal : ∀ x, conj (ψ x) = ψ x) (hψ0 : ∀ x, 0 ≤ (ψ x).re)
    (hψ1 : ∀ x ∈ Set.Icc (0 : ℝ) 1, cψ ≤ (ψ x).re)
    (hsupp : ∀ x : ℝ, B ^ 2 < |x| → 𝓕 ψ x = 0) (hCψ : (𝓕 ψ 0).re ≤ C) :
    ∀ᶠ T : ℝ in atTop, ∀ (Q P : Finset ℕ) (_hQ : ∀ p ∈ Q, p.Prime),
      (∀ p ∈ P, p.Prime) → (∀ p ∈ P, Odd p) →
      ∀ (D : ∀ p : ℕ, Finset (ZMod p)) (X : ℝ),
      0 < X → B ^ 2 < X / Q.toList.prod →
      ∀ (S : Finset ℤ), (∀ n ∈ S, 0 ≤ (n : ℝ) ∧ (n : ℝ) ≤ X) →
      a * Real.sqrt X / T ^ 6 ≤ (S.card : ℝ) →
…

Mentions: OAI.Ostmann.PublishedBonamiBound