OAI/Geometry/SingularHomology/MapHomology.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.Construction.rawClockFunction line 12
  2. def OAI.Problem340.Construction.rawPerturbation line 15
  3. def OAI.Problem340.Construction.rawRegisterFunction line 18
  4. theorem OAI.Problem340.Construction.rawMap_eq_rawUpdate_coefficients line 21
  5. theorem OAI.Problem340.Construction.continuous_rawMap_of_rawCoefficients line 25
  6. def OAI.Problem340.Construction.rawMapHomotopy line 30
  7. theorem OAI.Problem340.Construction.realHomologyMap_rawMap_eq_normalForm line 38
  8. theorem OAI.Problem340.Construction.rawMap_eigenvector_of_sphere line 45
  9. theorem OAI.Problem340.Construction.continuous_rawCoefficients line 54
  10. theorem OAI.Problem340.Construction.continuous_concrete_rawCoefficients line 85
  11. theorem OAI.Problem340.Construction.concreteMap_continuous_for_homotopy line 103
  12. def OAI.Problem340.Construction.concreteMapHomotopy line 108
  13. theorem OAI.Problem340.Construction.realHomologyMap_concreteMap_eq_normalForm line 115
  14. theorem OAI.Problem340.Construction.concreteMap_eigenvector_of_sphere line 121