OAI/Analysis/VlasovMaxwell/LocalPDE/PicardCurvature.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.uniform_physical_integrand_curvature line 18
  2. lemma OAI.RVM.uniform_physical_integral_curvature line 42
  3. lemma OAI.RVM.CurvatureBound.cross_const_left line 78
  4. lemma OAI.RVM.uniform_retarded_density_curvature line 85
  5. lemma OAI.RVM.boundary_integral_curvature line 120
  6. lemma OAI.RVM.mixed_fields_curvature line 143
  7. def OAI.RVM.SpatialFieldCurvature line 173
  8. def OAI.RVM.PhaseParticleCurvature line 176
  9. theorem OAI.RVM.uniform_picard_sequence_curvature line 179
  10. lemma OAI.RVM.FieldControl.spatialJetBound_one line 271
  11. lemma OAI.RVM.particleJetBound_one line 287
  12. theorem OAI.RVM.uniform_picard_sequence_jets line 298
  13. lemma OAI.RVM.hasFDerivWithinAt_uniform_limit_convex line 383
  14. lemma OAI.RVM.continuous_spatial_fderiv line 409
  15. def OAI.RVM.curlMap line 420
  16. lemma OAI.RVM.curl_eq_curlMap line 427
  17. def OAI.RVM.divMap line 437
  18. lemma OAI.RVM.divergence_eq_divMap line 443
  19. lemma OAI.RVM.fderiv_spatial_slice line 453
  20. def OAI.RVM.assembleDerivative line 459
  21. lemma OAI.RVM.fderiv_eq_assemble line 464
  22. lemma OAI.RVM.uniform_assembleDerivative line 476
  23. lemma OAI.RVM.uniform_clm_apply_bounded line 487
  24. lemma OAI.RVM.c1_slab_uniform_derivative line 523
  25. lemma OAI.RVM.picard_field_full_derivative_limit line 543