OAI/Geometry/BallPacking/Rigidity/PlanarResidueCutoff.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SymplecticBallPacking.Hamiltonian.planarCurl_contDiff line 11
  2. theorem OAI.SymplecticBallPacking.Hamiltonian.planarCurl_compact line 16
  3. def OAI.SymplecticBallPacking.Hamiltonian.cutoffWedge line 23
  4. theorem OAI.SymplecticBallPacking.Hamiltonian.planarCurl_spatial_smul line 26
  5. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_cutoffWedge line 37
  6. theorem OAI.SymplecticBallPacking.Hamiltonian.cutoffWedge_integrable line 50
  7. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_planar_residue_cutoff line 60
  8. theorem OAI.SymplecticBallPacking.Hamiltonian.cutoffWedge_radial_angular line 79
  9. theorem OAI.SymplecticBallPacking.Hamiltonian.planar_residue_defect line 92
  10. def OAI.SymplecticBallPacking.Hamiltonian.radialAnnulus line 116
  11. theorem OAI.SymplecticBallPacking.Hamiltonian.radialAnnulus_compact line 118
  12. theorem OAI.SymplecticBallPacking.Hamiltonian.radialAnnulus_ne_zero line 128
  13. theorem OAI.SymplecticBallPacking.Hamiltonian.radialAnnulus_radius_ne_zero line 135
  14. theorem OAI.SymplecticBallPacking.Hamiltonian.radiusSq_complex line 138
  15. theorem OAI.SymplecticBallPacking.Hamiltonian.radialAnnulus_coordinate_bound line 142
  16. theorem OAI.SymplecticBallPacking.Hamiltonian.radialAnnulus_real_volume_le line 151
  17. theorem OAI.SymplecticBallPacking.Hamiltonian.cutoffWedge_radial_apply line 167
  18. theorem OAI.SymplecticBallPacking.Hamiltonian.cutoffWedge_radial_bound line 178
  19. theorem OAI.SymplecticBallPacking.Hamiltonian.bounded_residue_error_integral line 206
  20. theorem OAI.SymplecticBallPacking.Hamiltonian.radialCutoff_deriv_zero_off_annulus line 229
  21. theorem OAI.SymplecticBallPacking.Hamiltonian.planarResidueDensity_zero_off line 244
  22. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_planar_residue_annulus line 256
  23. def OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff line 266
  24. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff_smooth line 268
  25. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff_compact line 271
  26. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff_one line 277
  27. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff_tsupport line 290
  28. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff_eventually_zero line 302
  29. theorem OAI.SymplecticBallPacking.Hamiltonian.radiusSq_pos line 317
  30. theorem OAI.SymplecticBallPacking.Hamiltonian.tendsto_shrinking_regular_residue line 325
  31. theorem OAI.SymplecticBallPacking.Hamiltonian.integral_annular_radial_derivative line 353
  32. theorem OAI.SymplecticBallPacking.Hamiltonian.continuousOn_cutoffWedge_radial line 361
  33. theorem OAI.SymplecticBallPacking.Hamiltonian.variable_flux_error_bound line 371
  34. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff_tsupport_scaled line 402
  35. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinkingCutoff_deriv line 414
  36. theorem OAI.SymplecticBallPacking.Hamiltonian.shrinking_variable_flux_error line 420
  37. theorem OAI.SymplecticBallPacking.Hamiltonian.tendsto_shrinking_variable_flux line 446