 127/-! ## Time Translation and Energy -/
 128
 129/-- Time translation by dt. -/
 130def TimeTranslation : OneParamGroup ℝ where
 131  flow t x := x + t
 132  flow_zero x := by ring
 133  flow_add s t x := by ring
 134
 135/-- **THEOREM**: Any time-translation-invariant function is conserved.
 136    (Energy is time-translation invariant ⟹ Energy is conserved) -/
 137theorem time_invariance_implies_conservation {E : ℝ → ℝ}
 138    (hinv : ∀ t, IsSymmetryOf (TimeTranslation.flow t) E) :
 139    IsConservedAlong E TimeTranslation.flow :=
 140  noether_core hinv
 141
 142/-! ## Space Translation and Momentum -/
 143
 144/-- Space translation by dx. -/
 145def SpaceTranslation : OneParamGroup ℝ where
 146  flow dx x := x + dx
 147  flow_zero x := by ring
 148  flow_add s t x := by ring
 149
 150/-- **THEOREM**: Any space-translation-invariant function is conserved.
 151    (Lagrangian invariant under space translation ⟹ Momentum conserved) -/
 152theorem space_invariance_implies_conservation {P : ℝ → ℝ}
 153    (hinv : ∀ dx, IsSymmetryOf (SpaceTranslation.flow dx) P) :
 154    IsConservedAlong P SpaceTranslation.flow :=
 155  noether_core hinv
 156
 157/-! ## Phase Rotation and Charge -/
 158
 159/-- Phase rotation on ℂ. -/
 160noncomputable def PhaseRotation : OneParamGroup ℂ where

papers checked against this theorem

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