OAI/Analysis/VlasovMaxwell/Retarded/PhysicalDirectTransportDensity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.dyadic_sqrt_radius_balance line 42
  2. lemma OAI.RVM.remaining_good_radial_sum line 83
  3. lemma OAI.RVM.remaining_magnetic_radial_sum line 108
  4. lemma OAI.RVM.direct_transport_bin_bound line 133
  5. lemma OAI.RVM.direct_source_bin_bound line 166
  6. def OAI.RVM.physicalDirectTransportDensity line 199
  7. lemma OAI.RVM.physicalDirectTransportDensity_bound line 206
  8. lemma OAI.RVM.PhaseFlowOn.direct_transport_near_far line 240
  9. lemma OAI.RVM.Admissible.direct_transport_relative_budget line 280
  10. def OAI.RVM.physicalDirectSourceDensity line 329
  11. lemma OAI.RVM.physicalDirectSourceDensity_bound line 341
  12. lemma OAI.RVM.physicalDirectSource_integral_bound line 385
  13. lemma OAI.RVM.Admissible.direct_source_two_budget_bound line 447
  14. lemma OAI.RVM.Admissible.direct_source_relative_budget line 490
  15. lemma OAI.RVM.PhaseFlowOn.direct_transport_split_near_far line 546
  16. lemma OAI.RVM.Admissible.direct_transport_split_relative_budget line 573
  17. lemma OAI.RVM.measurable_forceTransportKernel line 647
  18. lemma OAI.RVM.measurable_forceSourceKernel_lorentz line 660
  19. lemma OAI.RVM.physicalDirectTransportDensity_relative_cover line 683
  20. lemma OAI.RVM.physicalDirectSourceDensity_relative_cover line 698
  21. lemma OAI.RVM.measurable_forceTransportFamily line 715
  22. lemma OAI.RVM.measurable_forceSourceFamily line 729
  23. lemma OAI.RVM.measurable_lorentz_acceleration line 744
  24. lemma OAI.RVM.measurable_coneBin_kernelDensity line 753
  25. lemma OAI.RVM.physicalDirectTransportDensity_aemeasurable line 785
  26. lemma OAI.RVM.physicalDirectSourceDensity_aemeasurable line 810
  27. lemma OAI.RVM.EnergyPrefix.measurable_velocity_slice line 840
  28. lemma OAI.RVM.physicalDirectTransport_integral_relative_cover line 847
  29. lemma OAI.RVM.physicalDirectSource_integral_relative_cover line 865