id_is_symmetry

formal source

  47  ∀ x : X, J (T x) = J x
  48
  49/-- **THEOREM**: The identity is always a symmetry. -/
  50theorem id_is_symmetry {X : Type*} (J : X → ℝ) : IsSymmetryOf id J := by
  51  intro x
  52  rfl
  53
  54/-- **THEOREM**: Composition of symmetries is a symmetry. -/
  55theorem symmetry_comp {X : Type*} {T₁ T₂ : X → X} {J : X → ℝ}
  56    (h₁ : IsSymmetryOf T₁ J) (h₂ : IsSymmetryOf T₂ J) :
  57    IsSymmetryOf (T₁ ∘ T₂) J := by
  58  intro x
  59  simp only [Function.comp_apply, h₂ x, h₁ (T₂ x)]
  60
  61/-- **THEOREM**: Inverse of a bijective symmetry is a symmetry. -/
  62theorem symmetry_inv {X : Type*} [Nonempty X] {T : X → X} {J : X → ℝ}
  63    (hT : Function.Bijective T) (hsym : IsSymmetryOf T J) :
  64    IsSymmetryOf (Function.invFun T) J := by
  65  intro x
  66  have hinvr := Function.rightInverse_invFun hT.surjective
  67  rw [← hsym (Function.invFun T x)]
  68  congr 1
  69  exact hinvr x
  70
  71/-! ## Conserved Quantities -/
  72
  73/-- A quantity Q is conserved along a flow φ if it's constant on orbits. -/
  74def IsConservedAlong {X : Type*} (Q : X → ℝ) (φ : ℝ → X → X) : Prop :=
  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