OAI/Geometry/BallPacking/SurfaceArea/CubicRadialEndSmooth.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.radialEndProbability_contDiffAt line 14
  2. theorem OAI.PackingSufficiencySupport.CubicModel.radialEndRegularPrimitive_contDiffAt line 23
  3. theorem OAI.PackingSufficiencySupport.CubicModel.radialEndResidue_contDiffAt line 32
  4. theorem OAI.PackingSufficiencySupport.CubicModel.tendsto_radial_cubic_cutoff_mass line 42
  5. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.latticeOrigin line 115
  6. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.latticeIndex_injective line 118
  7. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.monomial_origin line 125
  8. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_monomial_origin line 137
  9. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_polynomial_origin line 144
  10. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_probability_origin line 149
  11. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_selected_origin line 158
  12. theorem OAI.PackingSufficiencySupport.CubicModel.radialPrimitive_swap line 177
  13. theorem OAI.PackingSufficiencySupport.CubicModel.radialPrimitive_origin line 190
  14. theorem OAI.PackingSufficiencySupport.CubicModel.radialForm_face_positive line 200
  15. theorem OAI.PackingSufficiencySupport.CubicModel.radialForm_positive line 213
  16. def OAI.PackingSufficiencySupport.CubicModel.regularEndPhase line 257
  17. def OAI.PackingSufficiencySupport.CubicModel.regularEndPrimitive line 260
  18. def OAI.PackingSufficiencySupport.CubicModel.endResidue line 263
  19. theorem OAI.PackingSufficiencySupport.CubicModel.regularEndPhase_contDiffAt line 265
  20. theorem OAI.PackingSufficiencySupport.CubicModel.regularEndPrimitive_contDiffAt line 272
  21. theorem OAI.PackingSufficiencySupport.CubicModel.endRegular_scale line 279
  22. theorem OAI.PackingSufficiencySupport.CubicModel.endQuotientPrimitive_residue line 283
  23. theorem OAI.PackingSufficiencySupport.CubicModel.cubic_curveFSPrimitive_infinity line 338
  24. theorem OAI.PackingSufficiencySupport.CubicModel.sum_endResidue line 359
  25. theorem OAI.PackingSufficiencySupport.CubicModel.exists_regularEndPrimitive_extension line 367
  26. theorem OAI.PackingSufficiencySupport.CubicModel.cubic_regular_extension_germ line 385