AmplifiedRepeatRemoval.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Retaining the amplified moment after deleting all repeated primes

theorem OAI.Ostmann.repeat_squared_budget line 12

theorem OAI.Ostmann.eventual_amplified_repeat_removal line 48

Source documentation

The actual ternary distinct-prime moment retains at least half of its positive amplified moment, uniformly for sufficiently large T.

theorem eventual_amplified_repeat_removal (C : ℝ) (hC : 1 ≤ C) :
    ∀ᶠ T : ℝ in atTop, ∀ {ι A : Type} [Fintype A] [DecidableEq A]
      (w : ι → ℝ) (y : ι → A → ℝ) (k : ℕ) (K X : ℝ),
      (∀ i, 0 ≤ w i) → (∀ i a, y i a = 0 ∨ y i a = 1 ∨ y i a = -1) →
      Summable w → 0 < k → Even k → k ≤ Fintype.card A →
      (k : ℝ) ≤ 2 * T ^ (3 / 5 : ℝ) →
      T ^ (9999999 / 10000000 : ℝ) / 1000 ≤ K → 0 < X →
      Real.exp T ≤ C * T * Fintype.card A → X ≤ Real.exp ((k : ℝ) * T) →
      (∑' i, w i) ≤ C * X →
      Real.sqrt X * Real.exp ((2 / 125 : ℝ) * K) ≤
        (∑' i, w i * ternaryMean (y i) ^ k) →
      (∑' i, w i * ternaryMean (y i) ^ k) / 2 ≤
…

Mentions: OAI.Ostmann.ternaryMean