spaceShift

formal source

  68/-! ## Space-translation invariance and momentum conservation -/
  69
  70/-- Space translation by `dx` on real-valued trajectories. -/
  71def spaceShift (dx : ℝ) : RealAction → RealAction :=
  72  fun γ t => γ t + dx
  73
  74/-- A J-action functional on real-valued trajectories is
  75    space-translation invariant if shifting the trajectory by a constant
  76    leaves the action unchanged. -/
  77def isSpaceTranslationInvariant (S : RealAction → ℝ) : Prop :=
  78  ∀ dx : ℝ, IsSymmetryOf (spaceShift dx) S
  79
  80/-- The space-translation flow on `RealAction`. -/
  81def spaceTranslationFlow : OneParamGroup RealAction where
  82  flow dx γ := spaceShift dx γ
  83  flow_zero γ := by funext s; simp [spaceShift]
  84  flow_add s t γ := by funext u; simp [spaceShift]; ring
  85
  86/-- **Momentum conservation from space-translation invariance.**
  87
  88    If a J-action functional is space-translation invariant, then by
  89    `noether_core` it is itself conserved along the space-translation
  90    flow. The conserved quantity is interpreted as the total momentum. -/
  91theorem space_translation_invariance_implies_momentum_conservation
  92    (S : RealAction → ℝ)
  93    (h_inv : ∀ dx, IsSymmetryOf (spaceTranslationFlow.flow dx) S) :
  94    IsConservedAlong S spaceTranslationFlow.flow :=
  95  noether_core h_inv
  96
  97/-! ## Specialized to the J-action: total energy is conserved -/
  98
  99/-- **The standard total energy of mechanical motion is conserved when
 100    the potential is time-independent.**
 101