OAI/Analysis/VlasovMaxwell/LocalPDE/PicardBounds.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.uniform_normalised_physical_kernel line 15
  2. lemma OAI.RVM.uniform_physical_kernel line 54
  3. lemma OAI.RVM.physical_integral_bound line 67
  4. lemma OAI.RVM.uniform_retarded_density_bound line 94
  5. lemma OAI.RVM.kernel_tip_le_on line 132
  6. lemma OAI.RVM.SmoothLorentzFlow.spatial_travel_bound line 149
  7. lemma OAI.RVM.SmoothLorentzFlow.momentum_travel_bound line 157
  8. lemma OAI.RVM.SmoothLorentzFlow.transport_for line 182
  9. lemma OAI.RVM.SmoothLorentzFlow.transport_for_inverse line 196
  10. lemma OAI.RVM.SmoothLorentzFlow.transported_sup_bound line 201
  11. lemma OAI.RVM.SmoothLorentzFlow.transported_phase_bound line 207
  12. lemma OAI.RVM.datum_boundary_uniform_bound line 229
  13. lemma OAI.RVM.mixed_physical_vector line 272
  14. lemma OAI.RVM.scaled_kernel_tip_le_on line 302
  15. lemma OAI.RVM.mixed_fields_bound line 312
  16. structure OAI.RVM.PicardRegular line 354
  17. theorem OAI.RVM.exists_picard_regular line 369
  18. def OAI.RVM.LocalFieldBound line 398
  19. def OAI.RVM.LocalParticleBound line 401
  20. lemma OAI.RVM.datum_particle_bounds line 405
  21. lemma OAI.RVM.PicardRegular.boundary_eq line 417
  22. theorem OAI.RVM.uniform_picard_invariance line 429
  23. theorem OAI.RVM.exists_uniform_picard_sequence line 493