OAI/Analysis/VlasovMaxwell/LocalPDE/SlabEquations.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RVM.SlabEquations line 16
2. lemma OAI.RVM.derivWithin_slab_assemble line 29
3. lemma OAI.RVM.slab_equations_of_derivatives line 41
4. lemma OAI.RVM.local_c1_limit_of_picard line 77
5. theorem OAI.RVM.exists_local_c1_core line 104
6. structure OAI.RVM.C1ClassicalPrefix line 155
7. lemma OAI.RVM.derivWithin_Ici_eq_Icc_of_lt line 168
8. lemma OAI.RVM.SlabEquations.equationsBefore line 176
9. lemma OAI.RVM.LocalParticleBound.compact line 181
10. theorem OAI.RVM.exists_local_classical_prefix line 192
11. lemma OAI.RVM.C1ClassicalPrefix.energyPrefix line 200