RangedPairAdmissibility.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual periods and frequencies fit below the separated prime scales

theorem OAI.Ostmann.eventual_word_pair_admissible line 12

Source documentation

A fixed-depth polynomial period is below the long-prime cutoff. Every actual frequency is also below the smallest retained prime.

theorem eventual_word_pair_admissible (n : ℕ) (b C z α β c : ℝ)
    (hb : 0 ≤ b) (hC : 0 ≤ C) (hz : 0 ≤ z) (hα : 0 < α)
    (hαβ : α < β) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ (t t' : FrequencyTree ℤ n)
      (B V A : ℕ) (lower m : ℝ),
      0 ≤ m → m ≤ z * L → (B : ℝ) ≤ b * (1 + m) →
      (V : ℝ) ≤ Real.exp (C * (1 + m)) →
      (∀ s ∈ allFrequencyList n t, s.natAbs ≤ V) →
      (∀ s ∈ allFrequencyList n t', s.natAbs ≤ V) →
      Real.exp (c * Real.exp (α * L)) ≤ lower →
      Real.exp (Real.exp (β * L)) ≤ (A : ℝ) →
      wordTransferFullPeriod n t B * wordTransferFullPeriod n t' B ≤ A ∧
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.allFrequencyList, OAI.Ostmann.wordTransferFullPeriod