OAI/NumberTheory/Ostmann/Arithmetic/MovingOccurrenceIntegrality.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSlotNaturalPath_append line 10
2. theorem OAI.Ostmann.movingSlotPathIntegral_append line 18
3. theorem OAI.Ostmann.MovingSlotData.occurrence_integral line 31

   Source documentation

   The integral support at a tree yields all the local integer equalities used in the polynomial line interpretation. This is constructive for every listed occurrence, including both child orders.

   theorem MovingSlotData.occurrence_integral {σ : Type*} (value : σ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (XL XR : ℕ) (hT : T.Integral value XL XR) :
       ∀ o ∈ T.occurrences,
         MovingSlotPathIntegral value o.path (XL, XR) ∧
         o.current.IntegralAt value (movingSlotNaturalPath value o.path (XL, XR)) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotPathIntegral, OAI.Ostmann.movingSlotNaturalPath

4. theorem OAI.Ostmann.buildMovingSlotData_occurrence_integral line 71