OAI/Geometry/BallPacking/Toric/CubicCoefficientDifferential.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.coefficientNorm_chart_hasFDerivAt line 13
  2. theorem OAI.PackingSufficiencySupport.CubicModel.weightedFSPrimitive_chart_log line 27
  3. theorem OAI.PackingSufficiencySupport.FiniteMoment.constrained_log_derivative line 63
  4. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_coeff_differentiableAt line 76
  5. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_log_variation line 83
  6. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_log_variation_nonneg line 130
  7. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_exterior_apply line 138
  8. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_exterior_positive line 159
  9. theorem OAI.PackingSufficiencySupport.CubicModel.reducedPrimitive_chart line 200
  10. theorem OAI.PackingSufficiencySupport.CubicModel.reducedForm_positive line 209
  11. def OAI.PackingSufficiencySupport.CubicModel.selectedProbability line 239
  12. theorem OAI.PackingSufficiencySupport.CubicModel.selectedProbability_pos line 243
  13. theorem OAI.PackingSufficiencySupport.CubicModel.selectedProbability_sum line 248
  14. theorem OAI.PackingSufficiencySupport.CubicModel.selectedProbability_mean line 252
  15. theorem OAI.PackingSufficiencySupport.CubicModel.selectedProbability_smooth line 256
  16. def OAI.PackingSufficiencySupport.CubicModel.selectedPrimitive line 266
  17. def OAI.PackingSufficiencySupport.CubicModel.selectedForm line 270
  18. theorem OAI.PackingSufficiencySupport.CubicModel.selectedPrimitive_smooth line 273
  19. theorem OAI.PackingSufficiencySupport.CubicModel.selectedForm_smooth line 281
  20. theorem OAI.PackingSufficiencySupport.CubicModel.selectedForm_skew line 286
  21. theorem OAI.PackingSufficiencySupport.CubicModel.selectedPrimitive_chart line 291
  22. theorem OAI.PackingSufficiencySupport.CubicModel.selectedForm_positive line 300
  23. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.face_surrounds line 334
  24. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.inverse_axis line 343
  25. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_axis_active line 354
  26. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_axis_inactive line 359
  27. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected_axis_active line 363
  28. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected_axis_inactive line 372
  29. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_swap line 381
  30. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse_swap line 386
  31. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected_swap line 398
  32. def OAI.PackingSufficiencySupport.CubicModel.radialProbability line 415
  33. def OAI.PackingSufficiencySupport.CubicModel.radialPrimitive line 419
  34. def OAI.PackingSufficiencySupport.CubicModel.radialForm line 423
  35. theorem OAI.PackingSufficiencySupport.CubicModel.radialProbability_smooth line 426
  36. theorem OAI.PackingSufficiencySupport.CubicModel.radialPrimitive_smooth line 439
  37. theorem OAI.PackingSufficiencySupport.CubicModel.radialForm_smooth line 449
  38. theorem OAI.PackingSufficiencySupport.CubicModel.radialForm_skew line 454
  39. theorem OAI.PackingSufficiencySupport.CubicModel.radialPrimitive_eq_reduced line 458
  40. theorem OAI.PackingSufficiencySupport.CubicModel.radialPrimitive_eq_face line 470