MovingSpectatorRangeUnits.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual separated prime ranges imply all spectator unit tests

theorem OAI.Ostmann.prime_cast_ne_zero_of_lt line 14

theorem OAI.Ostmann.movingPattern_spectator_units_of_ranges line 23

Source documentation

The spectator primes are far smaller than every original nongiant prime. This supplies the small-word and internal-sample unit tests for each pattern without any restriction on their actual residue values.

theorem movingPattern_spectator_units_of_ranges {B C : Type*} {N n m : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (small : Bool → TreeLeafTuple (List B) n)
    (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (hsmall : ∀ b, ∀ j ∈ flattenMovingSlots n (small b), j ∉ Set.range slot)
    (base : Fin (N + 1) → ℕ)
    (hbase : ∀ i ∉ Set.range (movingPatternBulkEmbedding e slot), (base i).Prime)
    (L : ℝ) (hL : 0 < L) (p : Fin m → ℕ) [∀ i, Fact (p i).Prime]
    (hp : ∀ i, (p i : ℝ) ≤ Real.exp (Real.exp ((1 / 1000 : ℝ) * L)))
    (hlarge : ∀ j, j ∉ Set.range (movingPatternBulkEmbedding e slot) →
      Real.exp (Real.exp ((39 / 10000 : ℝ) * L)) ≤ (base j : ℝ)) :
    (∀ i b, ∀ j ∈ flattenMovingSlots n (small b),
      (base (e.symm (.inl j)) : ZMod (p i)) ≠ 0) ∧
…

Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingPatternBulkEmbedding

theorem OAI.Ostmann.moving_spectator_frequency_range line 55
Source documentation
The original finite Fourier cutoff lies below every selected spectator prime, uniformly in the linear bulk length.
```
theorem moving_spectator_frequency_range (k : ℕ) (A a : ℝ)
    (hA : 0 ≤ A) (ha : 0 < a) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount