isTimeTranslationInvariant

formal source

  45
  46/-- A J-action `S` on `RealAction` is time-translation invariant if
  47    `S(γ ∘ t-shift) = S(γ)` for every shift. -/
  48def isTimeTranslationInvariant (S : RealAction → ℝ) : Prop :=
  49  ∀ dt : ℝ, IsSymmetryOf (timeShift dt) S
  50
  51/-- The time-translation flow on `RealAction`. -/
  52def timeTranslationFlow : OneParamGroup RealAction where
  53  flow t γ := timeShift t γ
  54  flow_zero γ := by funext s; simp [timeShift]
  55  flow_add s t γ := by funext u; simp [timeShift]; ring_nf
  56
  57/-- **Energy conservation from time-translation invariance.**
  58
  59    If a J-action functional is time-translation invariant, then by
  60    `noether_core` it is itself conserved along the time-translation flow.
  61    The conserved quantity is interpreted as the total energy. -/
  62theorem time_translation_invariance_implies_energy_conservation
  63    (S : RealAction → ℝ)
  64    (h_inv : ∀ t, IsSymmetryOf (timeTranslationFlow.flow t) S) :
  65    IsConservedAlong S timeTranslationFlow.flow :=
  66  noether_core h_inv
  67
  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