OAI/NumberTheory/Ostmann/Arithmetic/MovingSampleMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Evaluating the fixed indexed sample tree

This identifies the original sampled prime tree with evaluation of fixed slot data. Thus equality-pattern and polynomial arguments use the same literal constructor as the sampled coefficient.

  1. def OAI.Ostmann.MovingSampleSlots.map line 17
  2. theorem OAI.Ostmann.flattenMovingSlots_map line 23
  3. theorem OAI.Ostmann.appendMovingSlotLeaves_map line 31
  4. theorem OAI.Ostmann.movingCompensationSlots_map line 39
  5. theorem OAI.Ostmann.buildMovingSlotData_map line 47
  6. theorem OAI.Ostmann.movingSampleCoordinates_map line 59
  7. theorem OAI.Ostmann.canonicalMovingSamples_map line 72

    Source documentation

    All sampled values are the evaluation of one fixed indexed tree.

    theorem canonicalMovingSamples_map {A : Type*} (n : ℕ) (x : MovingSampleIndex n → A) :
    (canonicalMovingSamples n).map x = (movingSampleCoordinates A n).symm x := by
…

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