OAI/Analysis/VlasovMaxwell/Retarded/DirectLargeAngularSharp.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.directDyadicPowerConstant line 14
  2. lemma OAI.RVM.directDyadicPowerConstant_nonneg line 16
  3. lemma OAI.RVM.remaining_large_good_receiver line 19
  4. lemma OAI.RVM.remaining_large_good_angles line 42
  5. lemma OAI.RVM.remaining_large_magnetic_receiver line 59
  6. lemma OAI.RVM.remaining_large_magnetic_angles line 80
  7. lemma OAI.RVM.remaining_large_combined_angles line 98
  8. lemma OAI.RVM.capped_large_magnetic_sharp_ennreal_sum line 123
  9. lemma OAI.RVM.direct_large_good_balance line 150
  10. lemma OAI.RVM.Admissible.direct_source_large_sharp_sum line 158