OAI/Analysis/VlasovMaxwell/Retarded/PhysicalProjectedRemainderDensity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.angularMultiplierCLM_highband_transverse line 39
2. lemma OAI.RVM.signedRemainder_projected_norm line 47
3. def OAI.RVM.physicalProjectedRemainderDensity line 94
4. lemma OAI.RVM.physicalProjectedRemainderDensity_bound line 104
5. lemma OAI.RVM.physicalProjectedRemainder_integral_bound line 155
6. lemma OAI.RVM.PhaseFlowOn.projected_remainder_near_far line 186
7. def OAI.RVM.coneReceiverJacobian line 225
8. def OAI.RVM.coneFoot line 228
9. lemma OAI.RVM.measurable_coneFoot line 231
10. lemma OAI.RVM.measurable_coneReceiverJacobian line 236
11. lemma OAI.RVM.PhaseFlowOn.physicalBin_spatial_budget line 243
12. def OAI.RVM.prefixConeMagnetic line 335
13. lemma OAI.RVM.EnergyPrefix.measurable_prefixConeMagnetic line 338
14. lemma OAI.RVM.PhaseFlowOn.physicalBin_magneticField line 344
15. lemma OAI.RVM.Admissible.uniform_actual_magnetic_Cauchy line 403
16. lemma OAI.RVM.magneticFieldBudget_mono line 475
17. lemma OAI.RVM.PhaseFlowOn.physicalBin_magneticField_common line 480
18. lemma OAI.RVM.radial_source_interval_common line 494
19. lemma OAI.RVM.EnergyPrefix.shared_magneticFieldBudget line 502
20. lemma OAI.RVM.projected_source_direct_bin_bound line 548
21. lemma OAI.RVM.projected_source_cutoff_bin_bound line 581
22. lemma OAI.RVM.projected_source_combined_bin_bound line 616
23. def OAI.RVM.physicalProjectedSourceDensity line 634
24. lemma OAI.RVM.physicalProjectedSourceDensity_bound line 650
25. lemma OAI.RVM.physicalProjectedSource_integral_bound line 691
26. lemma OAI.RVM.Admissible.projected_source_two_budget_bound line 756