symmetry_comp

formal source

  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
  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