OAI/Analysis/VlasovMaxwell/Population/SqrtBaselineClippedLength.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.sqrt_baseline_clipped_length line 39
  2. lemma OAI.RVM.stabilityLength_pos line 57
  3. lemma OAI.RVM.direction_clipped_baseline_R_log_bound line 66
  4. lemma OAI.RVM.stability_massScale_identity line 84
  5. lemma OAI.RVM.direction_baseline_R_bound128 line 91
  6. lemma OAI.RVM.direction_baseline_R_log_bound128 line 130
  7. lemma OAI.RVM.direction_clipped_baseline_R_log_bound128 line 143
  8. lemma OAI.RVM.direction_clipped_source_angle_bound line 161
  9. lemma OAI.RVM.direction_source_far_scale line 208
  10. lemma OAI.RVM.remaining_good_angular line 271
  11. lemma OAI.RVM.remaining_magnetic_angular line 303
  12. lemma OAI.RVM.remaining_transport_angular line 334
  13. lemma OAI.RVM.direction_interval_momentum_factor line 362
  14. lemma OAI.RVM.remaining_good_balance_coefficient line 372
  15. lemma OAI.RVM.remaining_magnetic_balance_coefficient line 399
  16. lemma OAI.RVM.remaining_transport_balance_coefficient line 424