OAI/Analysis/VlasovMaxwell/Population/SelectionWeight.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.selected_coefficient_exponent_bound line 14
  2. lemma OAI.RVM.max_growth_bound line 45
  3. lemma OAI.RVM.selected_coefficient_power_table line 55
  4. lemma OAI.RVM.eventually_selection_constants line 123
  5. def OAI.RVM.selectionWeight line 154
  6. def OAI.RVM.receiverCoefficient line 157
  7. def OAI.RVM.stabilityRate line 160
  8. def OAI.RVM.stabilityLength line 163
  9. lemma OAI.RVM.div_stabilityLength line 166
  10. lemma OAI.RVM.sqrt_div_le_small_denominator line 171
  11. lemma OAI.RVM.rpow_min_exponent line 177
  12. lemma OAI.RVM.sqrt_rpow_base line 183
  13. lemma OAI.RVM.stabilityRate_power_bound line 189
  14. lemma OAI.RVM.nat_pow_rpow_base line 223
  15. lemma OAI.RVM.selectionWeight_power line 226
  16. lemma OAI.RVM.receiverCoefficient_power line 243
  17. lemma OAI.RVM.selected_near_far_powers line 255
  18. def OAI.RVM.ImprovedWindow line 322
  19. def OAI.RVM.PureOccupationBounds line 327
  20. lemma OAI.RVM.improvedWindow_of_powers line 334
  21. lemma OAI.RVM.pureOccupationBounds_power_table line 351
  22. lemma OAI.RVM.selected_receiverCoefficient_of_powers line 425
  23. lemma OAI.RVM.selected_receiverCoefficient line 466
  24. def OAI.RVM.pureOccupationEnvelope line 496
  25. lemma OAI.RVM.pureOccupationEnvelope_bounds line 506
  26. lemma OAI.RVM.pureOccupationEnvelope_nonneg line 521
  27. theorem OAI.RVM.receiverCoefficient_on_selected_bins line 530