OAI/Analysis/VlasovMaxwell/Flow/PhaseTimePullback.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RVM.phaseTimePullback line 38
2. lemma OAI.RVM.PhaseFlowOn.measurable_phaseTimePullback line 42
3. lemma OAI.RVM.PhaseFlowOn.lintegral_phaseTimePullback line 55
4. lemma OAI.RVM.PhaseFlowOn.phaseTimePullback_integrable_iff line 75
5. lemma OAI.RVM.PhaseFlowOn.integral_phaseTimePullback line 101
6. lemma OAI.RVM.PhaseFlowOn.arrival_polar_mem line 126
7. lemma OAI.RVM.PhaseFlowOn.arrival_polar_time line 150
8. lemma OAI.RVM.PhaseFlowOn.arrival_polar_radius line 166
9. lemma OAI.RVM.PhaseFlowOn.arrival_polar_direction line 173
10. def OAI.RVM.arrivalInverseSquare line 180
11. lemma OAI.RVM.PhaseFlowOn.measurable_arrivalInverseSquare line 183
12. lemma OAI.RVM.arrivalInverseSquare_nonneg line 194
13. lemma OAI.RVM.PhaseFlowOn.arrivalInverseSquare_lintegral line 199
14. lemma OAI.RVM.PhaseFlowOn.arrivalInverseSquare_integrable line 243
15. def OAI.RVM.phaseArrivalMajorant line 281
16. lemma OAI.RVM.PhaseFlowOn.measurable_phaseArrivalMajorant line 285
17. lemma OAI.RVM.phaseArrivalMajorant_nonneg line 292
18. lemma OAI.RVM.PhaseFlowOn.phaseArrivalMajorant_integrable line 297
19. lemma OAI.RVM.PhaseFlowOn.source_cone_integrable_of_bound line 306