noether_core

formal source

 108    then J itself is conserved along the flow.
 109
 110    This is the heart of Noether's theorem: symmetry ⟹ conservation. -/
 111theorem noether_core {X : Type*} {G : OneParamGroup X} {J : X → ℝ}
 112    (hinv : ∀ t, IsSymmetryOf (G.flow t) J) :
 113    IsConservedAlong J G.flow := by
 114  intro x t₁ t₂
 115  rw [hinv t₁ x, hinv t₂ x]
 116
 117/-- The Noether charge is any function conserved by the flow. -/
 118def NoetherCharge {X : Type*} (G : OneParamGroup X) :=
 119  { Q : X → ℝ // IsConservedAlong Q G.flow }
 120
 121/-- **THEOREM**: Any invariant function is a Noether charge. -/
 122theorem invariant_is_noether_charge {X : Type*} {G : OneParamGroup X} {J : X → ℝ}
 123    (hinv : ∀ t, IsSymmetryOf (G.flow t) J) :
 124    ∃ Q : NoetherCharge G, Q.val = J :=
 125  ⟨⟨J, noether_core hinv⟩, rfl⟩
 126
 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