OAI/Analysis/VlasovMaxwell/Population/CentralOccupation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.PhaseFlowOn.closedEulerian_joint_large_budget line 14
  2. lemma OAI.RVM.Admissible.representative_large_shared_occupation line 81
  3. lemma OAI.RVM.Admissible.representative_central_large_shared line 143
  4. def OAI.RVM.regularCentralIndex line 225
  5. def OAI.RVM.representativeRegularCentralCost line 230
  6. lemma OAI.RVM.Admissible.representative_regular_central_shared line 235
  7. lemma OAI.RVM.capped_square_tail_sum line 269
  8. lemma OAI.RVM.capped_fourth_tail_sum line 286
  9. lemma OAI.RVM.small_deficit_stabilityLength line 303
  10. lemma OAI.RVM.central_exception_coefficient line 327
  11. lemma OAI.RVM.capped_cube_tail_sum line 365
  12. lemma OAI.RVM.magnetic_low_radial_sum line 382
  13. lemma OAI.RVM.magnetic_low_angle_radial_sum line 396
  14. lemma OAI.RVM.magnetic_low_triple_sum line 425
  15. lemma OAI.RVM.magnetic_low_coefficient line 455
  16. lemma OAI.RVM.Admissible.representative_central_near line 478
  17. lemma OAI.RVM.Admissible.representative_regular_central_double_sum line 532
  18. lemma OAI.RVM.Admissible.central_regular_uniform line 596
  19. lemma OAI.RVM.central_exception_radial_sum line 666
  20. lemma OAI.RVM.central_exception_angle_radial_sum line 687
  21. lemma OAI.RVM.central_exception_triple_sum line 715
  22. def OAI.RVM.representativeExceptionCentralCost line 743
  23. lemma OAI.RVM.central_cost_eq_regular_add_exception line 748
  24. lemma OAI.RVM.Admissible.representative_exception_central_triple_sum line 757
  25. lemma OAI.RVM.sourceRepresentative_one_le line 827
  26. lemma OAI.RVM.Admissible.central_exception_uniform line 832
  27. lemma OAI.RVM.Admissible.representative_spatial_near line 910
  28. lemma OAI.RVM.Admissible.representative_spatial_regular_shared line 929
  29. lemma OAI.RVM.Admissible.representative_spatial_pure_far line 963
  30. lemma OAI.RVM.near_threshold_spatial line 1024
  31. lemma OAI.RVM.far_threshold_spatial line 1048
  32. lemma OAI.RVM.unselected_spatial_cap line 1067
  33. lemma OAI.RVM.Admissible.unselected_spatial_polynomial_cap line 1077
  34. lemma OAI.RVM.Admissible.central_uniform line 1133
  35. lemma OAI.RVM.remaining_transport_near_point line 1211
  36. lemma OAI.RVM.remaining_transport_near_angular line 1226