OAI/Analysis/VlasovMaxwell/Population/RadialSummation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.capped_positive_power_sum_unscaled line 40
  2. lemma OAI.RVM.large_radius_magnetic_relative_sum line 50
  3. lemma OAI.RVM.large_radius_magnetic_angular_sum line 78
  4. lemma OAI.RVM.physical_relative_remaining_upper line 118
  5. lemma OAI.RVM.large_radius_magnetic_full_sum line 129
  6. lemma OAI.RVM.relative_density_time_far_sqrt line 173
  7. lemma OAI.RVM.relative_large_magnetic_cauchy_scalar line 186
  8. lemma OAI.RVM.Admissible.direct_source_large_radius line 252
  9. lemma OAI.RVM.capped_large_magnetic_ennreal_sum line 319
  10. lemma OAI.RVM.remaining_good_coarse_balance line 367
  11. lemma OAI.RVM.Admissible.direct_source_remaining_large_sum line 394
  12. lemma OAI.RVM.capped_short_sqrt_radius_sum line 478
  13. lemma OAI.RVM.Admissible.direct_source_short_near_sum line 506
  14. lemma OAI.RVM.deficit_short_source_coefficient line 548
  15. lemma OAI.RVM.shortSqrtConstant_pos line 593
  16. lemma OAI.RVM.Admissible.direct_source_deficit_short_sum line 598
  17. lemma OAI.RVM.relativeCauchyConstant_energy_le line 633
  18. lemma OAI.RVM.remaining_stability_sqrt_coarse line 656
  19. lemma OAI.RVM.Admissible.direct_source_remaining_all_radii line 677
  20. lemma OAI.RVM.deficit_short_source_coefficient_expanded line 822
  21. lemma OAI.RVM.Admissible.direct_source_deficit_short_sum_expanded line 867
  22. lemma OAI.RVM.relativePhysicalBase_receiver_floor line 908
  23. lemma OAI.RVM.physicalDirectSource_integral_expanded_bad_zero line 924
  24. lemma OAI.RVM.physicalDirectTransport_integral_expanded_bad_zero line 943