OAI/Analysis/VlasovMaxwell/Population/MagneticEstimates.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.direct_magnetic_near_ennreal line 14
2. lemma OAI.RVM.direct_magnetic_far_ennreal line 27
3. lemma OAI.RVM.Admissible.representative_magnetic_short_Cauchy line 41
4. lemma OAI.RVM.Admissible.representative_magnetic_short_central line 150
5. lemma OAI.RVM.magnetic_central_near_scalar line 264
6. lemma OAI.RVM.magnetic_central_far_scalar line 280
7. lemma OAI.RVM.magnetic_central_near_ennreal line 296
8. lemma OAI.RVM.magnetic_central_far_ennreal line 307
9. def OAI.RVM.representativeRegularShortMagneticCost line 318
10. lemma OAI.RVM.Admissible.representative_regular_short_magnetic line 324
11. lemma OAI.RVM.Admissible.representative_regular_short_magnetic_double_sum line 389
12. lemma OAI.RVM.Admissible.magnetic_regular_short_uniform line 455
13. lemma OAI.RVM.Admissible.representative_magnetic_short_near line 525
14. def OAI.RVM.representativeLowShortMagneticCost line 553
15. lemma OAI.RVM.Admissible.representative_low_magnetic_triple_sum line 559
16. lemma OAI.RVM.Admissible.magnetic_low_uniform line 627
17. lemma OAI.RVM.Admissible.magnetic_small_short_uniform line 708
18. lemma OAI.RVM.Admissible.representative_magnetic_large_Cauchy line 796
19. lemma OAI.RVM.Admissible.representative_magnetic_large line 933
20. def OAI.RVM.representativeLargeMagneticCost line 964
21. lemma OAI.RVM.capped_large_magnetic_weighted_sum line 969
22. lemma OAI.RVM.capped_rpow_ennreal_sum line 1005
23. lemma OAI.RVM.capped_rpow_sum_constant_pos line 1016
24. lemma OAI.RVM.large_magnetic_triple_sum line 1020
25. lemma OAI.RVM.Admissible.representative_large_magnetic_triple_sum line 1049
26. lemma OAI.RVM.Admissible.magnetic_large_uniform line 1092
27. lemma OAI.RVM.Admissible.magnetic_small_uniform line 1154
28. lemma OAI.RVM.PhaseFlowOn.bulkSource_cost_sum line 1231
29. lemma OAI.RVM.Admissible.bulk_source_uniform line 1266