OAI/Analysis/VlasovMaxwell/Retarded/PhysicalAngularBound.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.transportSpatialFlux_joint_contDiffAt line 16
  2. lemma OAI.RVM.divergence_phase_first line 34
  3. lemma OAI.RVM.continuousOn_transportSpatialDivergence line 47
  4. lemma OAI.RVM.transportSpatialDivergence_uniform_bound line 62
  5. lemma OAI.RVM.divergence_phase_second line 79
  6. lemma OAI.RVM.continuous_divergence_phase_slices line 92
  7. lemma OAI.RVM.phase_division_integral line 109
  8. lemma OAI.RVM.contDiffAt_coneSpatialCoefficient_phase line 157
  9. lemma OAI.RVM.retarded_spatial_integral_division line 166
  10. lemma OAI.RVM.continuousOn_phase_divergences line 202
  11. lemma OAI.RVM.continuousOn_divergence_of_isOpen line 221
  12. lemma OAI.RVM.phase_division_annulus line 235
  13. def OAI.RVM.spatialTranslateParticle line 295
  14. lemma OAI.RVM.spatialTranslateParticle_add line 298
  15. lemma OAI.RVM.fderiv_spatialTranslateParticle line 304
  16. lemma OAI.RVM.shifted_retarded_local_data line 310
  17. lemma OAI.RVM.shifted_retarded_spatial_divergence line 340
  18. lemma OAI.RVM.retarded_spatial_annulus line 365