Translation of test functions

This file translates a test function on an open set V in the opposite direction to a vector h, producing a test function on any open set Ω that contains V + h. This is the common test-function operation used to prove translation invariance of weak derivatives.

Main declarations

• TauCeti.translateTestFunction: translate a test function while changing its domain.
• TauCeti.translateTestFunction_apply: evaluation of a translated test function.
• TauCeti.lineDeriv_translateTestFunction: directional derivatives commute with translation.

noncomputable def TauCeti.translateTestFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega V : TopologicalSpace.Opens E} {h : E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) (phi : TestFunction V ℝ ⊤) : TestFunction Omega ℝ ⊤

Translate a test function in the opposite direction, regarding it as a test function on an open set containing the translated support.

Equations

• TauCeti.translateTestFunction hVO phi = { toFun := fun (y : E) => phi (y - h), contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ }

@[simp]

theorem TauCeti.translateTestFunction_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega V : TopologicalSpace.Opens E} {h : E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) (phi : TestFunction V ℝ ⊤) (y : E) : (translateTestFunction hVO phi) y = phi (y - h)

Translating a test function evaluates it at the oppositely translated point.

@[simp]

theorem TauCeti.lineDeriv_translateTestFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega V : TopologicalSpace.Opens E} {h : E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Omega) (phi : TestFunction V ℝ ⊤) (y w : E) : lineDeriv ℝ (⇑(translateTestFunction hVO phi)) y w = lineDeriv ℝ (⇑phi) (y - h) w

The directional derivative of a translated test function is the translated directional derivative.