OAI/NumberTheory/Ostmann/Construction/ScheduledFrequencyHistory.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite frequency histories with the actual cutoff at every level

  1. def OAI.Ostmann.ScheduledFrequencyIndex line 11
  2. instance OAI.Ostmann.scheduledFrequencyIndexFintype line 16
  3. def OAI.Ostmann.scheduledFrequencyHistory line 25
  4. theorem OAI.Ostmann.scheduledFrequencyHistory_succ line 30
  5. theorem OAI.Ostmann.scheduledFrequencyHistory_root_bound line 34
  6. theorem OAI.Ostmann.scheduledFrequencyHistory_all_bound line 42

    Source documentation

    The largest level cutoff controls every actual child frequency.

    theorem scheduledFrequencyHistory_all_bound (V : ℕ → ℕ) (hV : Monotone V) (n : ℕ)
    (a : ScheduledFrequencyIndex V n) (s : ℤ)
    (hs : s ∈ allFrequencyList n (scheduledFrequencyHistory V n a)) : s.natAbs ≤ V n := by
…

    Mentions: OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.allFrequencyList, OAI.Ostmann.scheduledFrequencyHistory

  7. theorem OAI.Ostmann.scheduledFrequencyHistory_injective line 58