OAI/NumberTheory/Ostmann/Arithmetic/MovingPeriodBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.CompensationBound line 10
2. def OAI.Ostmann.movingPeriodExponent line 17
3. theorem OAI.Ostmann.movingPeriodExponent_step line 19
4. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_denominator_bound line 29
5. theorem OAI.Ostmann.movingNode_residuePeriod_bound line 45
6. theorem OAI.Ostmann.MovingSlotData.formulaNodes_period_bound line 63

   Source documentation

   All repeated ancestor denominators are counted in this estimate; no squarefree simplification or independence of those factors is used.

   theorem MovingSlotData.formulaNodes_period_bound {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (L R : HistoryFormula Bool)
       (B d : ℕ) (hB : 1 ≤ B) (hfreq : T.Frequencies (fun s => s.natAbs ≤ B))
       (hcomp : T.CompensationBound value B)
       (hL : L.cleared.denominator.natAbs ≤ B ^ d) (hR : R.cleared.denominator.natAbs ≤ B ^ d) :
       movingArithmeticPeriod (T.formulaNodes value hvalue childBound pivotBound hf L R) ≤
         B ^ movingPeriodExponent n d := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.HistoryFormula, OAI.Ostmann.movingArithmeticPeriod, OAI.Ostmann.movingPeriodExponent

7. theorem OAI.Ostmann.movingTopPeriod_bound line 95