OAI/Geometry/BallPacking/Models/EqualNormalModelConvergence.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalCoefficient_pos line 12
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalCoefficient_le_one line 18
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalCoefficient_uniform_limit line 23
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_equalNormalPrimitive_sequence line 48
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalPrimitive_mass line 75
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.equalNormalPrimitive_area_limit line 86
  7. def OAI.PackingSufficiencySupport.DiagonalQuadrics.normalHorizontalPrimitive line 111
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalHorizontalPrimitive_smooth line 114
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalHorizontalPrimitive_exterior line 119
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.normalHorizontalPrimitive_area_limit line 126
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverse_transition_differentiable line 146
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverse_transition_inverse_differentiable line 159
  13. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.transverseDiffeomorph_positive line 167
  14. def OAI.PackingSufficiencySupport.Hamiltonian.rectanglePolar line 190
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.rectanglePolar_smooth line 193
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.rectanglePolar_det line 198
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.rectanglePolar_det_pos line 217
  18. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.fixed_handle_densityChart_positive line 230
  19. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_positive_fixed_annularHandleData line 262
  20. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.exists_positive_annularHandleData line 269
  21. def OAI.PackingSufficiencySupport.momentSimplex line 280
  22. theorem OAI.PackingSufficiencySupport.momentSimplex_isClosed line 283
  23. theorem OAI.PackingSufficiencySupport.momentSimplex_isCompact line 289
  24. theorem OAI.PackingSufficiencySupport.momentSimplex_cons line 295
  25. theorem OAI.PackingSufficiencySupport.integrable_simplex_power line 305
  26. theorem OAI.PackingSufficiencySupport.simplex_power_cons line 310
  27. theorem OAI.PackingSufficiencySupport.integral_simplex_power_step line 329
  28. theorem OAI.PackingSufficiencySupport.integral_simplex_power line 355
  29. theorem OAI.PackingSufficiencySupport.volumeReal_momentSimplex line 379
  30. theorem OAI.PackingSufficiencySupport.integral_simplex_tent line 383
  31. theorem OAI.PackingSufficiencySupport.tent_indicator_eq line 387
  32. theorem OAI.PackingSufficiencySupport.integrableOn_tent line 400
  33. theorem OAI.PackingSufficiencySupport.integral_tent line 407
  34. theorem OAI.PackingSufficiencySupport.integral_sum_tents line 415
  35. def OAI.PackingSufficiencySupport.smallModelMean line 425
  36. theorem OAI.PackingSufficiencySupport.integral_small_model line 428
  37. theorem OAI.PackingSufficiencySupport.continuous_smallModelMean line 447
  38. theorem OAI.PackingSufficiencySupport.smallModelMean_half line 451
  39. def OAI.PackingSufficiencySupport.cappedAffine line 462
  40. theorem OAI.PackingSufficiencySupport.continuous_cappedAffine line 466
  41. theorem OAI.PackingSufficiencySupport.concaveOn_cappedAffine line 471