OAI/NumberTheory/Ostmann/Arithmetic/MovingIndexedLineSystem.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite index for every representative's actual line system

  1. abbrev OAI.Ostmann.MovingPairOccurrenceIndex line 11
  2. theorem OAI.Ostmann.movingPairOccurrenceIndex_card line 14
  3. def OAI.Ostmann.movingRepresentativeIndex line 23

    Source documentation

    Indices outside a representative's system repeat its selected base row. Thus every representative uses the same finite index without changing any test.

    noncomputable def movingRepresentativeIndex {σ : Type*} {n : ℕ}
    (T : Bool → MovingSlotData σ n) (rep : σ) (base : MovingPairRepresentativeOccurrences T rep)
    (o : MovingPairOccurrenceIndex T) : MovingPairRepresentativeOccurrences T rep :=
…

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPairRepresentativeOccurrences, OAI.Ostmann.MovingPairOccurrenceIndex

  4. theorem OAI.Ostmann.movingRepresentativeIndex_surjective line 29
  5. def OAI.Ostmann.movingIndexedOccurrence line 36
  6. def OAI.Ostmann.movingIndexedLine line 42
  7. theorem OAI.Ostmann.movingIndexedOccurrence_absent line 48
  8. theorem OAI.Ostmann.movingIndexedOccurrence_path_length line 62
  9. theorem OAI.Ostmann.movingIndexedOccurrence_units line 71
  10. theorem OAI.Ostmann.movingIndexedOccurrence_size line 90
  11. theorem OAI.Ostmann.movingInternalBaseProbability_indexed line 105