OAI/NumberTheory/Ostmann/Construction/RemainingRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Construction.RemainingSample line 13
  2. def OAI.Ostmann.Construction.remainingPrior line 16
  3. def OAI.Ostmann.Construction.remainingState line 19
  4. def OAI.Ostmann.Construction.remainingProduct line 25
  5. def OAI.Ostmann.Construction.remainingIntegrand line 28
  6. def OAI.Ostmann.Construction.remainingRow line 42
  7. theorem OAI.Ostmann.Construction.remainingRow_pairing line 54