OAI/Analysis/VlasovMaxwell/Population/SharedOccupation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.DyadicWindow.mono_width line 14
  2. lemma OAI.RVM.jointEnergyBudget_mono_width line 19
  3. lemma OAI.RVM.PhaseFlowOn.closedEulerian_shared_budget line 38
  4. def OAI.RVM.representativeJointEnergy line 124
  5. lemma OAI.RVM.representativeJointEnergy_nonneg line 128
  6. lemma OAI.RVM.SmoothClassicalPrefix.representativeJointEnergy_sum line 132
  7. lemma OAI.RVM.shared_budget_radius_scalar line 157
  8. def OAI.RVM.representativeSharedRadius line 175
  9. lemma OAI.RVM.representativeSharedRadius_one_le line 180
  10. lemma OAI.RVM.Admissible.representative_shared_occupation line 186
  11. def OAI.RVM.representativeCentralCost line 270
  12. def OAI.RVM.representativeSpatialCost line 277
  13. lemma OAI.RVM.central_near_scalar line 282
  14. lemma OAI.RVM.central_far_scalar line 286
  15. lemma OAI.RVM.Admissible.representative_central_shared line 294
  16. lemma OAI.RVM.central_shared_radial_sum line 375
  17. lemma OAI.RVM.capped_linear_tail_sum line 408
  18. lemma OAI.RVM.Admissible.representative_central_double_sum line 425
  19. lemma OAI.RVM.Admissible.central_actual_uniform line 499