OAI/NumberTheory/Ostmann/Arithmetic/MovingSampleCoordinateLevels.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Tier separation for the original indexed sample tree

  1. theorem OAI.Ostmann.movingCompensationSlots_forall line 10
  2. theorem OAI.Ostmann.movingSampleCoordinates_levels line 28

    Source documentation

    The sample constructor itself enforces the required tier of every compensation occurrence. No assumption about an independently chosen tree is needed when the labels are the actual sample coordinates.

    theorem movingSampleCoordinates_levels {A : Type*} (tier : A → ℕ)
    (n : ℕ) (x : MovingSampleIndex n → A)
    (hx : ∀ i, tier (x i) = movingSampleTier i) :
    ((movingSampleCoordinates A n).symm x).Levels tier := by
…

    Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingSampleTier, OAI.Ostmann.movingSampleCoordinates

  3. def OAI.Ostmann.canonicalMovingSamples line 48
  4. theorem OAI.Ostmann.canonicalMovingSamples_levels line 51