Translations on space

We define translations on space, and how translations act on distributions. Translations for part of the Poincaré group.

noncomputable instance Space.instVAddEuclideanSpaceRealFin {d : ℕ} : VAdd (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

• Space.instVAddEuclideanSpaceRealFin = { vadd := fun (v : EuclideanSpace ℝ (Fin d)) (s : Space d) => v + s }

noncomputable instance Space.instAddActionEuclideanSpaceRealFin {d : ℕ} : AddAction (EuclideanSpace ℝ (Fin d)) (Space d)

Equations

• Space.instAddActionEuclideanSpaceRealFin = { toVAdd := Space.instVAddEuclideanSpaceRealFin, zero_vadd := ⋯, add_vadd := ⋯ }

Translations of distributions

noncomputable def Space.translateSchwartz {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) : SchwartzMap (Space d) X →L[ℝ] SchwartzMap (Space d) X

The continuous linear map translating Schwartz maps.

Equations

• Space.translateSchwartz a = SchwartzMap.compCLM ℝ ⋯ ⋯

@[simp]

theorem Space.translateSchwartz_apply {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (η : SchwartzMap (Space d) X) (x : Space d) : ((translateSchwartz a) η) x = η (x - a)

theorem Space.translateSchwartz_coe_eq {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (η : SchwartzMap (Space d) X) : ⇑((translateSchwartz a) η) = fun (x : Space d) => η (x - a)

noncomputable def Space.translateD {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) : ((Space d)→d[ℝ] X) →ₗ[ℝ] (Space d)→d[ℝ] X

The continuous linear map translating distributions.

Equations

• Space.translateD a = { toFun := fun (T : (Space d)→d[ℝ] X) => ContinuousLinearMap.comp T (Space.translateSchwartz (-a)), map_add' := ⋯, map_smul' := ⋯ }

theorem Space.translateD_apply {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (T : (Space d)→d[ℝ] X) (η : SchwartzMap (Space d) ℝ) : ((translateD a) T) η = T ((translateSchwartz (-a)) η)

@[simp]

theorem Space.translateD_distGrad {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (T : (Space d)→d[ℝ] ℝ) : distGrad ((translateD a) T) = (translateD a) (distGrad T)

theorem Space.translateD_ofFunction {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} (a : EuclideanSpace ℝ (Fin d.succ)) (f : Space d.succ → X) (hf : Distribution.IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : (translateD a) (Distribution.ofFunction f hf hae) = Distribution.ofFunction (fun (x : EuclideanSpace ℝ (Fin d.succ)) => f (x - a)) ⋯ ⋯

@[simp]

theorem Space.distDiv_translateD {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) (T : (Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) : distDiv ((translateD a) T) = (translateD a) (distDiv T)