OAI/Geometry/BallPacking/Moments/RadialSwap.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.polynomial_swap line 15
  2. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.numerator_swap line 22
  3. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_swap line 27
  4. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.centered_swap line 33
  5. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_smooth_other_axis_radial_solution line 38
  6. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.basis_weights_separate line 86
  7. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.positive_radial_unique_basis line 109
  8. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_zero_coordinates line 124
  9. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.moment_injective_quadrant line 133
  10. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_smooth_boundary_radial_solution line 180
  11. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.exists_smooth_boundary_moment_inverse line 196
  12. abbrev OAI.PackingSufficiencySupport.FiniteMoment.Radial.Quadrant line 247
  13. instance OAI.PackingSufficiencySupport.FiniteMoment.Radial.(instance at line 248) line 248
  14. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse line 250
  15. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse_nonneg line 253
  16. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse_spec line 257
  17. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse_of_moment line 265
  18. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse_eq_of_moment line 272
  19. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.boundary_inverse_smooth_extension line 279
  20. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.boundary_inverse_contDiffWithinAt line 294
  21. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.boundary_inverse_coeff_contDiffAt line 305
  22. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.latticeIndex line 333
  23. def OAI.PackingSufficiencySupport.FiniteMoment.Radial.lowerTrapezoid line 336
  24. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_zero line 339
  25. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_unit_fst line 342
  26. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_unit_snd line 346
  27. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_end_fst line 350
  28. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.lattice_end_snd line 354
  29. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_radial_surjective line 358
  30. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_inverse_spec line 392
  31. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.planeVector_contDiff line 406
  32. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.expRadius_contDiff line 413
  33. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse_exp line 416
  34. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.nonnegativeInverse_interior_contDiffAt line 428
  35. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_inverse_contDiffWithinAt line 452
  36. theorem OAI.PackingSufficiencySupport.FiniteMoment.Radial.trapezoid_inverse_coeff_contDiffAt line 477