pith. machine review for the scientific record. sign in
theorem proved term proof

space_translation_invariance_implies_momentum_conservation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  91theorem space_translation_invariance_implies_momentum_conservation
  92    (S : RealAction → ℝ)
  93    (h_inv : ∀ dx, IsSymmetryOf (spaceTranslationFlow.flow dx) S) :
  94    IsConservedAlong S spaceTranslationFlow.flow :=

proof body

Term-mode proof.

  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. -/

depends on (33)

Lean names referenced from this declaration's body.

… and 3 more