RealAction

formal source

  37/-! ## Time-translation invariance and energy conservation -/
  38
  39/-- A J-action functional on real-valued trajectories. -/
  40abbrev RealAction := ℝ → ℝ
  41
  42/-- Time translation by `dt` on real-valued trajectories. -/
  43def timeShift (dt : ℝ) : RealAction → RealAction :=
  44  fun γ t => γ (t + dt)
  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. -/