OAI/NumberTheory/Ostmann/Arithmetic/MovingOccurrenceRelabel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotOccurrence.map line 11
2. theorem OAI.Ostmann.MovingSlotOccurrence.map_extend line 15
3. theorem OAI.Ostmann.MovingSlotData.occurrences_map line 20
4. theorem OAI.Ostmann.movingPrimeLineSystem_iff line 32

   Source documentation

   The finite index of occurrences is only bookkeeping: the event itself is exactly the conjunction over the original compensation slots.

   theorem movingPrimeLineSystem_iff {σ : Type*} {n : ℕ}
       (value : σ → ℕ) (T : Bool → MovingSlotData σ n) (p : ℕ) (x y : ZMod p) :
       (∀ j : MovingPrimeOccurrences value T p,
         let L := movingPrimeOccurrenceLine value T p j
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPrimeOccurrences, OAI.Ostmann.movingPrimeOccurrenceLine

5. theorem OAI.Ostmann.movingSlotLine_natural_map line 53
6. theorem OAI.Ostmann.movingPrimeLineSystem_map line 67
7. theorem OAI.Ostmann.movingInternalBaseProbability_map line 95