CharacterSelectionRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One endpoint family has common anchors and common target-cell lists

theorem OAI.Ostmann.eventual_common_character_selection line 13

Source documentation

The word bin has already been fixed. We fix the anchors and then the actual shell/list data without changing it, retaining an explicit rate.

theorem eventual_common_character_selection (k N : ℕ) (C z : ℝ)
    (hC : 0 ≤ C) (hz : 1 ≤ z) (hsize : (N + (k + 1) + (k + 1) : ℕ) ≤ z) :
    ∀ᶠ L : ℝ in atTop, ∀ (B : ℕ) (m X A : ℝ),
      (B + 1 : ℕ) ≤ Real.exp (C * L) → z * L ≤ 2 * m →
      ∀ (E : Finset ℕ), E.Nonempty → Real.sqrt X * Real.exp (-A * m) ≤ E.card →
      ∀ (P : Finset ℕ) (F : ℕ → ℕ → ℂ) (c δ U : ℝ)
        (anchor : ℕ → (Fin k × Bool) → ℕ) (T : ℕ → Option (Fin k) → ℝ)
        (w : ∀ a j, CharacterTargetWord P (F a) c δ U k (T a j)),
      0 < c → 0 < δ → 5 * k ≤ B → (∀ p ∈ P, primeLogIndex p ≤ B) →
      (∀ a ∈ E, ∀ j, anchor a j ≤ B) →
      (∀ a ∈ E, (∑ j : Option (Fin k), (w a j).indices.length) ≤ N) →
      ∃ a₀ ∈ E, ∃ S : Finset ℕ, S ⊆ E ∧ S.Nonempty ∧
…

Mentions: OAI.Ostmann.CharacterTargetWord, OAI.Ostmann.primeLogIndex