OAI/NumberTheory/Ostmann/Arithmetic/MovingSupportCells.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingArithmeticPeriod line 10
2. def OAI.Ostmann.movingArithmeticRootCuts line 13
3. theorem OAI.Ostmann.movingArithmeticPeriod_pos line 17
4. theorem OAI.Ostmann.movingArithmeticPeriod_dvd line 27
5. theorem OAI.Ostmann.movingArithmeticRootCuts_mem line 31
6. theorem OAI.Ostmann.movingArithmeticRootCuts_card line 40

   Source documentation

   A concrete cardinality budget for the constructed root cuts.

   theorem movingArithmeticRootCuts_card (nodes : List MovingFormulaNode)
       (a : Bool → ℤ) (coord : Bool) :
       (movingArithmeticRootCuts nodes a coord).card ≤
         ∑ f ∈ nodes.toFinset, ∑ j : Fin 3, (f.guard.polynomials a coord j).natDegree := by
   …

   Mentions: OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingArithmeticRootCuts

7. theorem OAI.Ostmann.movingFormulaNodes_holds_invariant line 50

   Source documentation

   The complete node support is constant on the explicitly constructed root and residue cells. It is the actual arithmetic support, not an assumed regularity property of the coefficient.

   theorem movingFormulaNodes_holds_invariant (nodes : List MovingFormulaNode)
       (a : Bool → ℤ) (coord : Bool) (z w : ℤ)
       (hres : ∀ i, movingGiantUpdate a coord z i ≡ movingGiantUpdate a coord w i
         [ZMOD movingArithmeticPeriod nodes])
       (hcell : rootCellCode (movingArithmeticRootCuts nodes a coord) (z : ℝ) =
         rootCellCode (movingArithmeticRootCuts nodes a coord) (w : ℝ)) :
       (∀ f ∈ nodes, f.guard.ValidAt (movingGiantUpdate a coord z) ∧
         f.newGiant.IntegralAt (movingGiantUpdate a coord z)) ↔
       (∀ f ∈ nodes, f.guard.ValidAt (movingGiantUpdate a coord w) ∧
         f.newGiant.IntegralAt (movingGiantUpdate a coord w)) := by
   …

   Mentions: OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingGiantUpdate, OAI.Ostmann.movingArithmeticPeriod, OAI.Ostmann.rootCellCode, OAI.Ostmann.movingArithmeticRootCuts