OAI/NumberTheory/Ostmann/Arithmetic/MovingUnitPeriodBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Size of the full giant-unit period, including regular and outside slots

  1. def OAI.Ostmann.MovingSlotData.RegularBound line 12

    Source documentation

    Bounds the current regular product at every actual state of the tree.

    def MovingSlotData.RegularBound {σ : Type*} (value : σ → ℕ) (B : ℕ) :
    {n : ℕ} → MovingSlotData σ n → Prop
  | _, T@(.leaf _ _) => MovingSlotReversal.naturalProduct value T.regularSlots ≤ B
  | _, T@(.node _ _ _ _ left right) =>
      MovingSlotReversal.naturalProduct value T.regularSlots ≤ B ∧
        left.RegularBound value B ∧ right.RegularBound value B

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotReversal.naturalProduct

  2. def OAI.Ostmann.movingGiantUnitExponent line 19
  3. theorem OAI.Ostmann.MovingSlotData.frequencyProduct_bound line 23
  4. theorem OAI.Ostmann.MovingSlotData.frequencyProduct_ne_zero line 42
  5. theorem OAI.Ostmann.movingGiantUnitPeriod_ne_zero line 49
  6. theorem OAI.Ostmann.movingGiantUnitPeriod_bound line 69