CommonCenterDiscard.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Numerical cost of discarding small common centers

theorem OAI.Ostmann.liftMomentUpper_le_scaled line 14

Source documentation

The original interval length and prime lower bound control the lower factorial moment, with only an exponential-in-the-tuple-length loss.

theorem liftMomentUpper_le_scaled (T : ℝ) (J r H Z : ℕ)
    (hT : 0 ≤ T)
    (hZ : Real.exp T / 2 ≤ (Z : ℝ))
    (hH : (H : ℝ) ≤ 2 * Real.exp ((r - 10 : ℕ) * T + T / 5)) :
    liftMomentUpper J (r - 10) H Z ≤
      6 * (2 : ℝ) ^ r * Real.exp (T / 5) * (J : ℝ) ^ (r - 10) := by
…

Mentions: OAI.Ostmann.liftMomentUpper

theorem OAI.Ostmann.eventual_commonCenter_population_budget line 53

Source documentation

The cost of ten missing prime factors dominates the tuple and logarithmic losses at the manuscript's population scale.

theorem eventual_commonCenter_population_budget (Cpop : ℝ) (hCpop : 500 ≤ Cpop) :
    ∀ᶠ T : ℝ in atTop, ∀ (J r : ℕ),
      Real.exp T ≤ Cpop * T * J → (2 : ℝ) ^ r ≤ Real.exp (T / 10) →
      48 * (2 : ℝ) ^ r * Real.exp (33 * T / 5) ≤ (J : ℝ) ^ 10 := by
…

theorem OAI.Ostmann.eventual_commonCenter_discard_budget line 82