OAI/Analysis/VlasovMaxwell/LocalPDE/SlabRHS.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RVM.crossBilinearCLM line 12
2. lemma OAI.RVM.spatialJetRegular_lorentz line 20
3. def OAI.RVM.slabParticleRHS line 29
4. def OAI.RVM.slabElectricRHS line 31
5. def OAI.RVM.slabMagneticRHS line 33
6. lemma OAI.RVM.slabParticleRHS_regular line 36
7. lemma OAI.RVM.slabMagneticRHS_regular line 41
8. lemma OAI.RVM.compact_particle_velocity_bound line 45
9. lemma OAI.RVM.spatialJetRegular_current line 60
10. lemma OAI.RVM.slabElectricRHS_regular line 85