OAI/Geometry/BallPacking/SurfaceArea/BoundedPlanarResidue.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialAnnulus_coordinate_bound line 13
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialAnnulus_real_volume_le line 22
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffWedge_radial_apply line 38
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffWedge_radial_bound line 49
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.bounded_residue_error_integral line 77
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveCutoffDefect_variable_coefficient line 110
  7. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveCutoff_variable_flux_partition line 159
  8. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveCutoff_variable_flux_mass line 203
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_annular_radial_derivative line 237
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.continuousOn_cutoffWedge_radial line 245
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.variable_flux_error_bound line 255
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff_tsupport_scaled line 286
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff_deriv line 298
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinking_variable_flux_error line 304
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.tendsto_shrinking_variable_flux line 330
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.tendsto_curveCutoff_bounded_residue line 368
  17. def OAI.PackingSufficiencySupport.Hamiltonian.logarithmicError line 414
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.logarithmicError_nonneg line 416
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.logarithmicError_bound line 422
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.tendsto_logarithmicError line 430
  21. theorem OAI.PackingSufficiencySupport.CubicModel.sum_limitingEndOrder line 449
  22. theorem OAI.PackingSufficiencySupport.CubicModel.tendsto_reduced_cubic_cutoff_mass line 457