OAI/Analysis/VlasovMaxwell/Continuation/Bootstrap.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.first_level_time line 32
  2. lemma OAI.RVM.last_level_time line 60
  3. lemma OAI.RVM.first_level_bound line 85
  4. lemma OAI.RVM.first_levels_strict line 92
  5. def OAI.RVM.PopulationIncrement line 102
  6. theorem OAI.RVM.momentum_bounded_of_increment line 108
  7. def OAI.RVM.incrementBound line 228
  8. lemma OAI.RVM.incrementBound_nonneg line 231
  9. lemma OAI.RVM.incrementBound_mono line 235
  10. lemma OAI.RVM.continuous_incrementBound line 241
  11. lemma OAI.RVM.IncrementBootstrap.ramp_error line 245
  12. lemma OAI.RVM.supported_weight_integral_eq line 266
  13. lemma OAI.RVM.closure_coefficient_bound line 275
  14. lemma OAI.RVM.PhaseFlowOn.physical_cap_of_labels line 294
  15. lemma OAI.RVM.Admissible.signed_increment_strict line 305
  16. lemma OAI.RVM.signed_bootstrap_propagation line 411
  17. def OAI.RVM.PhaseFlowOn.restrict line 516
  18. lemma OAI.RVM.SmoothClassicalPrefix.restrict line 527
  19. lemma OAI.RVM.PhaseFlowOn.supported_momentum_lipschitz line 547
  20. lemma OAI.RVM.Admissible.uniform_signed_increment line 584
  21. lemma OAI.RVM.Admissible.population_increment line 608