pith. machine review for the scientific record. sign in
structure definition def or abbrev

OneParamGroup

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)

  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.
 109
 110    This is the heart of Noether's theorem: symmetry ⟹ conservation. -/

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.