OAI/Analysis/VlasovMaxwell/Population/DirectionOverlap.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.SmoothClassicalPrefix.energyPrefix line 38
  2. lemma OAI.RVM.physicalPhaseForce_cutoff line 53
  3. lemma OAI.RVM.SmoothClassicalPrefix.retarded_force_phase_domain line 58
  4. lemma OAI.RVM.SmoothClassicalPrefix.retarded_force_label_integral line 80
  5. lemma OAI.RVM.SmoothClassicalPrefix.exists_phaseFlowOn line 98
  6. def OAI.RVM.DirectionOverlap line 110
  7. instance OAI.RVM.(instance at line 113) line 113
  8. lemma OAI.RVM.directionOverlap_card_le line 118
  9. lemma OAI.RVM.refined_direction_hit_duration line 154
  10. lemma OAI.RVM.retarded_boundary_hit_duration line 210
  11. lemma OAI.RVM.PhaseFlowOn.refined_direction_occupation line 230
  12. lemma OAI.RVM.velocity_direction_deficit line 305
  13. lemma OAI.RVM.velocity_change_of_direction line 328
  14. lemma OAI.RVM.refined_direction_hit_duration_of_hits line 345
  15. lemma OAI.RVM.relative_velocity_direction_cell line 400
  16. lemma OAI.RVM.direction_good_hit_separation line 429
  17. lemma OAI.RVM.PhaseFlowOn.direction_closed_bin_hit_separation line 457
  18. lemma OAI.RVM.PhaseFlowOn.direction_good_hit_duration line 488
  19. lemma OAI.RVM.receiver_cells_good_or_bad line 564
  20. lemma OAI.RVM.PhaseFlowOn.direction_total_hit_duration line 574