OAI/Geometry/BallPacking/Moser/BackgroundDensity.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_relative_planar_moser_correction line 19
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.homeomorph_image_closedRoundDisk line 50
  3. def OAI.PackingSufficiencySupport.Hamiltonian.backgroundDensity line 63
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.backgroundDensity_positive line 66
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.backgroundDensity_smooth line 78
  6. def OAI.PackingSufficiencySupport.Hamiltonian.backgroundField line 82
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.backgroundField_smooth line 86
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.backgroundField_compact line 97
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.backgroundField_transport line 109
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.backgroundField_tangent line 174
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_relative_background_moser line 187
  12. def OAI.PackingSufficiencySupport.Hamiltonian.parameterSegmentLinear line 231
  13. def OAI.PackingSufficiencySupport.Hamiltonian.parameterSegmentPath line 248
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterSegmentPath_apply line 251
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameterSegmentPath_smooth line 256
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.parameter_segment_integral_eq line 259
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.contDiff_parameter_segment_integral line 280
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitive_parameter_smooth line 291
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitive_zero_outside line 312
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSupport_fiber line 357
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_parametric_compact_primitive line 364
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixed_spatial_planar_primitive line 447
  23. def OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm line 512
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.fderiv_clm_eval line 515
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.fderiv_bilinear_eval line 521
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_smooth line 526
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_fderiv line 535
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_closed line 547