OAI/NumberTheory/Ostmann/Arithmetic/MovingSlotOccurrences.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.Ostmann.MovingSlotData line 12

   Source documentation

   At a node, the two regular lists exclude its moving giants. The compensation list is inserted in both children by the sampler.

   inductive MovingSlotData (σ : Type*) : ℕ → Type _
     | leaf (s : ℤ) (regular : List σ) : MovingSlotData σ 0
     | node {n : ℕ} (s : ℤ) (leftRegular rightRegular compensation : List σ)
         (left right : MovingSlotData σ n) : MovingSlotData σ (n + 1)

2. def OAI.Ostmann.MovingSlotData.frequency line 17
3. def OAI.Ostmann.MovingSlotData.step line 21
4. structure OAI.Ostmann.MovingSlotOccurrence line 31
5. def OAI.Ostmann.MovingSlotOccurrence.extend line 36
6. def OAI.Ostmann.MovingSlotData.occurrences line 42

   Source documentation

   Each root-to-occurrence path is recorded in the order of the cleared ancestor recursion, so the newest reversal occurs first.

   def MovingSlotData.occurrences {σ : Type*} : {n : ℕ} → MovingSlotData σ n → List (MovingSlotOccurrence σ)
     | _, .leaf _ _ => []
     | n + 1, .node s CL CR u left right =>
         ⟨n + 1, step s CL CR u left right false, []⟩ ::
           (left.occurrences.map (fun o => o.extend (step s CL CR u left right true))) ++
           (right.occurrences.map (fun o => o.extend (step s CL CR u left right false)))

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotOccurrence, OAI.Ostmann.MovingSlotData.step

7. def OAI.Ostmann.MovingSlotData.Levels line 49
8. def OAI.Ostmann.MovingSlotOccurrence.AvoidsBelow line 56
9. theorem OAI.Ostmann.MovingSlotData.occurrence_bounds line 67

   Source documentation

   The current compensation type is strictly below every variable in the current numerator and all its ancestor denominators. This holds for every occurrence simultaneously, including repeated occurrences of one sample.

   theorem MovingSlotData.occurrence_bounds {σ : Type*} (tier : σ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hT : T.Levels tier) :
       ∀ o ∈ T.occurrences, 0 < o.level ∧ o.level + o.path.length ≤ n ∧ o.AvoidsBelow tier := by
   …

   Mentions: OAI.Ostmann.MovingSlotData

10. theorem OAI.Ostmann.MovingSlotOccurrence.absent_of_level line 120