OAI/Geometry/BallPacking/Flows/TimeSteps.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.stepHomeomorph line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_of_zero line 27
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_of_zero line 36
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_hasCompactSupport line 41
  5. def OAI.PackingSufficiencySupport.Hamiltonian.clockField line 51
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.clockField_apply line 55
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.clockField_lipschitz line 59
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.clockField_smooth line 66
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_clock line 69
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.stepEndpoint_clock line 87
  11. def OAI.PackingSufficiencySupport.Hamiltonian.timeStep line 92
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_smooth line 95
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_inverse line 101
  14. def OAI.PackingSufficiencySupport.Hamiltonian.timeStepHomeomorph line 115
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedStep_variation_clock line 134
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_fderiv line 152
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.clockField_fderiv line 165
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_preserves_density line 171
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeStep_of_stationary line 253
  20. def OAI.PackingSufficiencySupport.Hamiltonian.timeSteps line 281
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_smooth line 286
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_of_stationary line 297
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.timeSteps_preserves_density line 306
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_density_transport line 330
  25. def OAI.PackingSufficiencySupport.Hamiltonian.segmentLinear line 360
  26. def OAI.PackingSufficiencySupport.Hamiltonian.segmentPath line 378
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.segmentPath_apply line 381
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.segmentPath_smooth line 386
  29. def OAI.PackingSufficiencySupport.Hamiltonian.pathAverage line 389
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.segment_integral_eq line 392
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiff_segment_integral line 410
  32. def OAI.PackingSufficiencySupport.Hamiltonian.planarMarginal line 420
  33. def OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitiveX line 423
  34. def OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitiveY line 426
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarMarginal_smooth line 429
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitive_smooth line 433
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitive_curl line 443
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.interval_primitive_zero_outside line 459
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitive_support line 485
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_eq_full_of_box_support line 538