OAI/Analysis/VlasovMaxwell/Retarded/ConeRegularity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.smoothReciprocal line 18
  2. lemma OAI.RVM.smoothReciprocal_smooth line 20
  3. lemma OAI.RVM.smoothReciprocal_eq line 35
  4. lemma OAI.RVM.uniform_cone_denominator line 42
  5. def OAI.RVM.smoothNormalisedPhysical line 62
  6. lemma OAI.RVM.smoothNormalisedPhysical_smooth line 71
  7. lemma OAI.RVM.smoothNormalisedPhysical_eq line 89
  8. lemma OAI.RVM.uniform_normalised_integrand_tame line 95
  9. lemma OAI.RVM.compact_parameter_taylor line 136
  10. lemma OAI.RVM.compact_parameter_curvature line 188
  11. lemma OAI.RVM.uniform_normalised_integrand_curvature line 222
  12. abbrev OAI.RVM.ConeParameters line 269
  13. abbrev OAI.RVM.coneParameterMeasure line 270
  14. def OAI.RVM.compactPolarIntegral line 272
  15. lemma OAI.RVM.compactPolarIntegral_eq line 275
  16. lemma OAI.RVM.compactPolarIntegral_smooth line 299
  17. lemma OAI.RVM.compactPolarIntegral_derivative_bound line 307
  18. def OAI.RVM.normalisedRetardedExtension line 347
  19. lemma OAI.RVM.normalisedRetardedExtension_smooth line 353
  20. lemma OAI.RVM.retardedElectricDensity_polar_integral line 365
  21. lemma OAI.RVM.retardedElectricDensity_polar_compact line 392
  22. lemma OAI.RVM.crossCLM_norm_le line 415
  23. lemma OAI.RVM.retardedMagneticDensity_polar_compact line 419
  24. def OAI.RVM.ParticleJetBound line 449
  25. lemma OAI.RVM.uniform_retarded_extension_tame line 452
  26. lemma OAI.RVM.integral_Icc_sub line 499
  27. lemma OAI.RVM.physical_cone_derivative_tame line 506