Translations on space

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

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 - basis.repr.symm 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 - basis.repr.symm a)

noncomputable def Space.distTranslate {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.distTranslate a = { toFun := fun (T : (Space d)→d[ℝ] X) => ContinuousLinearMap.comp T (Space.translateSchwartz (-a)), map_add' := ⋯, map_smul' := ⋯ }

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

@[simp]

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

theorem Space.distTranslate_ofFunction {X : Type} [NormedAddCommGroup X] [NormedSpace ℝ X] {d : ℕ} (a : EuclideanSpace ℝ (Fin d.succ)) (f : Space d.succ → X) (hf : IsDistBounded f) : (distTranslate a) (distOfFunction f hf) = distOfFunction (fun (x : Space d.succ) => f (x - basis.repr.symm a)) ⋯

@[simp]

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