OAI/Analysis/VlasovMaxwell/Population/GoodSharedEstimates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Admissible.representative_regular_good_shared line 16
  2. def OAI.RVM.goodInverseHalfConstant line 33
  3. lemma OAI.RVM.goodInverseHalfConstant_pos line 34
  4. lemma OAI.RVM.capped_inverse_half_floor_sum line 38
  5. lemma OAI.RVM.capped_inverse_half_floor_tsum line 51
  6. lemma OAI.RVM.good_shared_sqrt_balance line 66
  7. lemma OAI.RVM.good_shared_time_comparison line 75
  8. lemma OAI.RVM.capped_half_tail_sum line 92
  9. lemma OAI.RVM.capped_floor_count_half line 107
  10. lemma OAI.RVM.good_exception_model_sum line 120
  11. def OAI.RVM.representativeExceptionGoodCost line 172
  12. lemma OAI.RVM.good_cost_eq_regular_add_exception line 176
  13. lemma OAI.RVM.Admissible.good_exception_triple_sum line 184
  14. lemma OAI.RVM.Admissible.good_regular_radial line 235
  15. lemma OAI.RVM.Admissible.good_regular_double_sum line 281
  16. lemma OAI.RVM.Admissible.good_regular_uniform line 341
  17. lemma OAI.RVM.sourceRepresentative_twohalf_sum line 417
  18. lemma OAI.RVM.Admissible.good_exception_uniform line 432
  19. lemma OAI.RVM.good_exception_time_comparison line 498
  20. lemma OAI.RVM.Admissible.small_good_uniform line 514