OAI/NumberTheory/Ostmann/Construction/ActualAmplitude.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Construction.FinitePrior.pair line 13
  2. theorem OAI.Ostmann.Construction.FinitePrior.pair_cmean line 22
  3. abbrev OAI.Ostmann.Construction.OuterSample line 28
  4. def OAI.Ostmann.Construction.outerPrior line 31
  5. def OAI.Ostmann.Construction.outerState line 35
  6. def OAI.Ostmann.Construction.spectatorPrior line 39
  7. def OAI.Ostmann.Construction.spectatorList line 42
  8. def OAI.Ostmann.Construction.actualCoefficient line 45
  9. def OAI.Ostmann.Construction.actualAmplitude line 52
  10. theorem OAI.Ostmann.Construction.outerState_giants_prime line 64
  11. theorem OAI.Ostmann.Construction.actualCoefficient_zero_frequency line 70