OAI/Geometry/BallPacking/DiskMaps/CubicAreaExhaustion.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.CubicModel.exists_cubic_end_cutoff line 20
  2. theorem OAI.PackingSufficiencySupport.CubicModel.tendsto_cubic_cutoff_mass line 46
  3. theorem OAI.PackingSufficiencySupport.CubicModel.cubic_compact_area_le_degree line 74
  4. theorem OAI.PackingSufficiencySupport.CubicModel.tendsto_cubic_exhaustion_area line 86
  5. theorem OAI.PackingSufficiencySupport.CubicModel.exists_small_cubic_end_cutoff line 115
  6. theorem OAI.PackingSufficiencySupport.CubicModel.reduced_cubic_compact_area_le line 145
  7. theorem OAI.PackingSufficiencySupport.CubicModel.tendsto_reduced_cubic_exhaustion_area line 163
  8. theorem OAI.PackingSufficiencySupport.CubicModel.radial_cubic_compact_area_le line 195
  9. theorem OAI.PackingSufficiencySupport.CubicModel.tendsto_radial_cubic_exhaustion_area line 212
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_mono line 248
  11. theorem OAI.PackingSufficiencySupport.CubicModel.tendstoUniformlyOn_radial_cubic_area line 275
  12. def OAI.PackingSufficiencySupport.Hamiltonian.squareSqueeze line 312
  13. def OAI.PackingSufficiencySupport.Hamiltonian.squeezedDisk line 315
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.tanh_smooth line 317
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.tanh_hasDerivAt line 323
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.squareSqueeze_smooth line 331
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.squareSqueeze_injective line 335
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.squareSqueeze_fderiv line 341
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.squareSqueeze_det_pos line 352
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.squeezedDisk_compact line 362
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.squeezedDisk_subset line 365
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_squeezedDisk_contains line 370
  23. def OAI.PackingSufficiencySupport.Hamiltonian.squeezedArea line 402
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.squeezedArea_nonneg line 404
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_closed_square_volume line 406
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.squeezedArea_le line 413
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.squeezedArea_lower line 424
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_rounded_square line 432
  29. def OAI.PackingSufficiencySupport.Hamiltonian.diagonalScale line 439
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.diagonalScale_apply line 442
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.diagonalScale_det line 445
  32. def OAI.PackingSufficiencySupport.Hamiltonian.affineRectangle line 449
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineRectangle_image_volume line 451
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.affineRectangle_squeezedArea line 460
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_rounded_square_with_control line 469