IsConservedAlong'

formal source

  75  ∀ (x : X) (t₁ t₂ : ℝ), Q (φ t₁ x) = Q (φ t₂ x)
  76
  77/-- Alternative: Q is conserved if Q ∘ φ t = Q for all t. -/
  78def IsConservedAlong' {X : Type*} (Q : X → ℝ) (φ : ℝ → X → X) : Prop :=
  79  ∀ t : ℝ, Q ∘ (φ t) = Q
  80
  81/-- **THEOREM**: The two definitions of conservation are equivalent. -/
  82theorem conserved_iff_conserved' {X : Type*} (Q : X → ℝ) (φ : ℝ → X → X)
  83    (h0 : ∀ x, φ 0 x = x) :
  84    IsConservedAlong Q φ ↔ IsConservedAlong' Q φ := by
  85  constructor
  86  · intro h t
  87    funext x
  88    simp only [Function.comp_apply]
  89    rw [h x t 0, h0 x]
  90  · intro h x t₁ t₂
  91    have ht1 := congr_fun (h t₁) x
  92    have ht2 := congr_fun (h t₂) x
  93    simp only [Function.comp_apply] at ht1 ht2
  94    rw [ht1, ht2]
  95
  96/-! ## Noether's Core Result -/
  97
  98/-- A 1-parameter group action (simplified model). -/
  99structure OneParamGroup (X : Type*) where
 100  /-- The flow φ(t, x) giving the transformed point. -/
 101  flow : ℝ → X → X
 102  /-- φ(0, x) = x -/
 103  flow_zero : ∀ x, flow 0 x = x
 104  /-- Group property: φ(s+t, x) = φ(s, φ(t, x)) -/
 105  flow_add : ∀ s t x, flow (s + t) x = flow s (flow t x)
 106
 107/-- **THEOREM (Noether Core)**: If J is invariant under a 1-parameter group,
 108    then J itself is conserved along the flow.