OAI/Analysis/VlasovMaxwell/Population/MajorantRelativeDensityTimeFar.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.majorant_relative_density_time_far_sqrt line 15
2. lemma OAI.RVM.majorant_relative_large_magnetic_cauchy_scalar line 28
3. lemma OAI.RVM.Admissible.source_majorant_large_radius line 94
4. lemma OAI.RVM.majorant_capped_large_magnetic_ennreal_sum line 161
5. lemma OAI.RVM.majorant_remaining_good_coarse_balance line 210
6. lemma OAI.RVM.Admissible.source_majorant_remaining_large_sum line 237
7. lemma OAI.RVM.majorant_capped_short_sqrt_radius_sum line 321
8. lemma OAI.RVM.Admissible.source_majorant_short_near_sum line 349
9. lemma OAI.RVM.majorant_deficit_short_source_coefficient line 391
10. lemma OAI.RVM.majorant_shortSqrtConstant_pos line 436
11. lemma OAI.RVM.Admissible.source_majorant_deficit_short_sum line 441
12. lemma OAI.RVM.majorant_relativeCauchyConstant_energy_le line 476
13. lemma OAI.RVM.majorant_remaining_stability_sqrt_coarse line 499
14. lemma OAI.RVM.Admissible.source_majorant_remaining_all_radii line 530