OAI/Analysis/VlasovMaxwell/Retarded/SourceWaveSpatialIbp.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.sourceWave_spatial_ibp line 35
  2. lemma OAI.RVM.electricPotentialComponent_ball line 43
  3. lemma OAI.RVM.magneticPotentialComponent_ball line 66
  4. lemma OAI.RVM.uniform_integral_bound_compact line 100
  5. lemma OAI.RVM.contDiffOn_retarded_flux line 126
  6. lemma OAI.RVM.divergence_add_right line 143
  7. lemma OAI.RVM.coneRadius_add line 150
  8. lemma OAI.RVM.retarded_flux_norm_bound line 154
  9. lemma OAI.RVM.retarded_flux_tip line 220
  10. lemma OAI.RVM.retarded_weighted_integral_bound line 263
  11. def OAI.RVM.normalisedElectricKernel line 295
  12. lemma OAI.RVM.normalisedElectricKernel_eq line 299
  13. lemma OAI.RVM.continuousOn_normalisedElectricKernel line 306
  14. lemma OAI.RVM.retarded_electric_kernel_norm_bound line 320
  15. def OAI.RVM.retardedElectricDensity line 389
  16. def OAI.RVM.retardedElectricFlux line 394
  17. lemma OAI.RVM.field_contDiffAt_positive line 397
  18. lemma OAI.RVM.contDiffAt_physicalElectricKernel line 406
  19. lemma OAI.RVM.contDiffAt_retardedElectricIntegrand line 421
  20. lemma OAI.RVM.contDiffOn_retardedElectricDensity line 455
  21. lemma OAI.RVM.integrableOn_ball_of_punctured_bound line 473
  22. lemma OAI.RVM.integrableOn_retardedElectricDensity line 490