OAI/Geometry/BallPacking/Toric/RestrictedMassIndependence.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.restrictedPartitionFormMass_independent line 19
  2. def OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceBoxes line 74
  3. def OAI.PackingSufficiencySupport.Hamiltonian.compactSurfacePartition line 77
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfacePartition_subordinate line 81
  5. def OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral line 86
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_eq line 92
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_congr line 102
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.zero line 119
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.sum line 125
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_sum line 136
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.restrictedPartitionFormMass_smul line 158
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_smul line 170
  13. def OAI.PackingSufficiencySupport.Hamiltonian.equalNormalCoefficient line 181
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalCoefficient_smooth line 184
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_base_primitive_near_compact line 189
  16. def OAI.PackingSufficiencySupport.Hamiltonian.equalNormalPrimitive line 202
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalPrimitive_smooth line 208
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalPrimitive_exterior line 220
  19. def OAI.PackingSufficiencySupport.Hamiltonian.familySpatialExterior line 262
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.familySpatialExterior_smoothAt line 266
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.familySpatialExterior_eq_slice line 275
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_family_smooth line 288
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_spatial_smul line 306
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.spatial_smul line 312
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_zero_off line 324
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_path_closed line 337
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_path_time line 352
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.time_contDiffAt line 371
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldTimePrimitive_annihilates line 384
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldTimePrimitive_eval_constant line 395
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldTimePrimitive_stationary line 408
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_skew line 415
  33. def OAI.PackingSufficiencySupport.CubicModel.coefficientNorm line 436
  34. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientNorm_pos line 439
  35. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientNorm_smooth line 443
  36. def OAI.PackingSufficiencySupport.CubicModel.reducedProbability line 447
  37. theorem OAI.PackingSufficiencySupport.CubicModel.reducedProbability_pos line 450
  38. theorem OAI.PackingSufficiencySupport.CubicModel.reducedProbability_sum line 454
  39. theorem OAI.PackingSufficiencySupport.CubicModel.reducedProbability_mean line 458
  40. theorem OAI.PackingSufficiencySupport.CubicModel.reducedProbability_smooth line 462
  41. def OAI.PackingSufficiencySupport.CubicModel.reducedPrimitive line 472
  42. def OAI.PackingSufficiencySupport.CubicModel.reducedForm line 476
  43. theorem OAI.PackingSufficiencySupport.CubicModel.reducedPrimitive_smooth line 479
  44. theorem OAI.PackingSufficiencySupport.CubicModel.reducedForm_smooth line 487
  45. theorem OAI.PackingSufficiencySupport.CubicModel.reducedForm_skew line 492