OAI/Geometry/BallPacking/Toric/CubicRadialFamilyExtension.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.exists_radialPrimitive_smooth_extension line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionChartDensity_family_continuous line 71
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.restrictedPartitionFormMass_family_continuous line 101
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_family_continuous line 112
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_congr_germ line 125
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling_congr_germ line 139
  7. theorem OAI.PackingSufficiencySupport.CubicModel.radial_compact_area_continuousOn line 158
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.partialChartCoefficient_exterior line 187
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanPullbackOneForm_spatial_smul line 207
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.partialChartCoefficient_sub line 216
  11. def OAI.PackingSufficiencySupport.Hamiltonian.radialAnnulus line 223
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialAnnulus_compact line 225
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialAnnulus_ne_zero line 235
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialAnnulus_radius_ne_zero line 242
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_complex line 245
  16. def OAI.PackingSufficiencySupport.CubicModel.reducedEndProbability line 258
  17. def OAI.PackingSufficiencySupport.CubicModel.reducedEndRegularPrimitive line 262
  18. def OAI.PackingSufficiencySupport.CubicModel.reducedEndResidue line 266
  19. theorem OAI.PackingSufficiencySupport.CubicModel.reducedPrimitive_infinity line 270
  20. def OAI.PackingSufficiencySupport.CubicModel.regularCoefficientNorm line 303
  21. theorem OAI.PackingSufficiencySupport.CubicModel.regularCoefficientNorm_pos line 306
  22. theorem OAI.PackingSufficiencySupport.CubicModel.regularCoefficientNorm_contDiffAt line 309
  23. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientNorm_regularization line 314
  24. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientNorm_eq_regular_div line 327
  25. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_div_power line 348
  26. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_marked_error line 370
  27. def OAI.PackingSufficiencySupport.CubicModel.totalWeight line 418
  28. def OAI.PackingSufficiencySupport.CubicModel.cubicDegree line 419
  29. def OAI.PackingSufficiencySupport.CubicModel.cubicMarkedOrder line 420
  30. theorem OAI.PackingSufficiencySupport.CubicModel.totalWeight_le line 422
  31. theorem OAI.PackingSufficiencySupport.CubicModel.cubicMarked_lt_degree line 424
  32. theorem OAI.PackingSufficiencySupport.CubicModel.cubicMarked_twice_complement line 430
  33. theorem OAI.PackingSufficiencySupport.CubicModel.totalWeight_cast line 436
  34. theorem OAI.PackingSufficiencySupport.CubicModel.cubicDegree_cast line 440
  35. theorem OAI.PackingSufficiencySupport.CubicModel.cubicMarkedOrder_cast line 444
  36. theorem OAI.PackingSufficiencySupport.CubicModel.cubicEndOrder_cast line 458
  37. def OAI.PackingSufficiencySupport.CubicModel.radialEndProbability line 472
  38. def OAI.PackingSufficiencySupport.CubicModel.radialEndRegularPrimitive line 476
  39. def OAI.PackingSufficiencySupport.CubicModel.radialEndResidue line 480
  40. theorem OAI.PackingSufficiencySupport.CubicModel.radialPrimitive_infinity line 484