space_translation_invariance_implies_momentum_conservation

formal source

  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))
 112    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
 113    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
 114    (h_dE_eq_factored : ∀ t : ℝ,
 115      deriv (HamiltonianMech.totalEnergy m V γ) t =
 116        deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t)))
 117    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
 118    ∀ t₁ t₂ : ℝ,
 119      HamiltonianMech.totalEnergy m V γ t₁ = HamiltonianMech.totalEnergy m V γ t₂ :=
 120  HamiltonianMech.energy_conservation m hm V γ hV_diff hγ_diff hγ_diff2 h_dE_eq_factored hEL
 121