OAI/Analysis/VlasovMaxwell/Retarded/ConeRadius.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.selection_unsafe_actual line 36
  2. lemma OAI.RVM.selection_unsafe_window line 65
  3. lemma OAI.RVM.selection_unsafe_contradiction line 95
  4. lemma OAI.RVM.integrableOn_norm_rpow_neg line 114
  5. lemma OAI.RVM.integral_ball_norm_rpow_neg line 120
  6. lemma OAI.RVM.norm_integral_tip_le line 151
  7. lemma OAI.RVM.potential_tip_le line 165
  8. lemma OAI.RVM.kernel_tip_le line 175
  9. lemma OAI.RVM.dot_zero_right_rvm line 185
  10. lemma OAI.RVM.dot_zero_left_rvm line 186
  11. lemma OAI.RVM.hasDerivAt_norm_nonzero line 188
  12. def OAI.RVM.coneRadius line 200
  13. def OAI.RVM.coneDirection line 201
  14. lemma OAI.RVM.coneDirection_norm line 203
  15. lemma OAI.RVM.hasDerivAt_coneRadius line 207
  16. lemma OAI.RVM.hasDerivAt_eulerian_direction line 218
  17. def OAI.RVM.eulerianG line 232
  18. lemma OAI.RVM.hasDerivAt_eulerianG_space line 234
  19. lemma OAI.RVM.hasDerivAt_eulerianG_velocity line 252
  20. lemma OAI.RVM.eulerian_kernel_decomposition line 267
  21. lemma OAI.RVM.retarded_transport_chain line 278
  22. lemma OAI.RVM.retarded_transport_identity line 309
  23. lemma OAI.RVM.classical_retarded_transport line 321
  24. lemma OAI.RVM.dot_gradient_direction line 332
  25. lemma OAI.RVM.divergence_const_rvm line 337
  26. lemma OAI.RVM.fderiv_phase_split line 340
  27. lemma OAI.RVM.phase_divergence_transport line 361
  28. lemma OAI.RVM.hasDerivAt_line_rvm line 373
  29. lemma OAI.RVM.fderiv_of_line_rvm line 379
  30. lemma OAI.RVM.differentiableAt_coneRadius line 386
  31. lemma OAI.RVM.differentiableAt_coneDirection line 390
  32. lemma OAI.RVM.differentiableAt_eulerianG line 395
  33. lemma OAI.RVM.fderiv_eulerianG_space line 405
  34. lemma OAI.RVM.fderiv_eulerianG_velocity line 424
  35. def OAI.RVM.retardedG line 438
  36. lemma OAI.RVM.differentiableAt_retardedG line 441
  37. lemma OAI.RVM.fderiv_retardedG line 452
  38. def OAI.RVM.retardedDensity line 467
  39. lemma OAI.RVM.differentiableAt_retardedDensity line 470
  40. lemma OAI.RVM.fderiv_vec_component_at line 478
  41. lemma OAI.RVM.retardedG_deficit_component line 484
  42. lemma OAI.RVM.retarded_electric_density_identity line 492
  43. lemma OAI.RVM.fderiv_cross_apply line 522
  44. lemma OAI.RVM.fderiv_coneDirection_apply line 549
  45. lemma OAI.RVM.eulerian_cross_direction line 557
  46. def OAI.RVM.retardedH line 563
  47. lemma OAI.RVM.differentiableAt_retardedH line 565
  48. lemma OAI.RVM.fderiv_retardedH line 572
  49. lemma OAI.RVM.retardedH_deficit_component line 602
  50. lemma OAI.RVM.retarded_magnetic_density_identity line 609
  51. def OAI.RVM.holeCutoff line 640
  52. lemma OAI.RVM.contDiff_holeCutoff line 642
  53. lemma OAI.RVM.holeCutoff_zero line 645
  54. lemma OAI.RVM.holeCutoff_one line 651
  55. lemma OAI.RVM.holeCutoff_eventually_one line 657
  56. lemma OAI.RVM.contDiff_holeCutoff_smul line 664
  57. lemma OAI.RVM.divergence_congr_eventually line 677
  58. lemma OAI.RVM.divergence_holeCutoff line 684
  59. lemma OAI.RVM.divergence_annulus line 691
  60. lemma OAI.RVM.contDiff_dot_pair line 750
  61. lemma OAI.RVM.contDiff_eulerianG_velocity line 755
  62. lemma OAI.RVM.contDiff_retardedG_velocity line 763
  63. lemma OAI.RVM.contDiff_retardedH_velocity line 769
  64. lemma OAI.RVM.contDiff_particle_velocity_profile line 775
  65. lemma OAI.RVM.compactSupport_particle_velocity_profile line 782
  66. lemma OAI.RVM.integral_retarded_velocity_divergence_zero line 791
  67. lemma OAI.RVM.classical_retarded_electric_velocity_divergence line 798
  68. lemma OAI.RVM.classical_retarded_magnetic_velocity_divergence line 810
  69. lemma OAI.RVM.integrable_divergence_compact line 822
  70. lemma OAI.RVM.divergence_integral_uniform_support line 830
  71. lemma OAI.RVM.contDiffAt_coneRadius line 868
  72. lemma OAI.RVM.contDiffAt_coneDirection line 872
  73. lemma OAI.RVM.contDiffAt_retardedG line 877
  74. lemma OAI.RVM.contDiffAt_retardedH line 890
  75. lemma OAI.RVM.contDiffAt_retardedDensity line 896
  76. lemma OAI.RVM.particle_contDiffAt_positive line 905
  77. def OAI.RVM.retardedSpaceDomain line 914
  78. lemma OAI.RVM.isOpen_retardedSpaceDomain line 917
  79. lemma OAI.RVM.retarded_local_data line 925
  80. lemma OAI.RVM.integrable_spatial_divergence_uniform_support line 941
  81. lemma OAI.RVM.classical_retarded_flux_calculus line 972
  82. lemma OAI.RVM.continuous_physicalElectricKernel_velocity line 1003
  83. lemma OAI.RVM.classical_retarded_integral_identity line 1023
  84. lemma OAI.RVM.classical_retarded_electric_integral_identity line 1057
  85. lemma OAI.RVM.classical_retarded_magnetic_integral_identity line 1098
  86. lemma OAI.RVM.dirD_integral_sphere line 1145
  87. def OAI.RVM.radiusWaveKernel line 1160
  88. lemma OAI.RVM.sourceWave_eq_radius line 1163
  89. lemma OAI.RVM.contDiff_radiusWaveKernel line 1170
  90. lemma OAI.RVM.dirD_radius_average line 1181
  91. lemma OAI.RVM.dirD_radiusWaveKernel line 1203
  92. lemma OAI.RVM.dirD_sourceWave line 1221
  93. lemma OAI.RVM.electricPotentialComponent_source line 1230
  94. lemma OAI.RVM.magneticPotentialComponent_source line 1239
  95. lemma OAI.RVM.ballCutoff_one line 1248
  96. lemma OAI.RVM.ballCutoff_eventually_one line 1253
  97. lemma OAI.RVM.divergence_annulus_local line 1259
  98. lemma OAI.RVM.integral_annulus_tendsto line 1300
  99. lemma OAI.RVM.divergence_ball_singular line 1319
  100. def OAI.RVM.coneSpatialCoefficient line 1340
  101. def OAI.RVM.coneSpatialLift line 1343
  102. lemma OAI.RVM.coneSpatialCoefficient_identity line 1346
  103. lemma OAI.RVM.retarded_spatial_division line 1353
  104. lemma OAI.RVM.phase_divergence_split line 1366
  105. lemma OAI.RVM.differentiableAt_coneSpatialCoefficient line 1387
  106. lemma OAI.RVM.retarded_spatial_divergence line 1403