OAI/Analysis/VlasovMaxwell/Continuation/IncrementBootstrap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.norm_fderiv_q_le line 30
  2. lemma OAI.RVM.q_lipschitz line 38
  3. lemma OAI.RVM.norm_relativistic_projection_le line 44
  4. lemma OAI.RVM.norm_fderiv_velocity_le line 54
  5. lemma OAI.RVM.velocity_local_lipschitz line 62
  6. lemma OAI.RVM.continuous_barrier line 79
  7. lemma OAI.RVM.momentum_stopping line 111
  8. lemma OAI.RVM.one_le_q line 128
  9. def OAI.RVM.IncrementBootstrap line 133
  10. lemma OAI.RVM.IncrementBootstrap.stopped_forward line 138
  11. lemma OAI.RVM.IncrementBootstrap.velocity_stopped_forward line 177