OAI/Analysis/VlasovMaxwell/Continuation/DerivMovingEnergy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.EnergyPrefix.deriv_moving_energy line 30
2. lemma OAI.RVM.EnergyPrefix.coneShellFlux_nonneg line 119
3. lemma OAI.RVM.EnergyPrefix.deriv_cone_energy line 139
4. lemma OAI.RVM.EnergyPrefix.particle_flux_continuous_slab line 157
5. lemma OAI.RVM.EnergyPrefix.total_flux_continuous_slab line 176
6. lemma OAI.RVM.EnergyPrefix.coneShellFlux_continuous_slab line 183
7. lemma OAI.RVM.EnergyPrefix.coneShellFlux_integral_continuous line 194
8. lemma OAI.RVM.EnergyPrefix.cone_energy_continuous line 202
9. lemma OAI.RVM.EnergyPrefix.coneShellFlux_bound line 212
10. lemma OAI.RVM.EnergyPrefix.continuous_radialConeProfile line 245
11. lemma OAI.RVM.EnergyPrefix.continuous_spherical_radialConeProfile line 262
12. lemma OAI.RVM.EnergyPrefix.coneShellFlux_polar line 271
13. lemma OAI.RVM.EnergyPrefix.coneShellFlux_tendsto line 311
14. lemma OAI.RVM.EnergyPrefix.light_cone_flux line 322
15. lemma OAI.RVM.EnergyPrefix.null_cone_flux line 360
16. lemma OAI.RVM.EnergyPrefix.particle_cone_identity line 368
17. lemma OAI.RVM.EnergyPrefix.particle_cone_nonneg line 394
18. lemma OAI.RVM.EnergyPrefix.goodConeDensity_bounds line 401
19. lemma OAI.RVM.EnergyPrefix.goodConeDensity_continuousOn line 413
20. lemma OAI.RVM.EnergyPrefix.goodConeDensity_cone_continuous line 439
21. lemma OAI.RVM.EnergyPrefix.nullConeFlux_sphere_continuous line 457
22. lemma OAI.RVM.EnergyPrefix.goodConeDensity_sphere_integral_bound line 469
23. lemma OAI.RVM.EnergyPrefix.goodConeDensity_time_integral_bound line 484
24. theorem OAI.RVM.EnergyPrefix.good_cone_energy line 511