OAI/Analysis/VlasovMaxwell/Regularity/VelocityDerivatives.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.RVM.bounded_iteratedFDeriv_of_factorline 12 - def
OAI.RVM.velocityAugmentline 50 - def
OAI.RVM.velocityJetline 52 - lemma
OAI.RVM.velocityAugment_smoothline 56 - lemma
OAI.RVM.velocityJet_smoothline 59 - lemma
OAI.RVM.velocityAugment_derivline 66 - theorem
OAI.RVM.velocity_derivatives_boundedline 83