OAI/NumberTheory/Ostmann/Arithmetic/MovingTopCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.MovingSlotData.formulaNodes_frequencies line 10
2. def OAI.Ostmann.topGiantInput line 26
3. def OAI.Ostmann.movingTopPeriod line 29

   Source documentation

   The period depends only on the fixed small data and frequencies.

   noncomputable def movingTopPeriod {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) : ℕ :=
   …

   Mentions: OAI.Ostmann.MovingSlotData

4. theorem OAI.Ostmann.movingTopPeriod_pos line 34
5. def OAI.Ostmann.movingTopRootCuts line 40
6. theorem OAI.Ostmann.moving_top_support_cells line 49

   Source documentation

   With the other giant fixed, the original arithmetic support is constant on the constructed residue and root cells. This also covers empty depth.

   theorem moving_top_support_cells {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XL YL XR : ℕ)
       (hres : (XL : ℤ) ≡ (YL : ℤ) [ZMOD movingTopPeriod value hvalue childBound pivotBound T hf])
       (hcell : rootCellCode (movingTopRootCuts value hvalue childBound pivotBound T hf XR) (XL : ℝ) =
         rootCellCode (movingTopRootCuts value hvalue childBound pivotBound T hf XR) (YL : ℝ)) :
       T.ArithmeticSupport value childBound pivotBound XL XR ↔
         T.ArithmeticSupport value childBound pivotBound YL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingTopPeriod, OAI.Ostmann.rootCellCode, OAI.Ostmann.movingTopRootCuts