OAI/Analysis/VlasovMaxwell/Population/RetardedSameTimeSeparation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.retarded_same_time_separation line 35
  2. lemma OAI.RVM.velocity_ref_triangle line 54
  3. lemma OAI.RVM.relative_ref_triangle line 63
  4. lemma OAI.RVM.PhaseFlowOn.retarded_stable_cell_occupation line 69
  5. lemma OAI.RVM.exists_axis_basis line 154
  6. lemma OAI.RVM.volume_axis_box line 173
  7. lemma OAI.RVM.volume_velocity_cap line 195
  8. lemma OAI.RVM.lintegral_velocity_cap_density line 220
  9. lemma OAI.RVM.sphere_cap_area line 232
  10. lemma OAI.RVM.norm_sub_le_of_deficit line 263
  11. def OAI.RVM.coneBinMomentumSet line 301
  12. lemma OAI.RVM.measurableSet_coneBinMomentumSet line 305
  13. lemma OAI.RVM.coneBinMomentumSet_subset_cap line 313
  14. lemma OAI.RVM.coneBin_density_bound line 329
  15. lemma OAI.RVM.coneBin_density_small_bound line 346
  16. lemma OAI.RVM.receiver_bin_area line 362
  17. lemma OAI.RVM.PhaseFlowOn.particle_uniform_bound line 375
  18. def OAI.RVM.physicalBinDensity line 392
  19. lemma OAI.RVM.PhaseFlowOn.physicalBinDensity_bounds line 397
  20. abbrev OAI.RVM.ConeCoordinate line 409
  21. def OAI.RVM.physicalBinBase line 411
  22. def OAI.RVM.physicalBinMeasure line 416
  23. lemma OAI.RVM.measurableSet_physicalBinBase line 419
  24. lemma OAI.RVM.physicalBinMeasure_volume line 433