OAI/Analysis/VlasovMaxwell/Regularity/RealJointEnergyBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RVM.realJointEnergyBudget line 37
2. lemma OAI.RVM.PhaseFlowOn.realJointEnergyBudget_summable line 41
3. lemma OAI.RVM.PhaseFlowOn.realJointEnergyBudget_uniform line 47
4. lemma OAI.RVM.sum_cell_lintegral_le line 63
5. lemma OAI.RVM.PhaseFlowOn.averaged_cells_occupation line 74
6. lemma OAI.RVM.relative_angle_identity line 112
7. lemma OAI.RVM.actual_relative_separation line 119
8. lemma OAI.RVM.actual_small_sector_velocity line 130
9. lemma OAI.RVM.stopping_modulus_on_stability_scale line 153
10. lemma OAI.RVM.IncrementBootstrap.velocity_stability_scale line 198