OAI/NumberTheory/Ostmann/Construction/FixedCharacterPriors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_fixed_character_priors line 14

   Source documentation

   Fixing the actual anchor and whole-shell codes leaves a single collection of harmonic probability laws. Every retained endpoint has a large mean under these same laws, with the explicit selection cost from the code count.

   theorem eventual_fixed_character_priors (c δ β C z : ℝ) (k : ℕ)
       (hc : 0 < c) (hδ : 0 < δ) (hC : 0 ≤ C) (hz : 1 ≤ z)
       (hsize : ((characterTargetLabelBound c δ k + (k + 1) + (k + 1) : ℕ) : ℝ) ≤ z) :
       ∀ᶠ L : ℝ in atTop, ∀ (B : ℕ) (m X A U : ℝ),
         (B + 1 : ℕ) ≤ Real.exp (C * L) → z * L ≤ 2 * m → U ≤ β * L →
         ∀ (E : Finset ℕ), E.Nonempty → Real.sqrt X * Real.exp (-A * m) ≤ E.card →
         ∀ (P : Finset ℕ) (G : ℕ → ℕ → ℂ) (ζ : ℂ), ‖ζ‖ = 1 →
         5 * k ≤ B → (∀ p ∈ P, primeLogIndex p ≤ B) →
         ∀ (u : Fin k × Bool → ℝ), (∀ j, u j ≤ β * L) →
         ∀ (a : ∀ x j, CharacterAnchorCell P (fun p => ζ * G x p) c δ (u j)),
         (∀ x ∈ E, ∀ j, (a x j).index ≤ B) →
         ∀ (T : ℕ → Option (Fin k) → ℝ)
   …

   Mentions: OAI.Ostmann.characterTargetLabelBound, OAI.Ostmann.primeLogIndex, OAI.Ostmann.CharacterAnchorCell