OAI/Analysis/VlasovMaxwell/Regularity/TameDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.tame_iteratedFDeriv_comp line 17
2. lemma OAI.RVM.norm_iteratedFDeriv_precomp_contraction line 92
3. lemma OAI.RVM.norm_iteratedFDeriv_pair_le line 100
4. lemma OAI.RVM.bounded_derivatives_comp_on_compact line 113
5. lemma OAI.RVM.tame_comp_on_compact line 137