OAI/NumberTheory/Ostmann/Arithmetic/MovingPairedLogSlots.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic factors indexed by the actual terminal leaves

  1. def OAI.Ostmann.movingPairedLogSlots line 10
  2. theorem OAI.Ostmann.movingPairedLogSlots_count line 17
  3. theorem OAI.Ostmann.movingPairedLogSlots_length_le line 26

    Source documentation

    The concrete terminal groups satisfy exactly the length hypothesis of the weighted Page comparison. No bound on a fictitious common grouping is used.

    theorem movingPairedLogSlots_length_le {σ : Type*} (tier : σ → ℕ) (k : ℕ)
    {n : ℕ} (T : Bool → MovingSlotData σ n) (r : ℕ)
    (hT : ∀ b, (T b).RegularLengthLE r) :
    ∀ j, (movingPairedLogSlots tier k T j).length ≤ r := by
…

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingPairedLogSlots