OAI/Analysis/VlasovMaxwell/LocalPDE/RelativeCauchyConstant.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.Admissible.direct_source_relative_radius_budget line 14
2. def OAI.RVM.relativeCauchyConstant line 154
3. lemma OAI.RVM.relativeCauchyConstant_nonneg line 157
4. lemma OAI.RVM.relative_density_near_sqrt line 160
5. lemma OAI.RVM.relative_density_far_sqrt line 171
6. lemma OAI.RVM.relative_radius_cauchy_scalar line 183
7. lemma OAI.RVM.Admissible.direct_source_relative_short_radius line 246
8. lemma OAI.RVM.capped_sqrt_radius_ennreal_sum line 344
9. lemma OAI.RVM.Admissible.direct_source_relative_short_radial_sum line 370
10. lemma OAI.RVM.Admissible.direct_source_remaining_short_sum line 464
11. lemma OAI.RVM.Admissible.direct_source_large_radius_budget line 559
12. lemma OAI.RVM.relative_radius_cauchy_near line 736
13. lemma OAI.RVM.Admissible.direct_source_short_near line 765