OAI/Analysis/VlasovMaxwell/Regularity/PhysicalGradient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.source_density_integrable line 15
2. lemma OAI.RVM.retardedElectricDensity_split line 40
3. lemma OAI.RVM.Magnetic.source_density_integrable line 79
4. lemma OAI.RVM.Magnetic.retardedMagneticDensity_split line 104
5. lemma OAI.RVM.classical_electric_transport_source_before line 140
6. lemma OAI.RVM.Magnetic.classical_magnetic_transport_source_before line 174
7. lemma OAI.RVM.hasDerivAt_vec_component_line line 208
8. lemma OAI.RVM.classical_electric_gradient_bound line 218
9. lemma OAI.RVM.Magnetic.classical_magnetic_gradient_bound line 272
10. lemma OAI.RVM.classical_electric_gradient_volterra_bound line 329
11. lemma OAI.RVM.Magnetic.classical_magnetic_gradient_volterra_bound line 390