OAI/Analysis/VlasovMaxwell/Geometry/BallCutoff.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.continuous_dot line 31
  2. def OAI.RVM.ballCutoff line 35
  3. lemma OAI.RVM.contDiff_ballCutoff line 38
  4. lemma OAI.RVM.ballCutoff_fderiv line 43
  5. lemma OAI.RVM.ballCutoff_zero line 60
  6. lemma OAI.RVM.ballCutoff_compact line 65
  7. lemma OAI.RVM.ballCutoff_tendsto line 69
  8. lemma OAI.RVM.ballCutoff_integral_tendsto line 89
  9. lemma OAI.RVM.ballCutoff_divergence line 112
  10. lemma OAI.RVM.ballShell_polar line 122
  11. lemma OAI.RVM.divergence_ball line 170
  12. lemma OAI.RVM.hasFDerivAt_integral_sphere line 213
  13. lemma OAI.RVM.continuous_integral_sphere line 239
  14. lemma OAI.RVM.contDiff_integral_sphere_nat line 250
  15. lemma OAI.RVM.contDiff_integral_sphere line 276
  16. def OAI.RVM.sphereSum line 285
  17. lemma OAI.RVM.contDiff_sphereSum line 288
  18. lemma OAI.RVM.sphereSum_radial_deriv line 294
  19. lemma OAI.RVM.integral_ball_polar line 319
  20. def OAI.RVM.laplace line 361
  21. lemma OAI.RVM.contDiff_gradient line 363
  22. lemma OAI.RVM.continuous_laplace line 368
  23. lemma OAI.RVM.sphereSum_flux line 371