Physlib.SpaceAndTime.TimeAndSpace.EuclideanGroup.Action

Imports

/-
Copyright (c) 2026 Rob Sneiderman. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rob Sneiderman
-/
module

public import Physlib.SpaceAndTime.Space.EuclideanGroup.Action
public import Physlib.SpaceAndTime.TimeAndSpace.Basic

The action of the Euclidean group on `TimeAndSpace`

i. Overview

In this file we define the action of the Euclidean group on TimeAndSpace d. The action fixes the time coordinate and acts on the space coordinate by the usual Euclidean-group action on Space d.

ii. Key results

TimeAndSpace.instMulActionEuclideanGroup : The action of the Euclidean group on TimeAndSpace d.

TimeAndSpace.dist_smul : The Euclidean group action on TimeAndSpace d preserves distance.

TimeAndSpace.smul_hasTemperateGrowth : The Euclidean group action has temperate growth.

TimeAndSpace.antilipschitz_smul : The Euclidean group action is antilipschitz.

iii. Table of contents

A. The Euclidean group action

B. Temperate growth of the coordinate action

iv. References

@[expose] public section

A. The Euclidean group action

Coordinate formula for the Euclidean-group action on TimeAndSpace d.

@[simp]
lemma smul_mk (g : EuclideanGroup d) (t : Time) (x : Space d) :
    g • ((t, x) : TimeAndSpace d) = (t, g • x) := byd:ℕg:EuclideanGroup dt:Timex:Space d⊢ g • (t, x) = (t, g • x)
  show ((t, g • x) : TimeAndSpace d) = (t, g • x)d:ℕg:EuclideanGroup dt:Timex:Space d⊢ (t, g • x) = (t, g • x)
  rflAll goals completed! 🐙

The Euclidean-group action fixes the first coordinate.


@[simp]
lemma fst_smul (g : EuclideanGroup d) (tx : TimeAndSpace d) :
    (g • tx).1 = tx.1 := byd:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ (g • tx).1 = tx.1
  rcases tx with ⟨t, x⟩d:ℕg:EuclideanGroup dt:Timex:Space d⊢ (g • (t, x)).1 = (t, x).1
  rw [smul_mkd:ℕg:EuclideanGroup dt:Timex:Space d⊢ (t, g • x).1 = (t, x).1All goals completed! 🐙]All goals completed! 🐙

The Euclidean-group action applies to the second coordinate.


@[simp]
lemma snd_smul (g : EuclideanGroup d) (tx : TimeAndSpace d) :
    (g • tx).2 = g • tx.2 := byd:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ (g • tx).2 = g • tx.2
  rcases tx with ⟨t, x⟩d:ℕg:EuclideanGroup dt:Timex:Space d⊢ (g • (t, x)).2 = g • (t, x).2
  rw [smul_mkd:ℕg:EuclideanGroup dt:Timex:Space d⊢ (t, g • x).2 = g • (t, x).2All goals completed! 🐙]All goals completed! 🐙

The Euclidean-group action fixes the time projection.

lemma time_smul (g : EuclideanGroup d) (tx : TimeAndSpace d) :
    time (g • tx) = time tx := byd:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ time (g • tx) = time tx
  simp [time]All goals completed! 🐙

The Euclidean-group action applies to the space projection.

lemma space_smul (g : EuclideanGroup d) (tx : TimeAndSpace d) :
    space (g • tx) = g • space tx := byd:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ space (g • tx) = g • space tx
  simp [space]All goals completed! 🐙

The Euclidean-group action on TimeAndSpace d preserves product distance.


