  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
 102    This is the concrete Noether theorem for the standard mechanics
 103    Lagrangian `L = ½ m q̇² - V(q)`: time-translation invariance is
 104    automatic when `V` does not depend on `t` explicitly, and energy
 105    conservation `E = T + V` follows.
 106
 107    Proven directly by `Action.Hamiltonian.energy_conservation`, this
 108    lemma packages the result in the `Noether` namespace for clarity. -/
 109theorem energy_conservation_of_J_action (m : ℝ) (hm : 0 < m) (V : ℝ → ℝ)
 110    (γ : ℝ → ℝ)
 111    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.