OAI/NumberTheory/Ostmann/Arithmetic/MovingSampleIntegrality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.MovingGiantTree.castConstant_integral line 10
2. def OAI.Ostmann.MovingSlotData.Integral line 18

   Source documentation

   The labelled history is interpreted by the same positive integer pivots as the original sampler. No primality is imposed on a reconstructed giant.

   def MovingSlotData.Integral {σ : Type*} (value : σ → ℕ) :
       {n : ℕ} → MovingSlotData σ n → ℕ → ℕ → Prop
     | _, .leaf _ _, _, _ => True
     | _, .node s CL CR u left right, XL, XR =>
         let step := MovingSlotData.step s CL CR u left right false
   …

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

3. theorem OAI.Ostmann.buildMovingSlotData_integral line 26