TableSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.IncidenceTemplate.exists_tables_of_estimate line 22

Source documentation

Finite simultaneous selection from the source's independent master arrays and six-letter array. Its hypothesis is an explicit numerical upper bound, which tends to zero; it assumes no good table or coupling.

theorem exists_tables_of_estimate (T : J → ConditionalTest) {α β δ ε τ : ℝ}
    (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ)
    (hsmall : ∀ j, ((T j).k+1:ℝ)*(β+90*δ) ≤ 1/2)
    (hN : ∀ j, (T j).threshold ≤ Fintype.card A)
    (hε0 : 0 < ε) (hε1 : ε < 1) (hτ0 : 0 < τ) (hτ2 : τ ≤ 2)
    (hest : (∑ j, (T j).rate (Fintype.card A)) +
      ε*(60*(Fintype.card A:ℝ)^2*Real.exp (-τ^2*(Fintype.card A:ℝ)^(1-δ)/4)) < ε) :
    ∃ (w : TableModel.Entry (A := A) rowSupport → Bool) (d : (Fin 6 → A) → Bool),
…

Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest, OAI.HyperbolicObstruction.TableModel.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport

abbrev OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet line 58
Source documentation
The alphabet of rank n+1, including each generator and its formal inverse. This is an arbitrarily large cofinal set of the literal source alphabets.
```
abbrev SymmetricAlphabet (n : ℕ) := Fin (n+1) × Bool
```
lemma OAI.HyperbolicObstruction.IncidenceTemplate.card_symmetricAlphabet line 60
lemma OAI.HyperbolicObstruction.IncidenceTemplate.alphabet_size_tendsto line 63
theorem OAI.HyperbolicObstruction.IncidenceTemplate.eventually_exists_tables line 72
Source documentation
Every finite set of literal conditional tests is simultaneously realizable with small errors on arbitrarily large source alphabets. Parameters are fixed first; the actual table is chosen only after N is large.
```
theorem eventually_exists_tables (T : J → ConditionalTest) {α β δ ε τ : ℝ}
    (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ) (hd1 : δ < 1)
    (hsmall : ∀ j, ((T j).k+1:ℝ)*(β+90*δ) ≤ 1/2)
    (hε0 : 0 < ε) (hε1 : ε < 1) (hτ0 : 0 < τ) (hτ2 : τ ≤ 2) :
    ∀ᶠ n in atTop, ∃ (w : TableModel.Entry (A := SymmetricAlphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest, OAI.HyperbolicObstruction.TableModel.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport