OAI/Analysis/VlasovMaxwell/Population/TransportRemainder.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.capped_inverse_power_sum line 15
  2. lemma OAI.RVM.relative_occupation_angular_sum line 51
  3. def OAI.RVM.relativeSourceAngle line 90
  4. def OAI.RVM.relativeAngularConstant line 93
  5. lemma OAI.RVM.relativeAngularConstant_nonneg line 97
  6. lemma OAI.RVM.relativeSourceAngle_nonneg line 106
  7. lemma OAI.RVM.relative_source_angle_sum line 111
  8. lemma OAI.RVM.capped_lower_weighted_power_sum line 129
  9. lemma OAI.RVM.remaining_good_fixed_receiver_sum line 148
  10. lemma OAI.RVM.remaining_magnetic_fixed_receiver_sum line 180
  11. lemma OAI.RVM.square_root_clipped_stability line 201
  12. def OAI.RVM.remainingGoodConstant line 263
  13. def OAI.RVM.remainingMagneticConstant line 266
  14. lemma OAI.RVM.remaining_shared_source_angular line 269
  15. lemma OAI.RVM.remaining_stable_source_angular line 320
  16. lemma OAI.RVM.Admissible.direct_source_shared_short_angles_expanded line 340
  17. lemma OAI.RVM.capped_inverse_square_floor_sum line 791
  18. lemma OAI.RVM.capped_inverse_square_floor_tsum line 806
  19. lemma OAI.RVM.small_transport_coefficient line 821
  20. lemma OAI.RVM.small_transport_near_scalar line 830
  21. lemma OAI.RVM.small_transport_exception_model_sum line 841
  22. def OAI.RVM.smallTransportCoefficient line 897
  23. lemma OAI.RVM.smallTransportCoefficient_nonneg line 900
  24. lemma OAI.RVM.physicalDirectTransportDensity_representative_small line 907
  25. lemma OAI.RVM.PhaseFlowOn.directTransport_representative_small line 924
  26. lemma OAI.RVM.Admissible.small_transport_regular_radial line 940
  27. lemma OAI.RVM.Admissible.small_transport_exception_triple_sum line 987
  28. lemma OAI.RVM.Admissible.small_transport_regular_double_sum line 1049
  29. lemma OAI.RVM.Admissible.small_transport_regular_uniform line 1103
  30. lemma OAI.RVM.sourceRepresentative_cube_sum line 1182
  31. lemma OAI.RVM.Admissible.small_transport_exception_uniform line 1196
  32. lemma OAI.RVM.tsum_representativeSmallSector line 1265
  33. lemma OAI.RVM.Admissible.small_transport_uniform line 1297