OAI/NumberTheory/Ostmann/Construction/InitialEtaDefs.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Construction.InitialEta.HalfPosition line 12
  2. abbrev OAI.Ostmann.Construction.InitialEta.Position line 13
  3. abbrev OAI.Ostmann.Construction.InitialEta.JointSample line 14
  4. def OAI.Ostmann.Construction.InitialEta.halfAt line 18
  5. def OAI.Ostmann.Construction.InitialEta.halfSource line 23
  6. def OAI.Ostmann.Construction.InitialEta.tupleSource line 30
  7. def OAI.Ostmann.Construction.InitialEta.halfSample line 34
  8. def OAI.Ostmann.Construction.InitialEta.tupleSample line 43
  9. def OAI.Ostmann.Construction.InitialEta.tupleValues line 48
  10. def OAI.Ostmann.Construction.InitialEta.jointPrior line 53
  11. def OAI.Ostmann.Construction.InitialEta.tupleEquiv line 58
  12. theorem OAI.Ostmann.Construction.InitialEta.tupleValues_prime line 74
  13. theorem OAI.Ostmann.Construction.InitialEta.card_position line 80
  14. def OAI.Ostmann.Construction.InitialEta.tuplePhysical line 86
  15. def OAI.Ostmann.Construction.InitialEta.repeatedContribution line 94
  16. def OAI.Ostmann.Construction.InitialEta.distinctContribution line 102