OAI/NumberTheory/Ostmann/Arithmetic/MovingModularSpectator.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Spectator evaluation without internal primes in the period

At a spectator prime the entire reversal denominator is a unit. The field recursion therefore depends only on the two spectator residues, even though the original recursion used integer division by compensation products.

  1. def OAI.Ostmann.MovingSlotReversal.modularPivot line 15
  2. def OAI.Ostmann.MovingSlotData.ModularDenominators line 21
  3. theorem OAI.Ostmann.MovingSlotData.modularDenominators_of_units line 28
  4. theorem OAI.Ostmann.MovingSlotReversal.modularPivot_of_signedIntegral line 44
  5. def OAI.Ostmann.movingModularSpectator line 57
  6. theorem OAI.Ostmann.movingSignedSpectator_eq_modular line 67
  7. theorem OAI.Ostmann.movingModularSpectator_norm line 82