OAI/Analysis/VlasovMaxwell/Geometry/ArrivalDomain.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.EnergyPrefix.mono line 31
  2. lemma OAI.RVM.EnergyPrefix.weighted_phase_integrable line 47
  3. lemma OAI.RVM.EnergyPrefix.phase_energy_lintegral line 68
  4. lemma OAI.RVM.EnergyPrefix.phase_energy_bound line 78
  5. lemma OAI.RVM.PhaseFlowOn.cone_occupation_energy_bound line 91
  6. def OAI.RVM.arrivalDomain line 133
  7. def OAI.RVM.arrivalLabel line 136
  8. def OAI.RVM.arrivalTime line 139
  9. def OAI.RVM.arrivalRadius line 142
  10. def OAI.RVM.arrivalDirection line 145
  11. def OAI.RVM.arrivalVelocity line 148
  12. lemma OAI.RVM.PhaseFlowOn.arrivalLabel_mem line 151
  13. lemma OAI.RVM.PhaseFlowOn.arrivalLabel_continuousAt line 162
  14. lemma OAI.RVM.PhaseFlowOn.isOpen_arrivalDomain line 169
  15. lemma OAI.RVM.PhaseFlowOn.arrival_time_spec line 186
  16. lemma OAI.RVM.PhaseFlowOn.arrivalTime_continuousAt line 198
  17. lemma OAI.RVM.PhaseFlowOn.arrivalRadius_continuousAt line 204
  18. lemma OAI.RVM.PhaseFlowOn.arrivalFlow_continuousAt line 209
  19. lemma OAI.RVM.PhaseFlowOn.arrivalDirection_continuousAt line 218
  20. lemma OAI.RVM.PhaseFlowOn.arrivalVelocity_continuousAt line 225
  21. lemma OAI.RVM.PhaseFlowOn.norm_arrivalDirection line 232
  22. lemma OAI.RVM.PhaseFlowOn.measurable_arrival_zero line 240