OAI/Analysis/VlasovMaxwell/LocalPDE/PicardBoundary.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.coordinate_fderiv_apply line 12
  2. lemma OAI.RVM.BoundedSmooth.coordinate_bounds line 17
  3. lemma OAI.RVM.freeWave_bound_global line 48
  4. lemma OAI.RVM.BoundedSmooth.freeWave_coordinate_bound line 75
  5. lemma OAI.RVM.electricConeBoundary_datum_bound_global line 105
  6. lemma OAI.RVM.magneticConeBoundary_datum_bound_global line 151
  7. lemma OAI.RVM.datum_boundary_global_bound line 204
  8. lemma OAI.RVM.smooth_compact_lipschitz line 247
  9. lemma OAI.RVM.BoundedSmooth.iterated_lipschitz line 258
  10. lemma OAI.RVM.BoundedSmooth.spatial_lipschitz line 271
  11. lemma OAI.RVM.uniform_datum_velocity_integral_lipschitz line 309
  12. lemma OAI.RVM.abs_sphere_integral_sub_le line 344
  13. lemma OAI.RVM.waveK_lipschitz line 350
  14. lemma OAI.RVM.freeWave_lipschitz line 365
  15. lemma OAI.RVM.datum_moment_lipschitz line 401
  16. lemma OAI.RVM.BoundedSmooth.freeWave_coordinate_lipschitz line 418
  17. lemma OAI.RVM.datum_sphere_flux_lipschitz line 456
  18. lemma OAI.RVM.weighted_sphere_mean_lipschitz line 486
  19. lemma OAI.RVM.datum_initial_electric_flux_normalised line 505
  20. lemma OAI.RVM.datum_initial_magnetic_flux_normalised line 513
  21. lemma OAI.RVM.electricConeBoundary_datum_lipschitz line 521
  22. lemma OAI.RVM.magneticConeBoundary_datum_lipschitz line 554
  23. lemma OAI.RVM.datum_boundary_global_lipschitz line 602