OAI/Analysis/VlasovMaxwell/Regularity/IntegralBallPolarFlip.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.integral_ball_polar_flip line 37
2. lemma OAI.RVM.normalisedSignedForce_flux line 65
3. lemma OAI.RVM.coneRadius_sub_smul line 75
4. lemma OAI.RVM.coneDirection_sub_smul line 79
5. lemma OAI.RVM.retardedForceKernel_polar_normalised line 84
6. lemma OAI.RVM.classical_retarded_force_polar_before line 96
7. lemma OAI.RVM.sourceAcceleration_cutoff line 125
8. lemma OAI.RVM.SmoothClassicalPrefix.retarded_force_polar line 131
9. lemma OAI.RVM.integral_Ioo_reflect line 160
10. lemma OAI.RVM.SmoothClassicalPrefix.retarded_force_source_polar line 167