OAI/Analysis/VlasovMaxwell/Population/GoodCrossings.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Admissible.representative_good_central line 14
  2. lemma OAI.RVM.capped_sqrt_min_sum line 99
  3. lemma OAI.RVM.magnetic_shared_radial_sum line 146
  4. lemma OAI.RVM.good_central_near_scalar line 172
  5. lemma OAI.RVM.good_central_far_scalar line 186
  6. lemma OAI.RVM.good_central_near_ennreal line 202
  7. lemma OAI.RVM.good_central_far_ennreal line 213
  8. def OAI.RVM.representativeRegularGoodCost line 224
  9. lemma OAI.RVM.Admissible.representative_regular_good line 230
  10. lemma OAI.RVM.capped_negative_power_sum line 295
  11. lemma OAI.RVM.capped_inverse_head_sum line 330
  12. lemma OAI.RVM.capped_balance_sum line 345
  13. lemma OAI.RVM.scaled_capped_crossing_sum line 364
  14. lemma OAI.RVM.good_structural_radial_sum line 418
  15. lemma OAI.RVM.structural_angle_tsum_le line 447
  16. lemma OAI.RVM.Admissible.representative_regular_good_structural_double_sum line 477
  17. lemma OAI.RVM.small_pair_source_sum line 533
  18. lemma OAI.RVM.small_pair_I_source_sum line 561
  19. lemma OAI.RVM.Admissible.good_regular_structural_uniform line 587
  20. lemma OAI.RVM.Admissible.representative_good_near line 667
  21. def OAI.RVM.representativeLowShortGoodCost line 695
  22. lemma OAI.RVM.good_low_coefficient line 701
  23. lemma OAI.RVM.Admissible.representative_low_good_structural_triple_sum line 723
  24. lemma OAI.RVM.Admissible.good_low_uniform line 799
  25. lemma OAI.RVM.Admissible.good_structural_uniform line 880
  26. lemma OAI.RVM.crossing_bound_normalised line 963
  27. lemma OAI.RVM.scaled_capped_crossing_normalised line 982
  28. lemma OAI.RVM.scaled_two_level_crossing_sum line 992
  29. lemma OAI.RVM.spatial_crossing_scale line 1042
  30. lemma OAI.RVM.spatial_crossing_normalisation line 1050
  31. lemma OAI.RVM.spatial_transition_double_sum line 1091