OAI/Analysis/VlasovMaxwell/Flow/PhaseHits.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.lintegral_radial_measure line 31
2. lemma OAI.RVM.lintegral_polar line 42
3. lemma OAI.RVM.PhaseFlowOn.receiver_lintegral line 65
4. lemma OAI.RVM.PhaseFlowOn.lintegral_comp line 92
5. lemma OAI.RVM.label_hit_tonelli line 101
6. lemma OAI.RVM.PhaseFlowOn.transport_weight_lintegral line 122
7. def OAI.RVM.phaseHits line 132
8. lemma OAI.RVM.PhaseFlowOn.measurable_phaseHits line 135
9. lemma OAI.RVM.PhaseFlowOn.phase_occupation_identity line 152