OAI/Analysis/VlasovMaxwell/Population/LabelOccupation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.PhaseFlowOn.receiver_integrable line 31
2. lemma OAI.RVM.PhaseFlowOn.receiver_polar_integral line 51
3. def OAI.RVM.labelOccupation line 92
4. lemma OAI.RVM.PhaseFlowOn.label_occupation_rate_bound line 95
5. def OAI.RVM.branchDirection line 122
6. lemma OAI.RVM.PhaseFlowOn.branchDirection_norm line 126
7. lemma OAI.RVM.PhaseFlowOn.branchRate_pos line 136
8. lemma OAI.RVM.PhaseFlowOn.branchRate_lower_bound line 146
9. lemma OAI.RVM.PhaseFlowOn.label_occupation_angular_bound line 166