OAI/NumberTheory/Ostmann/Construction/InitialAmplitudeReindex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Coordinate invariance of the actual initial prime amplitude

  1. theorem OAI.Ostmann.tupleGraphPhase_equiv line 11
  2. theorem OAI.Ostmann.sampledTuplePhase_equiv line 27
  3. theorem OAI.Ostmann.tupleFrequencies_equiv line 37
  4. theorem OAI.Ostmann.sampledTupleAmplitude_equiv line 48
  5. theorem OAI.Ostmann.prime_sample_pairwise_iff_injective line 67