OAI/Analysis/VlasovMaxwell/Retarded/ConeMotion.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Elementary relativistic geometry needed by the retarded-force identity.

  1. lemma OAI.RVM.q_pos line 14
  2. lemma OAI.RVM.q_sq line 17
  3. lemma OAI.RVM.norm_lt_q line 20
  4. lemma OAI.RVM.norm_velocity_lt_one line 25
  5. lemma OAI.RVM.dot_comm line 30
  6. lemma OAI.RVM.dot_add_left line 33
  7. lemma OAI.RVM.dot_sub_left line 36
  8. lemma OAI.RVM.dot_smul_left line 39
  9. lemma OAI.RVM.dot_add_right line 42
  10. lemma OAI.RVM.dot_sub_right line 45
  11. lemma OAI.RVM.dot_smul_right line 48
  12. lemma OAI.RVM.dot_eq_inner line 51
  13. lemma OAI.RVM.dot_self line 54
  14. lemma OAI.RVM.dot_le_norm line 57
  15. lemma OAI.RVM.cone_denom_pos line 61
  16. lemma OAI.RVM.velocity_self line 67
  17. lemma OAI.RVM.cone_angle_identity line 74
  18. lemma OAI.RVM.hasDerivAt_dot line 79
  19. def OAI.RVM.coneMotion line 85
  20. def OAI.RVM.signedPrimitive line 88
  21. lemma OAI.RVM.coneMotion_dot_source line 91
  22. lemma OAI.RVM.coneMotion_receiver_identity line 99
  23. def OAI.RVM.signedPrimitiveRate line 111
  24. lemma OAI.RVM.hasDerivAt_signedPrimitive line 116
  25. def OAI.RVM.retardedPrimitive line 129
  26. def OAI.RVM.retardedPrimitiveRate line 132
  27. lemma OAI.RVM.hasDerivAt_retardedPrimitive line 137
  28. def OAI.RVM.coneTransform line 153
  29. lemma OAI.RVM.coneTransform_source line 155
  30. def OAI.RVM.sourceVelocityRate line 165
  31. def OAI.RVM.signedForceKernel line 168
  32. lemma OAI.RVM.signed_force_identity line 173
  33. lemma OAI.RVM.signed_force_identity_along_branch line 191
  34. lemma OAI.RVM.unsafe_selected_actual_margins line 208
  35. lemma OAI.RVM.unsafe_selected_improved_window line 246
  36. lemma OAI.RVM.unsafe_selected_improved_contradiction line 272
  37. lemma OAI.RVM.norm_velocity_le_margin line 283
  38. def OAI.RVM.receiverConeFunction line 298
  39. lemma OAI.RVM.receiverCone_growth line 301
  40. lemma OAI.RVM.receiverCone_strictMonoOn line 316
  41. lemma OAI.RVM.exists_unique_receiver_time line 325
  42. lemma OAI.RVM.hit_duration_bound line 347
  43. lemma OAI.RVM.projected_hit_duration line 367
  44. lemma OAI.RVM.scalar_clm_invertible line 389
  45. def OAI.RVM.squaredCone line 408
  46. lemma OAI.RVM.contDiffAt_squaredCone line 411
  47. lemma OAI.RVM.hasDerivAt_squaredCone_receiver line 418
  48. lemma OAI.RVM.receiver_partial_squaredCone line 427