OAI/Analysis/VlasovMaxwell/Retarded/SourceForceConeKernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.SmoothClassicalPrefix.sourceForceEnergyPrefix line 40
  2. def OAI.RVM.sourceForceConeKernel line 56
  3. lemma OAI.RVM.PhaseFlowOn.actualLabelSignedForce_eq_normalised line 61
  4. lemma OAI.RVM.labelConeKernel_receiver_weight line 77
  5. lemma OAI.RVM.SmoothClassicalPrefix.weighted_retarded_force_label line 87
  6. def OAI.RVM.unselectedLabelSignedForce line 128
  7. lemma OAI.RVM.split_label_force line 133
  8. lemma OAI.RVM.PhaseFlowOn.weightedLabelSignedForce_integrable line 141
  9. lemma OAI.RVM.PhaseFlowOn.unselectedLabelSignedForce_integrable line 150
  10. lemma OAI.RVM.PhaseFlowOn.split_label_force_integral line 163
  11. lemma OAI.RVM.SmoothClassicalPrefix.selected_force_decomposition line 182
  12. lemma OAI.RVM.triangleConeKernel_receiver_multiplier line 230
  13. lemma OAI.RVM.labelConeKernel_receiver_multiplier line 240
  14. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_multiplier_fiber line 250
  15. lemma OAI.RVM.PhaseFlowOn.triangleConeKernel_fiber_sphere line 276
  16. lemma OAI.RVM.SmoothClassicalPrefix.multiplier_retarded_force_label line 309
  17. lemma OAI.RVM.PhaseFlowOn.split_multiplier_force_integral line 351
  18. lemma OAI.RVM.SmoothClassicalPrefix.selected_multiplier_decomposition line 377