OAI/Analysis/VlasovMaxwell/Population/SelectionCounts.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.representativeGoodCost line 14
  2. lemma OAI.RVM.Admissible.representative_good_Cauchy line 27
  3. lemma OAI.RVM.direct_good_near_scalar line 112
  4. lemma OAI.RVM.direct_good_far_sqrt line 130
  5. lemma OAI.RVM.direct_good_far_scalar line 141
  6. lemma OAI.RVM.direct_good_near_ennreal line 163
  7. lemma OAI.RVM.direct_good_far_ennreal line 174
  8. def OAI.RVM.selectionDecay line 189
  9. lemma OAI.RVM.selectionDecay_pos line 191
  10. lemma OAI.RVM.selectionDecay_lt_one line 192
  11. lemma OAI.RVM.selectionDecay_pow line 195
  12. lemma OAI.RVM.cappedRepresentative_selection_pow line 201
  13. lemma OAI.RVM.sourceRepresentative_two_pow line 209
  14. lemma OAI.RVM.selection_angle_index line 213
  15. lemma OAI.RVM.selectionWeight_gap_bound line 224
  16. lemma OAI.RVM.sum_selectionDecay line 247
  17. lemma OAI.RVM.sum_selectionDecay_box line 253
  18. lemma OAI.RVM.sum_selectionDecay_finset line 267
  19. lemma OAI.RVM.sum_selectionWeight line 273
  20. lemma OAI.RVM.source_ratio_sq_le line 319
  21. lemma OAI.RVM.source_ratio_sq_sum line 327
  22. lemma OAI.RVM.pair_source_ratio_sq_sum line 348
  23. lemma OAI.RVM.joint_budget_Cauchy line 396
  24. lemma OAI.RVM.joint_budget_weighted_Cauchy line 419
  25. lemma OAI.RVM.shared_weighted_pair_Cauchy line 441
  26. def OAI.RVM.pairCountConstant line 458
  27. lemma OAI.RVM.pairCountConstant_pos line 459
  28. lemma OAI.RVM.exists_small_pair_count line 464
  29. lemma OAI.RVM.small_pair_cardinals line 482
  30. lemma OAI.RVM.angle_sqrt_factor line 502
  31. lemma OAI.RVM.shared_radius_expansion line 512
  32. lemma OAI.RVM.source_receiver_pair_sum line 529
  33. lemma OAI.RVM.paired_count_Cauchy_factors line 560
  34. lemma OAI.RVM.shared_radius_pair_sum line 577
  35. lemma OAI.RVM.Admissible.representative_good_envelope line 647
  36. def OAI.RVM.representativeSelected line 735
  37. def OAI.RVM.representativeSmallSector line 744
  38. lemma OAI.RVM.selectionWeight_nonneg line 749
  39. lemma OAI.RVM.selection_weighted_tsum line 752
  40. lemma OAI.RVM.Admissible.unselected_good_uniform line 778
  41. lemma OAI.RVM.small_power_four line 817
  42. lemma OAI.RVM.small_negative_power_four line 826
  43. lemma OAI.RVM.selectionWeight_neighbor line 834
  44. lemma OAI.RVM.selected_neighbor_near_lower line 867