OAI/Analysis/VlasovMaxwell/LocalPDE/PicardContraction.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.velocity_global_lipschitz line 17
  2. lemma OAI.RVM.lorentzField_difference_bound line 25
  3. lemma OAI.RVM.gronwallBound_le_exp_linear line 66
  4. lemma OAI.RVM.SmoothLorentzFlow.backward_stability line 78
  5. lemma OAI.RVM.transported_comparison line 113
  6. lemma OAI.RVM.transported_spatial_lipschitz line 134
  7. lemma OAI.RVM.norm_boundary_integral_difference line 150
  8. lemma OAI.RVM.mixed_fields_difference_bound line 166
  9. def OAI.RVM.GlobalFieldBound line 206
  10. def OAI.RVM.SpatialFieldLip line 209
  11. theorem OAI.RVM.uniform_global_picard_invariance line 213
  12. lemma OAI.RVM.uniform_picard_comparison line 280
  13. def OAI.RVM.FieldControl line 312
  14. def OAI.RVM.PhaseParticleLip line 315
  15. theorem OAI.RVM.uniform_picard_control line 318
  16. theorem OAI.RVM.exists_contractive_picard_sequence line 461
  17. lemma OAI.RVM.exists_uniform_limit_geometric line 513
  18. theorem OAI.RVM.exists_picard_field_limit line 533
  19. lemma OAI.RVM.geometric_picard_particle_differences line 562
  20. lemma OAI.RVM.picard_particle_limit line 594
  21. lemma OAI.RVM.picard_field_exterior line 641
  22. lemma OAI.RVM.picard_uniform_limit_exterior line 676