OAI/Geometry/BallPacking/DiskMaps/FlatIsotopy.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.flat_isotopy_stationary line 19
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_flat_embedding_extension line 35
  3. structure OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy line 72
  4. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.refl line 84
  5. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.trans line 94
  6. def OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.symm line 108
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.mapsTo line 121
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.SupportedSmoothIsotopy.mapsTo_compl line 129
  9. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothlyAmbientRelated line 136
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothlyAmbientRelated.refl line 140
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothlyAmbientRelated.trans line 143
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothlyAmbientRelated.symm line 153
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothlyAmbientRelated.mono line 161
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothlyAmbientRelated_of_path line 170
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.parametric_flat_isotopy_stationary line 189
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_flat_embedding_extension line 211
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiff_fixed_integral line 255
  18. def OAI.PackingSufficiencySupport.Hamiltonian.smoothBlowup line 276
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothBlowup_contDiff line 279
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothBlowup_zero line 288
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.smul_smoothBlowup line 293
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothBlowup_eq line 308
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothBlowup_injOn line 313
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothBlowup_hasFDerivAt line 326
  25. def OAI.PackingSufficiencySupport.Hamiltonian.complexPair line 347
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPair_apply line 350
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.realLinear_complex_decomposition line 352
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.complex_decomposition_orientation line 362
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.complexPair_invertible line 369
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_positive_complex_linear_path line 383
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_small_positive_perturbation line 437