OAI/Analysis/VlasovMaxwell/Retarded/SourceKernels.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.contDiffAt_sourceAngularCore line 16
  2. def OAI.RVM.sourceAngularProfile line 26
  3. lemma OAI.RVM.sourceAngularProfile_contDiffAt line 30
  4. def OAI.RVM.sourceFixedCoefficient line 45
  5. def OAI.RVM.sourceFixedFlux line 48
  6. lemma OAI.RVM.sourceFixedCoefficient_contDiffAt line 51
  7. lemma OAI.RVM.sourceFixedFlux_contDiffAt line 59
  8. lemma OAI.RVM.sourceFixedFlux_homogeneous line 63
  9. lemma OAI.RVM.fderiv_degree_neg_one line 70
  10. lemma OAI.RVM.divergence_degree_neg_one line 89
  11. def OAI.RVM.sourceConeCoefficient line 106
  12. lemma OAI.RVM.sourceConeCoefficient_contDiffAt line 110
  13. lemma OAI.RVM.electric_source_division_annulus line 126
  14. def OAI.RVM.sourceJointFlux line 148
  15. lemma OAI.RVM.sourceJointFlux_contDiffAt line 151
  16. lemma OAI.RVM.sourceJointFlux_derivative_bound line 166
  17. lemma OAI.RVM.sourceFixedFlux_spatial_derivative line 185
  18. lemma OAI.RVM.sourceFixedFlux_field_derivative line 193
  19. lemma OAI.RVM.sourceFixedFlux_field_differentiable line 200
  20. lemma OAI.RVM.sourceFixedFlux_field_rescale line 205
  21. lemma OAI.RVM.sourceFixedFlux_bounds line 217
  22. lemma OAI.RVM.divergence_parameter_chain line 257
  23. lemma OAI.RVM.source_dynamic_spatial_divergence_bound line 279
  24. lemma OAI.RVM.retarded_spacetime_lipschitz line 316
  25. lemma OAI.RVM.norm_fderiv_retarded_fields line 326
  26. lemma OAI.RVM.physical_source_spatial_bound line 345
  27. def OAI.RVM.sourceVelocityProfile line 373
  28. lemma OAI.RVM.sourceVelocityProfile_contDiffAt line 378
  29. lemma OAI.RVM.continuousOn_sourceVelocityDivergence line 393
  30. lemma OAI.RVM.sourceVelocityDivergence_uniform_bound line 407
  31. lemma OAI.RVM.source_velocity_divergence_rescale line 426
  32. lemma OAI.RVM.physical_source_velocity_bound line 445
  33. lemma OAI.RVM.sourceFixedFlux_uniform_bound line 460
  34. lemma OAI.RVM.source_sphere_rescale line 479
  35. lemma OAI.RVM.source_sphere_boundary_bound line 502
  36. def OAI.RVM.sourceDivisionBulk line 541
  37. lemma OAI.RVM.inverse_source_majorant line 547
  38. lemma OAI.RVM.source_division_bulk_annulus_bound line 554
  39. lemma OAI.RVM.source_sphere_support line 625
  40. lemma OAI.RVM.source_bulk_support line 645
  41. lemma OAI.RVM.electric_source_annulus_gradient_bound line 663
  42. lemma OAI.RVM.sourceConeCoefficient_uniform_bound line 698
  43. lemma OAI.RVM.source_particle_derivative_integrable line 724
  44. lemma OAI.RVM.electric_source_particle_gradient_bound line 783
  45. lemma OAI.RVM.sourceAngularProfile_derivative_bound line 806
  46. def OAI.RVM.sourceReceiverKernel line 823
  47. lemma OAI.RVM.sourceReceiverKernel_contDiffAt line 826
  48. lemma OAI.RVM.source_receiver_fderiv_formula line 842
  49. lemma OAI.RVM.physical_source_receiver_bound line 860
  50. def OAI.RVM.sourceWeightedPacket line 895
  51. lemma OAI.RVM.sourceWeightedPacket_contDiffAt line 898
  52. lemma OAI.RVM.sourceWeightedPacket_fderiv line 909
  53. lemma OAI.RVM.source_packet_estimates line 932
  54. lemma OAI.RVM.hasDerivAt_electric_source_integral line 972
  55. lemma OAI.RVM.retarded_packet_inner_integrable line 998
  56. lemma OAI.RVM.norm_integral_ball_inverse_le line 1007
  57. def OAI.RVM.sourceReceiverParticlePacket line 1019
  58. lemma OAI.RVM.sourceReceiverParticlePacket_continuousAt line 1022
  59. lemma OAI.RVM.source_receiver_packet_bound line 1033
  60. lemma OAI.RVM.electric_source_receiver_integral_bound line 1057
  61. lemma OAI.RVM.electric_source_deriv_bound line 1079
  62. lemma OAI.RVM.Magnetic.contDiffAt_sourceAngularCore line 1162
  63. def OAI.RVM.Magnetic.sourceAngularProfile line 1169
  64. lemma OAI.RVM.Magnetic.sourceAngularProfile_contDiffAt line 1173
  65. def OAI.RVM.Magnetic.sourceFixedCoefficient line 1188
  66. def OAI.RVM.Magnetic.sourceFixedFlux line 1191
  67. lemma OAI.RVM.Magnetic.sourceFixedCoefficient_contDiffAt line 1194
  68. lemma OAI.RVM.Magnetic.sourceFixedFlux_contDiffAt line 1202
  69. lemma OAI.RVM.Magnetic.sourceFixedFlux_homogeneous line 1206
  70. lemma OAI.RVM.Magnetic.fderiv_degree_neg_one line 1213
  71. lemma OAI.RVM.Magnetic.divergence_degree_neg_one line 1232
  72. def OAI.RVM.Magnetic.sourceConeCoefficient line 1249
  73. lemma OAI.RVM.Magnetic.sourceConeCoefficient_contDiffAt line 1253
  74. lemma OAI.RVM.Magnetic.magnetic_source_division_annulus line 1269