OAI/Geometry/BallPacking/Moments/AnalyticBoundary.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered_contDiff_analytic line 15
  2. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_analytic_axis_radial_solution line 19
  3. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_analytic_other_axis_radial_solution line 44
  4. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_analytic_boundary_radial_solution line 89
  5. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_analytic_boundary_moment_inverse line 105
  6. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_inverse_open_representative line 153
  7. def OAI.PackingSufficiencySupport.FiniteMoment.gibbs line 207
  8. theorem OAI.PackingSufficiencySupport.FiniteMoment.gibbs_pos line 210
  9. theorem OAI.PackingSufficiencySupport.FiniteMoment.sum_gibbs line 213
  10. theorem OAI.PackingSufficiencySupport.FiniteMoment.gibbs_mean line 220
  11. theorem OAI.PackingSufficiencySupport.FiniteMoment.gibbs_log line 228
  12. theorem OAI.PackingSufficiencySupport.FiniteMoment.scalar_relative_log line 233
  13. theorem OAI.PackingSufficiencySupport.FiniteMoment.relative_log_sum_le line 245
  14. theorem OAI.PackingSufficiencySupport.FiniteMoment.probability_log_sum_nonpos line 252
  15. theorem OAI.PackingSufficiencySupport.FiniteMoment.probability_log_sum_lower line 266
  16. theorem OAI.PackingSufficiencySupport.FiniteMoment.probability_weighted_le line 278
  17. theorem OAI.PackingSufficiencySupport.FiniteMoment.probability_weighted_ge line 285
  18. theorem OAI.PackingSufficiencySupport.FiniteMoment.finite_log_height_bound line 292
  19. theorem OAI.PackingSufficiencySupport.FiniteMoment.gibbs_tilt_log line 322
  20. theorem OAI.PackingSufficiencySupport.FiniteMoment.gibbs_tilt_height_bound line 331
  21. theorem OAI.PackingSufficiencySupport.FiniteMoment.partition_scale_translate line 351
  22. theorem OAI.PackingSufficiencySupport.FiniteMoment.gibbs_scale_translate line 360
  23. theorem OAI.PackingSufficiencySupport.FiniteMoment.moment_scale_translate line 371
  24. theorem OAI.PackingSufficiencySupport.FiniteMoment.probability_nonneg_bound line 378
  25. def OAI.PackingSufficiencySupport.FiniteMoment.selected line 389
  26. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_pos line 393
  27. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_sum line 397
  28. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_mean line 400
  29. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_contDiffAt line 404
  30. theorem OAI.PackingSufficiencySupport.FiniteMoment.selected_gauge line 414
  31. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability line 434
  32. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected line 437
  33. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_nonneg line 440
  34. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_sum line 445
  35. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_mean line 450
  36. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_contDiffAt line 468
  37. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.probability_expRadius line 475
  38. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected_nonneg line 479
  39. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected_sum line 483
  40. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.selected_eq_exponential line 487
  41. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_selected_contDiffWithinAt line 498
  42. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_selected_coeff_contDiffAt line 511
  43. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_selected_mean line 522
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.compact_local_smooth_extension line 542
  45. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_selected_open_representative line 569
  46. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_selected_compact_extension line 597