OAI/Analysis/VlasovMaxwell/Population/SphericalFluxNorm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.spherical_flux_norm_le line 33
  2. lemma OAI.RVM.spherical_flux_tendsto_zero line 49
  3. lemma OAI.RVM.fderiv_norm_apply_rvm line 61
  4. lemma OAI.RVM.fderiv_conePotential_apply line 73
  5. lemma OAI.RVM.divergence_conePotential line 97
  6. lemma OAI.RVM.integrableOn_ball_div_norm_pow line 114
  7. lemma OAI.RVM.norm_direction_coord_le line 126
  8. lemma OAI.RVM.integrableOn_ball_direction_div_norm_pow line 132
  9. lemma OAI.RVM.contDiffAt_conePotential line 143
  10. lemma OAI.RVM.integrable_conePotential_divergence line 151
  11. lemma OAI.RVM.conePotential_tip_flux line 167
  12. lemma OAI.RVM.conePotential_spatial_ibp line 185