OAI/Analysis/VlasovMaxwell/Maxwell/FieldGradientNorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.curl_norm_le_gradient line 13
2. lemma OAI.RVM.full_field_derivative_bound line 28
3. lemma OAI.RVM.current_norm_bound_of_momentum line 53
4. lemma OAI.RVM.maxwell_full_derivative_bound line 66
5. lemma OAI.RVM.spatial_field_lipschitz_of_gradient line 104
6. lemma OAI.RVM.norm_clm_le_nine_components line 110