OAI/Geometry/BallPacking/Hamiltonian/ScaledPlanarMotion.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarHamiltonianField_smul line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaled_planar_fderiv line 19
  3. def OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarHamiltonian line 33
  4. def OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarTrace line 38
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarHamiltonian_smooth line 42
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarHamiltonian_compact line 55
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarTrace_continuous line 77
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarTrace_zero line 86
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarTrace_flow line 92
  10. def OAI.PackingSufficiencySupport.Hamiltonian.PlanarHamiltonianMotion.scaled line 111
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialArea_smul line 126
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarTrace_smooth line 131
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarTrace_cutoff_zero line 141
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaledPlanarTrace_time_one line 147
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaled_disk_fixed line 152
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaled_disk_mapsTo line 164
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.scaled_disk_preserves_slice line 179
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.HamiltonianDiskIsotopyFamily.exists_support_margin line 189
  19. theorem OAI.PackingSufficiencySupport.Comparison.exists_longer_strict_interval line 210
  20. def OAI.PackingSufficiencySupport.Comparison.IntervalRoom line 243
  21. theorem OAI.PackingSufficiencySupport.Comparison.intervalRoom_open line 246
  22. theorem OAI.PackingSufficiencySupport.Comparison.strictMono_open line 257
  23. theorem OAI.PackingSufficiencySupport.Comparison.exists_uniform_interval_widths line 269
  24. def OAI.PackingSufficiencySupport.Comparison.clampUnit line 322
  25. theorem OAI.PackingSufficiencySupport.Comparison.continuous_clampUnit line 324
  26. theorem OAI.PackingSufficiencySupport.Comparison.clampUnit_eq line 327
  27. def OAI.PackingSufficiencySupport.Comparison.unitIntervalValue line 330
  28. def OAI.PackingSufficiencySupport.Comparison.unitRearrange line 343
  29. theorem OAI.PackingSufficiencySupport.Comparison.unitRearrange_attained line 347
  30. theorem OAI.PackingSufficiencySupport.Comparison.unitRearrange_le_candidate line 357
  31. theorem OAI.PackingSufficiencySupport.Comparison.unitRearrange_one line 365
  32. theorem OAI.PackingSufficiencySupport.Comparison.unitRearrange_mono line 371
  33. def OAI.PackingSufficiencySupport.Comparison.unitSublevel line 385
  34. theorem OAI.PackingSufficiencySupport.Comparison.unitSublevel_open line 388
  35. theorem OAI.PackingSufficiencySupport.Comparison.unitSublevel_room line 394
  36. theorem OAI.PackingSufficiencySupport.Comparison.unitSublevel_convex line 404
  37. theorem OAI.PackingSufficiencySupport.Comparison.unitSublevel_mono line 415
  38. def OAI.PackingSufficiencySupport.Comparison.fixedIntervalValue line 426
  39. def OAI.PackingSufficiencySupport.Comparison.intervalMinimum line 431
  40. theorem OAI.PackingSufficiencySupport.Comparison.intervalMinimum_attained line 433
  41. theorem OAI.PackingSufficiencySupport.Comparison.intervalMinimum_le_candidate line 439
  42. theorem OAI.PackingSufficiencySupport.Comparison.intervalMinimum_shortening line 445
  43. theorem OAI.PackingSufficiencySupport.Comparison.intervalMinimum_outer_strip line 469
  44. theorem OAI.PackingSufficiencySupport.Comparison.intervalMinimum_small line 480
  45. def OAI.PackingSufficiencySupport.Comparison.scaledUnitFamily line 491
  46. def OAI.PackingSufficiencySupport.Comparison.fiberFunction line 495
  47. theorem OAI.PackingSufficiencySupport.Comparison.unitRearrange_scaled line 498