OAI/Analysis/VlasovMaxwell/Population/TransportSingularBulk.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.Magnetic.singular_radial_log_bound_norm line 18
2. lemma OAI.RVM.Magnetic.integral_annulus_polar_radial line 31
3. def OAI.RVM.Magnetic.transportSingularBulk line 66
4. lemma OAI.RVM.Magnetic.transportSingularBulk_continuousOn line 69
5. lemma OAI.RVM.Magnetic.transportSingularBulk_shell line 105
6. lemma OAI.RVM.Magnetic.transportSingularBulk_annulus line 152
7. lemma OAI.RVM.Magnetic.physical_transport_annulus_log_bound line 162
8. lemma OAI.RVM.Magnetic.norm_integral_annulus_inverse_sq_le line 192
9. def OAI.RVM.Magnetic.transportVelocityBulk line 220
10. lemma OAI.RVM.Magnetic.transport_velocity_annulus_bound line 225
11. lemma OAI.RVM.Magnetic.transport_velocity_divergence_continuousOn line 264
12. lemma OAI.RVM.Magnetic.shifted_particle_continuousOn line 278
13. lemma OAI.RVM.Magnetic.transport_bulk_split line 287
14. lemma OAI.RVM.Magnetic.transport_sphere_support line 355
15. lemma OAI.RVM.Magnetic.abs_sub_sub_add_le line 370
16. lemma OAI.RVM.Magnetic.magnetic_transport_annulus_gradient_bound line 374
17. lemma OAI.RVM.Magnetic.sourceFixedFlux_uniform_bound line 428
18. lemma OAI.RVM.Magnetic.source_sphere_rescale line 447
19. lemma OAI.RVM.Magnetic.source_sphere_boundary_bound line 470
20. def OAI.RVM.Magnetic.sourceDivisionBulk line 509
21. lemma OAI.RVM.Magnetic.inverse_source_majorant line 515
22. lemma OAI.RVM.Magnetic.source_division_bulk_annulus_bound line 522