OAI/Analysis/VlasovMaxwell/Population/SharedBudget.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Admissible.direct_source_shared_short_radius line 14
  2. lemma OAI.RVM.Admissible.direct_source_shared_short_radial_sum line 123
  3. lemma OAI.RVM.relativeCauchyConstant_factor line 221
  4. lemma OAI.RVM.relative_source_balance_factor line 226
  5. lemma OAI.RVM.relative_source_good_balance_factor line 251
  6. lemma OAI.RVM.Admissible.direct_source_shared_short_radial_factored line 262
  7. lemma OAI.RVM.Admissible.direct_source_shared_short_clipped line 322
  8. def OAI.RVM.directReceiverGoodBudget line 389
  9. def OAI.RVM.directReceiverMagneticBudget line 394
  10. lemma OAI.RVM.SmoothClassicalPrefix.directReceiverGoodBudget_sum line 398
  11. lemma OAI.RVM.SmoothClassicalPrefix.directReceiverMagneticBudget_sum line 421
  12. lemma OAI.RVM.budget_sqrt_weight_sum line 453
  13. lemma OAI.RVM.budget_sqrt_sum line 466
  14. lemma OAI.RVM.source_sqrt_sum_bound line 474
  15. lemma OAI.RVM.source_stability_sqrt_sum line 503
  16. lemma OAI.RVM.receiver_scale_card line 534
  17. lemma OAI.RVM.receiver_good_sqrt_sum line 560
  18. lemma OAI.RVM.momentum_affine_stability_sum line 570
  19. lemma OAI.RVM.source_stability_sqrt_sum_upper line 584
  20. lemma OAI.RVM.rpow_three_quarters_le_sqrt line 615
  21. lemma OAI.RVM.plain_magnetic_three_quarters line 620
  22. lemma OAI.RVM.source_parameter_scalar line 639
  23. lemma OAI.RVM.remaining_source_uniform_numerics line 668
  24. lemma OAI.RVM.receiver_shared_two_budget_sum line 710
  25. lemma OAI.RVM.momentum_affine_stability_sum_upper line 741
  26. lemma OAI.RVM.remaining_source_budget_total line 756
  27. lemma OAI.RVM.receiver_scale_card_enlarged line 831
  28. lemma OAI.RVM.Admissible.direct_source_shared_short_angles line 849
  29. lemma OAI.RVM.remainingGoodConstant_nonneg line 931
  30. lemma OAI.RVM.remainingMagneticConstant_nonneg line 938
  31. lemma OAI.RVM.Admissible.direct_remaining_source_short_uniform line 944
  32. lemma OAI.RVM.Admissible.direct_remaining_source_short_uniform_expanded line 1066