OAI/NumberTheory/Ostmann/Construction/InitialEtaPhysical.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Construction.InitialEta.tupleLocalTest line 11
  2. def OAI.Ostmann.Construction.InitialEta.halfBins line 17
  3. def OAI.Ostmann.Construction.InitialEta.tupleBins line 23
  4. theorem OAI.Ostmann.Construction.InitialEta.halfBins_nonneg line 28
  5. theorem OAI.Ostmann.Construction.InitialEta.halfBins_le_one line 33
  6. theorem OAI.Ostmann.Construction.InitialEta.tupleBins_nonneg line 39
  7. theorem OAI.Ostmann.Construction.InitialEta.tupleBins_le_one line 44
  8. theorem OAI.Ostmann.Construction.InitialEta.residueTest_ofReal_re line 50
  9. theorem OAI.Ostmann.Construction.InitialEta.favorableTest_ofReal_re line 57
  10. theorem OAI.Ostmann.Construction.InitialEta.tupleValues_giant line 68
  11. theorem OAI.Ostmann.Construction.InitialEta.tupleValues_bulk line 73
  12. theorem OAI.Ostmann.Construction.InitialEta.tupleValues_spectator line 78
  13. theorem OAI.Ostmann.Construction.InitialEta.tupleValues_aux line 83
  14. theorem OAI.Ostmann.Construction.InitialEta.tupleTest_eq line 88
  15. theorem OAI.Ostmann.Construction.InitialEta.tuplePhysical_eq line 111