OAI/Geometry/BallPacking/Residues/AreaPolarChart.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.areaPolarRadial line 14
  2. def OAI.PackingSufficiencySupport.Hamiltonian.areaPolar line 17
  3. def OAI.PackingSufficiencySupport.Hamiltonian.areaPolarDomain line 19
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolarRadial_smoothAt line 21
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolar_smoothAt line 26
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolarRadial_target line 30
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolar_injOn line 38
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolarRadial_fderiv line 50
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolar_det line 60
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolar_capacity line 78
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.areaPolar_image_volume line 89
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactSupport.left_slice line 105
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactSupport.right_slice line 112
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_compact_partial_fst line 119
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_compact_partial_snd line 140
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.compact_planar_stokes line 161
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactSupport.comp_radiusSq line 188
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactSupport.comp_square line 201
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_radial_derivative line 206
  20. def OAI.PackingSufficiencySupport.Hamiltonian.planarDot line 232
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarDot_apply line 238
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_hasFDerivAt line 240
  23. def OAI.PackingSufficiencySupport.Hamiltonian.angularOneForm line 252
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.angularOneForm_contDiffAt line 254
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialArea_curl line 258
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffAngular_curl line 271
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_cutoffAngular_density line 286
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCurl_contDiff line 291
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCurl_compact line 296
  30. def OAI.PackingSufficiencySupport.Hamiltonian.cutoffWedge line 303
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCurl_spatial_smul line 306
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_cutoffWedge line 317
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffWedge_integrable line 330
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_planar_residue_cutoff line 340
  35. def OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff line 359
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff_smooth line 361
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff_compact line 364
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff_one line 370
  39. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff_tsupport line 383
  40. theorem OAI.PackingSufficiencySupport.Hamiltonian.shrinkingCutoff_eventually_zero line 395
  41. theorem OAI.PackingSufficiencySupport.Hamiltonian.radiusSq_pos line 410
  42. theorem OAI.PackingSufficiencySupport.Hamiltonian.tendsto_shrinking_regular_residue line 418
  43. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_cutoff line 449
  44. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_compact_extension line 463
  45. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveSigmaCompact line 503
  46. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_end_cutoff line 507
  47. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.shrinking_curveEndCutoff_compact line 533
  48. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_eventually_one_on_compact line 543