OAI/Dynamics/EntropyCounterexample/AmbientRetraction.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.AmbientRetraction.normalize line 13
  2. theorem OAI.Problem340.AmbientRetraction.contDiffAt_normalize line 15
  3. theorem OAI.Problem340.AmbientRetraction.normalize_mem_sphere line 19
  4. theorem OAI.Problem340.AmbientRetraction.normalize_eq_self line 24
  5. theorem OAI.Problem340.AmbientRetraction.norm_smul_normalize line 29
  6. theorem OAI.Problem340.AmbientRetraction.norm_normalize_le_one line 34
  7. theorem OAI.Problem340.AmbientRetraction.norm_normalize_sub_le line 39
  8. theorem OAI.Problem340.AmbientRetraction.norm_fderiv_normalize_le line 64
  9. theorem OAI.Problem340.AmbientRetraction.norm_fderiv_normalize_le_four line 69
  10. def OAI.Problem340.AmbientRetraction.cylinder line 76
  11. theorem OAI.Problem340.AmbientRetraction.contDiffAt_cylinder line 78
  12. theorem OAI.Problem340.AmbientRetraction.norm_cylinder_sub_le_four line 82
  13. theorem OAI.Problem340.AmbientRetraction.norm_fderiv_cylinder_le_four line 97
  14. theorem OAI.Problem340.AmbientRetraction.cylinder_eq_self line 103
  15. def OAI.Problem340.AmbientRetraction.cylinderDomain line 108
  16. theorem OAI.Problem340.AmbientRetraction.isOpen_cylinderDomain line 111
  17. theorem OAI.Problem340.AmbientRetraction.mapsTo_normalizedPredictor line 114
  18. theorem OAI.Problem340.AmbientRetraction.contDiffOn_normalizedPredictor line 127
  19. theorem OAI.Problem340.AmbientRetraction.norm_fderiv_normalizedPredictor_le line 136
  20. theorem OAI.Problem340.AmbientRetraction.normalizedPredictor_iterate_eq line 152
  21. theorem OAI.Problem340.AmbientRetraction.normalizedPredictor_iterate_succ_eq line 165
  22. def OAI.Problem340.AmbientRetraction.domain line 175
  23. theorem OAI.Problem340.AmbientRetraction.isOpen_domain line 178
  24. theorem OAI.Problem340.AmbientRetraction.standardEmbedding_mem_domain line 187
  25. def OAI.Problem340.AmbientRetraction.project line 191
  26. theorem OAI.Problem340.AmbientRetraction.contDiffOn_project line 194
  27. theorem OAI.Problem340.AmbientRetraction.project_standardEmbedding line 208
  28. def OAI.Problem340.AmbientRetraction.toManifold line 215
  29. theorem OAI.Problem340.AmbientRetraction.standardEmbedding_toManifold line 220
  30. theorem OAI.Problem340.AmbientRetraction.continuous_toManifold line 223
  31. theorem OAI.Problem340.AmbientRetraction.toManifold_standardEmbedding line 228
  32. def OAI.Problem340.AmbientRetraction.fromAmbient line 233
  33. theorem OAI.Problem340.AmbientRetraction.standardEmbedding_fromAmbient line 239
  34. theorem OAI.Problem340.AmbientRetraction.isC1SelfMap_fromAmbient line 246