OAI/Analysis/VlasovMaxwell/Retarded/DirectForce.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RVM.Admissible.direct_transport_radius_near line 16
  2. lemma OAI.RVM.capped_linear_radius_sum line 85
  3. lemma OAI.RVM.Admissible.direct_transport_remaining_all_radii line 94
  4. lemma OAI.RVM.transport_absolute_coefficient line 150
  5. lemma OAI.RVM.Admissible.direct_transport_all_radii_consistent line 173
  6. lemma OAI.RVM.physicalDirectTransport_integral_geometry_zero line 217
  7. lemma OAI.RVM.Admissible.direct_transport_all_radii line 231
  8. lemma OAI.RVM.exists_dyadicFactor_positive line 261
  9. lemma OAI.RVM.exists_dyadicMultiFactor_positive line 270
  10. abbrev OAI.RVM.DirectOuterIndex line 275
  11. def OAI.RVM.directOuterBin line 277
  12. lemma OAI.RVM.physical_direct_finite_cover line 280
  13. lemma OAI.RVM.physicalBinFamily_cover_lintegral line 313
  14. lemma OAI.RVM.directOuter_card line 348
  15. lemma OAI.RVM.directOuter_family_sum_bound line 351
  16. def OAI.RVM.directTriangleDomain line 370
  17. lemma OAI.RVM.measurableSet_directTriangleDomain line 373
  18. def OAI.RVM.directTriangleDensity line 377
  19. def OAI.RVM.directTransportTriangleKernel line 384
  20. def OAI.RVM.directSourceTriangleKernel line 387
  21. lemma OAI.RVM.measurable_directTriangleDensity line 393
  22. lemma OAI.RVM.measurable_directTransportTriangleKernel line 406
  23. lemma OAI.RVM.measurable_directSourceTriangleKernel line 412
  24. lemma OAI.RVM.directTriangleDensity_nonzero line 426
  25. lemma OAI.RVM.directTransportTriangle_bin_bound line 440
  26. lemma OAI.RVM.directSourceTriangle_bin_bound line 458
  27. lemma OAI.RVM.PhaseFlowOn.directTriangleDensity_finite_cover line 476
  28. lemma OAI.RVM.PhaseFlowOn.directTriangle_family_estimate line 493
  29. lemma OAI.RVM.Admissible.direct_transport_physical_bound line 521
  30. lemma OAI.RVM.Admissible.direct_source_physical_bound line 558
  31. lemma OAI.RVM.exists_direct_dyadic_count line 602
  32. lemma OAI.RVM.ennreal_count_four_bound line 613
  33. lemma OAI.RVM.Admissible.direct_transport_physical_log_bound line 625
  34. lemma OAI.RVM.Admissible.direct_source_physical_log_bound line 649
  35. lemma OAI.RVM.directTriangle_lintegral_polar line 679
  36. lemma OAI.RVM.directTriangleDensity_outside line 716
  37. lemma OAI.RVM.normalised_direct_kernel_identity line 721
  38. lemma OAI.RVM.normalised_direct_density_bound line 736
  39. lemma OAI.RVM.norm_integral_ENN_bound line 752
  40. lemma OAI.RVM.SmoothClassicalPrefix.direct_force_fiber_bound line 757
  41. lemma OAI.RVM.restrict_inside_finite_prefix line 781
  42. lemma OAI.RVM.SmoothClassicalPrefix.directForceEnergyPrefix line 791
  43. lemma OAI.RVM.SmoothClassicalPrefix.direct_force_triangle_bound line 807
  44. lemma OAI.RVM.SmoothClassicalPrefix.direct_lorentz_triangle_bound line 835
  45. lemma OAI.RVM.Admissible.direct_lorentz_log_bound line 862
  46. def OAI.RVM.directOuterIndexEquiv line 929
  47. lemma OAI.RVM.directOuter_remaining_sum line 935
  48. lemma OAI.RVM.ennreal_filter_sum_le_tsum line 974
  49. lemma OAI.RVM.directOuter_remaining_le_tsum line 979