lemma dist_smul (g : EuclideanGroup d) (tx ty : TimeAndSpace d) :
    dist (g • tx) (g • ty) = dist tx ty := byd:ℕg:EuclideanGroup dtx:TimeAndSpace dty:TimeAndSpace d⊢ dist (g • tx) (g • ty) = dist tx ty
  rcases tx with ⟨t, x⟩d:ℕg:EuclideanGroup dty:TimeAndSpace dt:Timex:Space d⊢ dist (g • (t, x)) (g • ty) = dist (t, x) ty
  rcases ty with ⟨t', x'⟩d:ℕg:EuclideanGroup dt:Timex:Space dt':Timex':Space d⊢ dist (g • (t, x)) (g • (t', x')) = dist (t, x) (t', x')
  show dist ((t, g • x) : TimeAndSpace d) (t', g • x') = dist (t, x) (t', x')d:ℕg:EuclideanGroup dt:Timex:Space dt':Timex':Space d⊢ dist (t, g • x) (t', g • x') = dist (t, x) (t', x')
  rw [Prod.dist_eq,d:ℕg:EuclideanGroup dt:Timex:Space dt':Timex':Space d⊢ max (dist (t, g • x).1 (t', g • x').1) (dist (t, g • x).2 (t', g • x').2) = dist (t, x) (t', x')All goals completed! 🐙 Prod.dist_eq,d:ℕg:EuclideanGroup dt:Timex:Space dt':Timex':Space d⊢ max (dist (t, g • x).1 (t', g • x').1) (dist (t, g • x).2 (t', g • x').2) =
  max (dist (t, x).1 (t', x').1) (dist (t, x).2 (t', x').2)All goals completed! 🐙 EuclideanGroup.dist_smuld:ℕg:EuclideanGroup dt:Timex:Space dt':Timex':Space d⊢ max (dist (t, g • x).1 (t', g • x').1) (dist x x') = max (dist (t, x).1 (t', x').1) (dist (t, x).2 (t', x').2)All goals completed! 🐙]All goals completed! 🐙

B. Temperate growth of the coordinate action



lemma smul_eq_actionLinearMap_add (g : EuclideanGroup d) (tx : TimeAndSpace d) :
    g • tx = actionLinearMap g tx + actionTranslation g := byd:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ g • tx = (actionLinearMap g) tx + actionTranslation g
  refine Prod.ext ?_ ?_refine_1d:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ (g • tx).1 = ((actionLinearMap g) tx + actionTranslation g).1refine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ (g • tx).2 = ((actionLinearMap g) tx + actionTranslation g).2
  ·refine_1d:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ (g • tx).1 = ((actionLinearMap g) tx + actionTranslation g).1 simp [actionLinearMap, actionTranslation]All goals completed! 🐙
  ·refine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ (g • tx).2 = ((actionLinearMap g) tx + actionTranslation g).2 ext irefine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin d⊢ (g • tx).2.val i = ((actionLinearMap g) tx + actionTranslation g).2.val i
    have hx : tx.2 -ᵥ (0 : Space d) = Space.basis.repr tx.2 := byd:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ g • tx = (actionLinearMap g) tx + actionTranslation grefine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g • tx).2.val i = ((actionLinearMap g) tx + actionTranslation g).2.val i
      ext jd:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dj:Fin d⊢ (tx.2 -ᵥ 0).ofLp j = (Space.basis.repr tx.2).ofLp jrefine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g • tx).2.val i = ((actionLinearMap g) tx + actionTranslation g).2.val i
      simp [Space.vsub_apply, Space.zero_apply, Space.basis_repr_apply]refine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g • tx).2.val i = ((actionLinearMap g) tx + actionTranslation g).2.val irefine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g • tx).2.val i = ((actionLinearMap g) tx + actionTranslation g).2.val i
    rw [TimeAndSpace.snd_smul,refine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g • tx.2).val i = ((actionLinearMap g) tx + actionTranslation g).2.val irefine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g.linear • (tx.2 -ᵥ 0)).ofLp i + g.translation.ofLp i = ((actionLinearMap g) tx + actionTranslation g).2.val i EuclideanGroup.smul_applyrefine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g.linear • (tx.2 -ᵥ 0)).ofLp i + g.translation.ofLp i = ((actionLinearMap g) tx + actionTranslation g).2.val irefine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g.linear • (tx.2 -ᵥ 0)).ofLp i + g.translation.ofLp i = ((actionLinearMap g) tx + actionTranslation g).2.val i]refine_2d:ℕg:EuclideanGroup dtx:TimeAndSpace di:Fin dhx:tx.2 -ᵥ 0 = Space.basis.repr tx.2⊢ (g.linear • (tx.2 -ᵥ 0)).ofLp i + g.translation.ofLp i = ((actionLinearMap g) tx + actionTranslation g).2.val i
    simp [actionLinearMap, actionTranslation, hx, Space.add_apply, Space.basis_repr_symm_apply]All goals completed! 🐙

The Euclidean-group action on TimeAndSpace d has temperate growth.


lemma smul_hasTemperateGrowth (g : EuclideanGroup d) :
    Function.HasTemperateGrowth (fun tx : TimeAndSpace d => g • tx) := byd:ℕg:EuclideanGroup d⊢ Function.HasTemperateGrowth fun tx => g • tx
  have hfun : (fun tx : TimeAndSpace d => g • tx) =
      fun tx => actionLinearMap g tx + actionTranslation g := by
    funext txd:ℕg:EuclideanGroup dtx:TimeAndSpace d⊢ g • tx = (actionLinearMap g) tx + actionTranslation gd:ℕg:EuclideanGroup dhfun:(fun tx => g • tx) = fun tx => (actionLinearMap g) tx + actionTranslation g⊢ Function.HasTemperateGrowth fun tx => g • tx
    exact smul_eq_actionLinearMap_add g txd:ℕg:EuclideanGroup dhfun:(fun tx => g • tx) = fun tx => (actionLinearMap g) tx + actionTranslation g⊢ Function.HasTemperateGrowth fun tx => g • txd:ℕg:EuclideanGroup dhfun:(fun tx => g • tx) = fun tx => (actionLinearMap g) tx + actionTranslation g⊢ Function.HasTemperateGrowth fun tx => g • tx
  rw [hfund:ℕg:EuclideanGroup dhfun:(fun tx => g • tx) = fun tx => (actionLinearMap g) tx + actionTranslation g⊢ Function.HasTemperateGrowth fun tx => (actionLinearMap g) tx + actionTranslation gd:ℕg:EuclideanGroup dhfun:(fun tx => g • tx) = fun tx => (actionLinearMap g) tx + actionTranslation g⊢ Function.HasTemperateGrowth fun tx => (actionLinearMap g) tx + actionTranslation g]d:ℕg:EuclideanGroup dhfun:(fun tx => g • tx) = fun tx => (actionLinearMap g) tx + actionTranslation g⊢ Function.HasTemperateGrowth fun tx => (actionLinearMap g) tx + actionTranslation g
  exact Function.HasTemperateGrowth.add (actionLinearMap g).hasTemperateGrowth
    (Function.HasTemperateGrowth.const (actionTranslation g))All goals completed! 🐙

The Euclidean-group action on TimeAndSpace d is an isometry.

lemma isometry_smul (g : EuclideanGroup d) :
    Isometry (fun tx : TimeAndSpace d => g • tx) :=
  Isometry.of_dist_eq (TimeAndSpace.dist_smul g)

The Euclidean-group action on TimeAndSpace d is antilipschitz.

lemma antilipschitz_smul (g : EuclideanGroup d) :
    AntilipschitzWith 1 (fun tx : TimeAndSpace d => g • tx) :=
  (isometry_smul g).antilipschitz

The action of the Euclidean group on TimeAndSpace

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The Euclidean group action

B. Temperate growth of the coordinate action

The action of the Euclidean group on `TimeAndSpace`