OAI/Analysis/VlasovMaxwell/Retarded/ReceiverQCLM.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.receiverQCLM line 36
  2. lemma OAI.RVM.receiverQCLM_apply line 39
  3. lemma OAI.RVM.integral_receiverQ line 43
  4. def OAI.RVM.retardedForceKernel line 47
  5. lemma OAI.RVM.physical_lorentz_density line 53
  6. lemma OAI.RVM.classical_boundaryLorentzForce_datum line 68
  7. lemma OAI.RVM.classical_retarded_force_representation line 79
  8. lemma OAI.RVM.ball_puncture_ae line 94
  9. lemma OAI.RVM.integrable_joint_of_punctured_norm_bound line 100
  10. lemma OAI.RVM.coneDirection_translate line 129
  11. lemma OAI.RVM.continuousOn_coneDirection_zero line 132
  12. lemma OAI.RVM.integrable_radial_lift line 138
  13. lemma OAI.RVM.integrable_retarded_weighted_radial line 181
  14. lemma OAI.RVM.continuousOn_receiverQ line 209
  15. def OAI.RVM.retardedNormalisedForce line 216
  16. lemma OAI.RVM.continuousOn_retardedNormalisedForce line 222
  17. lemma OAI.RVM.radial_retardedNormalisedForce_eq line 257
  18. lemma OAI.RVM.integrable_joint_retardedForceKernel line 268
  19. lemma OAI.RVM.classical_retarded_force_phase_integral line 282
  20. lemma OAI.RVM.retarded_phase_translate_integral line 324
  21. lemma OAI.RVM.retarded_phase_translate_integrable_iff line 357
  22. def OAI.RVM.physicalPhaseForce line 399
  23. lemma OAI.RVM.retardedForceKernel_phase line 405
  24. lemma OAI.RVM.integrableOn_physical_force_phase line 409
  25. lemma OAI.RVM.classical_retarded_force_phase_domain line 418
  26. lemma OAI.RVM.classical_retarded_force_label_integral line 427
  27. lemma OAI.RVM.physical_force_branch_kernel line 445
  28. abbrev OAI.RVM.ConeKernelState line 492
  29. def OAI.RVM.coneKernelDomain line 493
  30. lemma OAI.RVM.EnergyPrefix.uniform_cone_kernel_bound line 496
  31. def OAI.RVM.normalisedSignedForce line 520
  32. lemma OAI.RVM.normalisedSignedForce_eq line 523
  33. lemma OAI.RVM.continuousOn_normalisedSignedForce line 530
  34. def OAI.RVM.sourceAcceleration line 543
  35. lemma OAI.RVM.EnergyPrefix.continuousOn_sourceAcceleration line 546
  36. lemma OAI.RVM.PhaseFlowOn.normalised_source_force_continuousOn line 559
  37. lemma OAI.RVM.PhaseFlowOn.source_force_inverse_square_bound line 579
  38. def OAI.RVM.arrivalPhaseDomain line 597
  39. def OAI.RVM.arrivalKernelState line 600
  40. lemma OAI.RVM.PhaseFlowOn.isOpen_arrivalPhaseDomain line 604
  41. lemma OAI.RVM.PhaseFlowOn.arrivalKernelState_mem line 608
  42. lemma OAI.RVM.PhaseFlowOn.arrivalKernelState_continuousOn line 616
  43. def OAI.RVM.arrivalConeKernel line 625
  44. lemma OAI.RVM.PhaseFlowOn.measurable_arrivalConeKernel line 630
  45. lemma OAI.RVM.PhaseFlowOn.arrivalConeKernel_integrable line 649
  46. def OAI.RVM.actualArrivalSignedForce line 679
  47. lemma OAI.RVM.PhaseFlowOn.actualArrivalSignedForce_eq line 685
  48. lemma OAI.RVM.PhaseFlowOn.actualArrivalSignedForce_measurable line 706
  49. lemma OAI.RVM.PhaseFlowOn.actualArrivalSignedForce_integrable line 712
  50. lemma OAI.RVM.PhaseFlowOn.actualArrivalSignedForce_integrable_weight line 718