OAI/Analysis/VlasovMaxwell/Retarded/SourceVelocityProfile.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.Magnetic.source_dynamic_spatial_divergence_bound line 13
2. lemma OAI.RVM.Magnetic.retarded_spacetime_lipschitz line 50
3. lemma OAI.RVM.Magnetic.norm_fderiv_retarded_fields line 60
4. lemma OAI.RVM.Magnetic.physical_source_spatial_bound line 79
5. def OAI.RVM.Magnetic.sourceVelocityProfile line 107
6. lemma OAI.RVM.Magnetic.sourceVelocityProfile_contDiffAt line 112
7. lemma OAI.RVM.Magnetic.continuousOn_sourceVelocityDivergence line 127
8. lemma OAI.RVM.Magnetic.sourceVelocityDivergence_uniform_bound line 141
9. lemma OAI.RVM.Magnetic.source_velocity_divergence_rescale line 160
10. lemma OAI.RVM.Magnetic.physical_source_velocity_bound line 179