OAI/Geometry/BallPacking/Surfaces/QuadricOrientation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.real_transition_positive line 14
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.positivePlaneTransitions line 26
  3. def OAI.PackingSufficiencySupport.Hamiltonian.partialChartCoefficient line 47
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.partialChartCoefficient_contDiffOn line 52
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.partialChartCoefficient_change line 64
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.partialChart_area_integral_change line 77
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_eq_partialChart_integral line 127
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_box_primitive line 147
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.connected_cover_overlap_chain line 185
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoForm.coefficient_integrable line 232
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_box_difference line 241
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_overlap_bump_difference line 269
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_bump_difference line 294
  14. def OAI.PackingSufficiencySupport.Hamiltonian.partitionTwoForm line 327
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionTwoForm_smooth line 332
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionTwoForm_skew line 338
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionTwoForm_zero line 346
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionTwoForm_sum line 360
  19. def OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass line 384
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.surface_partition_primitive line 388
  21. def OAI.PackingSufficiencySupport.Hamiltonian.PositivePartialChart line 481
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.partialChartCoefficient_smul line 487
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_eq_partialChart_integral line 492