Dilation of test functions

Dilating the support of a test function by a nonzero real scalar amounts to precomposing with its inverse. The derivative, gradient and divergence acquire the inverse scalar. These formulas transport the test-field pairings that define distributional variation and perimeter under dilations, and the homogeneous Sobolev norms of test functions. Combining dilation with translation rescales a test vector field around a point x (TestFunction.exists_eq_comp); for small ratios the rescaled support stays inside any open neighbourhood of x (TauCeti.eventually_forall_tsupport_add_smul_mem).

noncomputable def TauCeti.dilateTestFunction {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} {r : ℝ} (hr : r ≠ 0) (hVO : Set.MapsTo (fun (x : E) => r • x) ↑V ↑Ω) (φ : TestFunction V F ⊤) : TestFunction Ω F ⊤

Dilate the support of a test function by r, regarding it as a test function on any open set containing the dilated original domain.

@[simp]

theorem TauCeti.dilateTestFunction_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} {r : ℝ} (hr : r ≠ 0) (hVO : Set.MapsTo (fun (x : E) => r • x) ↑V ↑Ω) (φ : TestFunction V F ⊤) (y : E) : (dilateTestFunction hr hVO φ) y = φ (r⁻¹ • y)

Evaluation of a test function whose support has been dilated.

@[simp]

theorem TauCeti.fderiv_dilateTestFunction {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} {r : ℝ} (hr : r ≠ 0) (hVO : Set.MapsTo (fun (x : E) => r • x) ↑V ↑Ω) (φ : TestFunction V F ⊤) (y : E) : fderiv ℝ (⇑(dilateTestFunction hr hVO φ)) y = r⁻¹ • fderiv ℝ (⇑φ) (r⁻¹ • y)

The derivative of a dilated test function acquires the inverse dilation factor.

@[simp]

theorem TauCeti.lineDeriv_dilateTestFunction {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} {r : ℝ} (hr : r ≠ 0) (hVO : Set.MapsTo (fun (x : E) => r • x) ↑V ↑Ω) (φ : TestFunction V F ⊤) (y w : E) : lineDeriv ℝ (⇑(dilateTestFunction hr hVO φ)) y w = r⁻¹ • lineDeriv ℝ (⇑φ) (r⁻¹ • y) w

The directional derivative of a dilated test function acquires the inverse dilation factor.

@[simp]

theorem TauCeti.divergenceCLM_dilateTestFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω V : TopologicalSpace.Opens E} {r : ℝ} [FiniteDimensional ℝ E] (hr : r ≠ 0) (hVO : Set.MapsTo (fun (x : E) => r • x) ↑V ↑Ω) (φ : TestFunction V E ⊤) : TestFunction.divergenceCLM (dilateTestFunction hr hVO φ) = r⁻¹ • dilateTestFunction hr hVO (TestFunction.divergenceCLM φ)

The divergence of a dilated test vector field acquires the inverse dilation factor.

@[simp]

theorem TauCeti.gradient_dilateTestFunction {r : ℝ} {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {Ω V : TopologicalSpace.Opens H} (hr : r ≠ 0) (hVO : Set.MapsTo (fun (x : H) => r • x) ↑V ↑Ω) (φ : TestFunction V ℝ ⊤) (y : H) : gradient (⇑(dilateTestFunction hr hVO φ)) y = r⁻¹ • gradient (⇑φ) (r⁻¹ • y)

The gradient of a dilated real test function acquires the inverse dilation factor.

theorem TauCeti.eventually_forall_tsupport_add_smul_mem {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {x : E} (hx : x ∈ Ω) (φ : TestFunction ⊤ F ⊤) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ y ∈ tsupport ⇑φ, x + r • y ∈ Ω

For small r > 0 the support of a test function on E, rescaled by r around x ∈ Ω, lies in Ω.

theorem TestFunction.exists_eq_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} [FiniteDimensional ℝ E] {x : E} (φ : TestFunction ⊤ E ⊤) {r : ℝ} (hr : r ≠ 0) (hΩ : ∀ y ∈ tsupport ⇑φ, x + r • y ∈ Ω) : ∃ (ψ : TestFunction Ω E ⊤), (∀ (y : E), ψ y = φ (r⁻¹ • (y - x))) ∧ ∀ (y : E), (divergenceCLM ψ) y = r⁻¹ * (divergenceCLM φ) (r⁻¹ • (y - x))

Rescaling a test vector field on E around x by a ratio r ≠ 0 gives a test vector field on Ω, provided the rescaled support lies in Ω.