CharacterInitialRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed character priors give a uniform initial amplitude

theorem OAI.Ostmann.eventual_character_initial_rate line 14

Source documentation

The exponent depends on the endpoint and word rates, but not on the number of selected nonword cells. That number only changes the threshold.

theorem eventual_character_initial_rate (k nc : ℕ)
    (a b z Cmass Ctotal Aend Bword B_D c s γ : ℝ)
    (ha : 0 < a) (hb : 0 < b) (hz : 1 ≤ z)
    (hCmass : 0 ≤ Cmass) (hCtotal : 0 ≤ Ctotal) (hc : 1 ≤ c)
    (hs : 0 < s) (hγ : 0 < γ) (hbudget : 4 * nc * Cmass ≤ z)
    (hgap : 2 * ((2 * Real.log (3 / a) + 3 + 2 * Ctotal) +
      (Aend + 2 * Bword + 1) + 2) ≤ B_D) (ψ : 𝓢(ℝ, ℂ)) :
    ∀ᶠ m : ℕ in atTop, ∀ (r : Fin k → ℕ) (f : ℕ)
      (cell : (Σ v, Fin (characterCellSize r f v)) ≃ Fin nc)
      (L logX τ : ℝ), 0 < L → (m : ℝ) ≤ z * L → z * L ≤ 2 * m →
      ∀ (P B T₀ : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
      (Q : Fin (m + 1) → Finset ℕ) (R : Fin nc → Finset ℕ),
…

Mentions: OAI.Ostmann.characterCellSize