OAI/Analysis/VlasovMaxwell/Continuation/GlobalContinuation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.SmoothClassicalPrefix.particle_bound_datum line 22
  2. lemma OAI.RVM.physical_field_integral_bound line 30
  3. lemma OAI.RVM.physical_fields_volterra line 40
  4. lemma OAI.RVM.bounded_momentum_field_bound line 99
  5. lemma OAI.RVM.ClassicalBefore.mono line 116
  6. lemma OAI.RVM.log_one_add_mul_exp_le line 121
  7. lemma OAI.RVM.integral_lorentz_coefficient_bound line 130
  8. lemma OAI.RVM.classical_electric_log_closed_bound line 146
  9. lemma OAI.RVM.classical_magnetic_log_closed_bound line 185
  10. lemma OAI.RVM.classical_fields_gradient_current_volterra line 224
  11. lemma OAI.RVM.component_le_double_sum line 264
  12. lemma OAI.RVM.prefix_spatial_gradient_volterra line 269
  13. lemma OAI.RVM.bounded_momentum_field_gradient_bound line 389
  14. lemma OAI.RVM.bounded_momentum_particle_lipschitz_bound line 416
  15. lemma OAI.RVM.bounded_momentum_particle_gradient_bound line 465
  16. def OAI.RVM.secondJetSum line 480
  17. lemma OAI.RVM.secondJetSum_nonneg line 485
  18. lemma OAI.RVM.prefix_second_jet_volterra line 488
  19. lemma OAI.RVM.bounded_momentum_second_jet_bound line 646
  20. lemma OAI.RVM.family_datum_restart_control line 682
  21. theorem OAI.RVM.family_bounded_classical_prefix line 744
  22. lemma OAI.RVM.SmoothClassicalPrefix.spatial_support_datum line 761
  23. theorem OAI.RVM.bounded_momentum_uniform_restart line 780
  24. theorem OAI.RVM.bounded_momentum_arbitrarily_long_prefix line 857
  25. lemma OAI.RVM.time_slab_mem_nhdsWithin line 885
  26. lemma OAI.RVM.contDiffOn_halfspace_of_slabs line 893
  27. lemma OAI.RVM.timeContinuousL2_of_slabs line 904
  28. theorem OAI.RVM.global_classical_of_arbitrarily_long_prefixes line 928
  29. theorem OAI.RVM.global_classical_of_uniform_prefix_momentum line 1010
  30. theorem OAI.RVM.global_classical_of_uniform_physical_increment line 1030