HarmonicHistoryRates.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The single-history arithmetic rate under the actual prime priors

theorem OAI.Ostmann.harmonic_history_support_rate line 15

Source documentation

All growth and normalization hypotheses refer to the original prime sets. The only arithmetic input is the proved bound for divisors.

theorem harmonic_history_support_rate (n : ℕ) (K C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
    ∀ᶠ m : ℝ in atTop, ∀ N V : ℕ, ∀ Δ : ℝ, ∀ P : Finset ℕ, ∀ S : Finset ℤ,
      (N : ℝ) ≤ Real.exp (C * m) →
      (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m) →
      (∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N) →
      ∀ Q : FrequencyTree S n → ℕ, ∀ [_hQ : ∀ t, NeZero (Q t)],
      ∀ T : TreeLeafIndex n → Finset ℕ, ∀ h J : TreeLeafIndex n → ℕ,
      ∀ hunit : ∀ t, ∀ p : P, (p : ℕ).Coprime (Q t),
      (∀ t i, Q t ≤ 2 ^ h i) →
      (∀ i p, p ∈ T i → 2 ^ h i ≤ p ∧ p < 2 ^ (h i + J i)) →
      ∀ a C₁ L : ℝ, 0 < a → 1 ≤ L →
      (∀ i, a ≤ ∑ p ∈ T i, (p : ℝ)⁻¹) →
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafIndex