OAI/Analysis/VlasovMaxwell/Retarded/RetardedMomentumForce.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RVM.retardedMomentumForce line 39
  2. lemma OAI.RVM.PhaseFlowOn.momentumForce_continuousOn line 46
  3. lemma OAI.RVM.PhaseFlowOn.retardedMomentum_regular line 60
  4. lemma OAI.RVM.PhaseFlowOn.actual_projector_regular line 88
  5. lemma OAI.RVM.PhaseFlowOn.actual_selected_projected_identity line 107
  6. lemma OAI.RVM.angularDerivativeCLM_smul_force line 134
  7. lemma OAI.RVM.moving_projector_measure_identity line 142
  8. lemma OAI.RVM.time_weight_measure_identity line 153
  9. lemma OAI.RVM.moving_projector_small_kernel line 161
  10. lemma OAI.RVM.projected_time_weight_small_kernel line 179
  11. lemma OAI.RVM.projected_primitive_highband_kernel line 226
  12. lemma OAI.RVM.moving_projector_highband_kernel line 241
  13. def OAI.RVM.physicalProjectedPrimitiveDensity line 259
  14. lemma OAI.RVM.physicalProjectedPrimitiveDensity_bound line 266
  15. lemma OAI.RVM.physicalProjectedPrimitive_near line 309
  16. lemma OAI.RVM.Admissible.projected_primitive_near_constant line 352
  17. lemma OAI.RVM.selected_multiplier_support_congr line 376
  18. lemma OAI.RVM.selected_initial_support_congr line 395
  19. lemma OAI.RVM.PhaseFlowOn.selected_angular_fubini line 407
  20. lemma OAI.RVM.directionWeight_tsupport line 432
  21. lemma OAI.RVM.continuousOn_angular_force line 444
  22. lemma OAI.RVM.exists_weighted_exit_of_modulus line 452
  23. lemma OAI.RVM.IncrementBootstrap.direction_modulus line 483
  24. lemma OAI.RVM.IncrementBootstrap.exists_weighted_angular_exit line 498
  25. def OAI.RVM.physicalMovingProjectorDensity line 560
  26. lemma OAI.RVM.physicalMovingProjectorDensity_bound line 567
  27. lemma OAI.RVM.physicalMovingProjector_near line 611
  28. lemma OAI.RVM.Admissible.moving_projector_near_constant line 656
  29. lemma OAI.RVM.selected_radial_factor line 676
  30. lemma OAI.RVM.selected_radial_width line 687
  31. lemma OAI.RVM.selected_projected_coefficient line 698
  32. lemma OAI.RVM.selected_moving_coefficient line 707
  33. lemma OAI.RVM.radial_half_decay line 716
  34. lemma OAI.RVM.sum_radial_half_decay line 724
  35. lemma OAI.RVM.sum_angular_half_decay line 731
  36. lemma OAI.RVM.sum_selected_radial_angular line 737