OAI/Analysis/VlasovMaxwell/Retarded/VolterraKernels.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Magnetic.integral_symmetric_annulus_tendsto line 16
  2. lemma OAI.RVM.Magnetic.norm_integral_ball_of_annulus_bound line 42
  3. lemma OAI.RVM.Magnetic.particle_spatial_fderiv line 50
  4. lemma OAI.RVM.Magnetic.transportConeCoefficient_uniform_bound line 59
  5. lemma OAI.RVM.Magnetic.transport_derivative_integrable line 82
  6. lemma OAI.RVM.Magnetic.magnetic_transport_gradient_bound line 138
  7. lemma OAI.RVM.Magnetic.particle_fixed_time_contDiff line 160
  8. lemma OAI.RVM.Magnetic.transport_kernel_velocity_contDiff line 166
  9. lemma OAI.RVM.Magnetic.hasDerivAt_transport_particle_line line 172
  10. lemma OAI.RVM.Magnetic.norm_transport_velocity_integral_le line 210
  11. lemma OAI.RVM.Magnetic.transport_density_integrable line 232
  12. lemma OAI.RVM.Magnetic.hasDerivAt_magnetic_transport_integral line 263
  13. lemma OAI.RVM.Magnetic.magnetic_transport_deriv_bound line 310
  14. lemma OAI.RVM.Magnetic.source_sphere_support line 331
  15. lemma OAI.RVM.Magnetic.source_bulk_support line 351
  16. lemma OAI.RVM.Magnetic.magnetic_source_annulus_gradient_bound line 369
  17. lemma OAI.RVM.Magnetic.sourceConeCoefficient_uniform_bound line 404
  18. lemma OAI.RVM.Magnetic.source_particle_derivative_integrable line 430
  19. lemma OAI.RVM.Magnetic.magnetic_source_particle_gradient_bound line 489
  20. lemma OAI.RVM.Magnetic.sourceAngularProfile_derivative_bound line 512
  21. def OAI.RVM.Magnetic.sourceReceiverKernel line 529
  22. lemma OAI.RVM.Magnetic.sourceReceiverKernel_contDiffAt line 532
  23. lemma OAI.RVM.Magnetic.source_receiver_fderiv_formula line 548
  24. lemma OAI.RVM.Magnetic.physical_source_receiver_bound line 566
  25. lemma OAI.RVM.Magnetic.norm_velocity_integral_bound line 601
  26. lemma OAI.RVM.Magnetic.retarded_packet_integrable line 613
  27. lemma OAI.RVM.Magnetic.retarded_packet_spatial_fderiv line 633
  28. lemma OAI.RVM.Magnetic.retarded_packet_derivative_zero line 639
  29. lemma OAI.RVM.Magnetic.hasDerivAt_retarded_packet_line line 649
  30. lemma OAI.RVM.Magnetic.hasDerivAt_retarded_packet_integral line 679
  31. lemma OAI.RVM.radial_volterra_majorant_integrable line 713
  32. lemma OAI.RVM.kernel_volterra_norm_subset line 727
  33. lemma OAI.RVM.source_volterra_factor line 758
  34. lemma OAI.RVM.source_division_bulk_annulus_volterra_bound line 764
  35. lemma OAI.RVM.electric_source_annulus_gradient_volterra_bound line 835
  36. lemma OAI.RVM.electric_source_particle_gradient_volterra_bound line 872
  37. lemma OAI.RVM.source_receiver_packet_volterra_bound line 895
  38. lemma OAI.RVM.electric_source_receiver_integral_volterra_bound line 920
  39. lemma OAI.RVM.electric_source_deriv_volterra_bound line 956
  40. lemma OAI.RVM.uniform_normalised_integrand_curvature_horizon line 1044
  41. lemma OAI.RVM.uniform_physical_integrand_curvature_horizon line 1078
  42. lemma OAI.RVM.uniform_physical_integral_curvature_horizon line 1102
  43. lemma OAI.RVM.boundary_integral_curvature_volterra line 1146
  44. lemma OAI.RVM.retarded_density_curvature_volterra line 1176
  45. lemma OAI.RVM.classical_fields_curvature_volterra_bound line 1216