OAI/Analysis/VlasovMaxwell/Retarded/AngularBump.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.momentumDirection_increment line 38
2. lemma OAI.RVM.norm_momentum_of_high_band line 54
3. lemma OAI.RVM.IncrementBootstrap.direction_increment line 61
4. lemma OAI.RVM.sqrt_linear_small line 87
5. lemma OAI.RVM.IncrementBootstrap.finite_direction_stops line 96
6. def OAI.RVM.angularZeroBump line 122
7. def OAI.RVM.extendedAngularCLM line 125
8. lemma OAI.RVM.extendedAngularCLM_contDiff line 128
9. lemma OAI.RVM.extendedAngularCLM_eq line 144
10. lemma OAI.RVM.extendedAngularCLM_eventuallyEq line 149
11. lemma OAI.RVM.hasDerivAt_extendedAngularCLM line 155
12. lemma OAI.RVM.extendedAngularCLM_fderiv line 161