OriginalPositiveFirstMoment.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

First moment of the original positive-frequency statistic

def OAI.Ostmann.originalPrimeProductStatistic line 16
theorem OAI.Ostmann.physical_positive_first_mean line 21

theorem OAI.Ostmann.exists_positive_first_mean line 62

Source documentation

The phase table in the first-moment bound is constructed by CRT and is indexed by products, so it is compatible with the fixed coefficient moments.

theorem exists_positive_first_mean (Q P : Finset ℕ)
    (hQ : ∀ p ∈ Q, p.Prime) (hP : ∀ p ∈ P, p.Prime) (hodd : ∀ p ∈ P, Odd p)
    (D : ∀ p : ℕ, Finset (ZMod p)) (ψ : 𝓢(ℝ, ℂ))
    (hreal : ∀ x, conj (ψ x) = ψ x) (hψ0 : ∀ x, 0 ≤ (ψ x).re)
    (X H : ℝ) (hX : 0 < X) (hH : 0 ≤ H)
    (ε : ℕ → ℝ) (hε : ∀ p ∈ P, ε p = 1 ∨ ε p = -1) (t : ℕ → ℤ)
    (k N : ℕ) (hk : 0 < k) (hkP : k ≤ P.card) (hK : 3000 ≤ (Q.card : ℝ))
    (hcop : ∀ M ∈ primeSubsetProducts P k, Q.toList.prod.Coprime M)
    (hcut : ∀ M ∈ primeSubsetProducts P k, H * ((M : ℝ) / X) * Q.toList.prod ≤ N)
    (hsupp : ∀ x : ℝ, H < x → 𝓕 ψ x = 0)
    (hlower : Real.sqrt X * Real.exp ((2 / 125 : ℝ) * Q.card) / 2 ≤
      ∑' n : ℤ, physicalWeight Q D ψ X n *
…

Mentions: OAI.Ostmann.primeSubsetProducts, OAI.Ostmann.physicalWeight

theorem OAI.Ostmann.eventual_original_positive_mean line 100

Source documentation

The original tail bias and size estimates now imply the Fourier first moment. There is no assumed Fourier lower bound in this statement.

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