OAI/Analysis/VlasovMaxwell/Population/NullConeFlux.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.sphere_neg_preserving line 20
  2. lemma OAI.RVM.integral_sphere_neg line 37
  3. def OAI.RVM.nullConeFlux line 42
  4. lemma OAI.RVM.nullConeFlux_spherical_eq line 46
  5. lemma OAI.RVM.classical_null_cone_flux line 57
  6. lemma OAI.RVM.classical_particle_cone_identity line 65
  7. lemma OAI.RVM.classical_particle_cone_nonneg line 91
  8. def OAI.RVM.goodConeDensity line 98
  9. lemma OAI.RVM.goodConeDensity_bounds line 102
  10. lemma OAI.RVM.goodConeDensity_continuousOn line 114
  11. lemma OAI.RVM.goodConeDensity_cone_continuous line 140
  12. lemma OAI.RVM.nullConeFlux_sphere_continuous line 158
  13. lemma OAI.RVM.goodConeDensity_sphere_integral_bound line 170
  14. lemma OAI.RVM.goodConeDensity_time_integral_bound line 185
  15. theorem OAI.RVM.classical_good_cone_energy line 212
  16. def OAI.RVM.velocityProjection line 230
  17. def OAI.RVM.goodField line 232
  18. lemma OAI.RVM.velocityProjection_add line 234
  19. lemma OAI.RVM.velocityProjection_norm line 239
  20. lemma OAI.RVM.velocityProjection_dot_symm line 250
  21. lemma OAI.RVM.norm_velocityProjection_normal line 256
  22. lemma OAI.RVM.cross_sub_left line 271
  23. lemma OAI.RVM.cross_sub_right line 275
  24. lemma OAI.RVM.cross_self line 279
  25. lemma OAI.RVM.cross_normal_decomposition line 283
  26. lemma OAI.RVM.magnetic_projection_identity line 289
  27. lemma OAI.RVM.magnetic_projection_normal_identity line 310
  28. lemma OAI.RVM.abs_dot_le line 320
  29. lemma OAI.RVM.velocity_normal_distance_bound line 324
  30. lemma OAI.RVM.source_energy_rate_bound line 333
  31. lemma OAI.RVM.magnetic_projection_bound line 352
  32. lemma OAI.RVM.lorentz_source_acceleration_bound line 390
  33. lemma OAI.RVM.lorentz_source_normal_acceleration_bound line 409