OAI/Analysis/VlasovMaxwell/Retarded/SourceMajorant.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.sourceMajorantKernel line 15
  2. lemma OAI.RVM.sourceMajorantKernel_nonneg line 19
  3. lemma OAI.RVM.forceSourceKernel_le_majorant line 27
  4. lemma OAI.RVM.sourceMajorantKernel_bin_bound line 36
  5. def OAI.RVM.physicalSourceMajorantDensity line 65
  6. lemma OAI.RVM.physicalSourceMajorantDensity_bound line 76
  7. lemma OAI.RVM.physicalSourceMajorant_integral_bound line 119
  8. lemma OAI.RVM.Admissible.source_majorant_two_budget_bound line 181
  9. lemma OAI.RVM.Admissible.source_majorant_relative_budget line 224
  10. lemma OAI.RVM.Admissible.source_majorant_time_budget line 280
  11. lemma OAI.RVM.projected_source_combined_le_majorant line 326
  12. lemma OAI.RVM.physicalProjectedSourceDensity_le_majorant line 382
  13. lemma OAI.RVM.physicalProjectedSourceIntegral_le_majorant line 401
  14. lemma OAI.RVM.Admissible.source_majorant_relative_radius_budget line 420
  15. def OAI.RVM.majorant_relativeCauchyConstant line 560
  16. lemma OAI.RVM.majorant_relativeCauchyConstant_nonneg line 563
  17. lemma OAI.RVM.majorant_relative_density_near_sqrt line 566
  18. lemma OAI.RVM.majorant_relative_density_far_sqrt line 577
  19. lemma OAI.RVM.majorant_relative_radius_cauchy_scalar line 589
  20. lemma OAI.RVM.Admissible.source_majorant_relative_short_radius line 652
  21. lemma OAI.RVM.majorant_capped_sqrt_radius_ennreal_sum line 750
  22. lemma OAI.RVM.Admissible.source_majorant_relative_short_radial_sum line 776
  23. lemma OAI.RVM.Admissible.source_majorant_remaining_short_sum line 870
  24. lemma OAI.RVM.Admissible.source_majorant_large_radius_budget line 965
  25. lemma OAI.RVM.majorant_relative_radius_cauchy_near line 1142
  26. lemma OAI.RVM.Admissible.source_majorant_short_near line 1171