OAI/Geometry/BallPacking/Toric/CubicRadialProbability.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.radialProbability_nonneg line 15
  2. theorem OAI.PackingSufficiencySupport.CubicModel.radialProbability_sum line 20
  3. theorem OAI.PackingSufficiencySupport.CubicModel.radialProbability_mean line 25
  4. theorem OAI.PackingSufficiencySupport.CubicModel.reducedEndRegularPrimitive_norm_le line 37
  5. theorem OAI.PackingSufficiencySupport.CubicModel.exists_regularCoefficient_log_bound line 50
  6. theorem OAI.PackingSufficiencySupport.CubicModel.exists_regularPrimitive_bound line 74
  7. theorem OAI.PackingSufficiencySupport.CubicModel.radialEndRegularPrimitive_norm_le line 100
  8. def OAI.PackingSufficiencySupport.CubicModel.limitingEndOrder line 114
  9. theorem OAI.PackingSufficiencySupport.CubicModel.probability_affine_degree line 118
  10. theorem OAI.PackingSufficiencySupport.CubicModel.reducedEndProbability_regularized line 127
  11. theorem OAI.PackingSufficiencySupport.CubicModel.reducedEndResidue_error line 144
  12. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lowerTrapezoid_interior_sequence line 201
  13. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_selected_tendsto line 224
  14. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected_marked_error_lower line 236
  15. theorem OAI.PackingSufficiencySupport.CubicModel.radialEndProbability_regularized line 274
  16. theorem OAI.PackingSufficiencySupport.CubicModel.radialEndResidue_error line 291
  17. theorem OAI.PackingSufficiencySupport.CubicModel.reducedEndProbability_contDiffAt line 341
  18. theorem OAI.PackingSufficiencySupport.CubicModel.reducedEndRegularPrimitive_contDiffAt line 349
  19. theorem OAI.PackingSufficiencySupport.CubicModel.reducedEndResidue_contDiffAt line 357