Physical spatial dilation preserves continuity of every actual L² jet. The proof uses its explicit bounded action on differences.

def EulerLpTranslation.SmoothL2Field.subField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothL2Field V) : SmoothL2Field V

Sub field, bundling field, smooth, integrable.

Equations

• A.subField B = { field := A.field - B.field, smooth := ⋯, integrable := ⋯ }

@[simp]

theorem EulerLpTranslation.SmoothL2Field.subField_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothL2Field V) (x : EulerSmoothLimit.Space) : (A.subField B).field x = A.field x - B.field x

theorem EulerLpTranslation.SmoothL2Field.jetLp_subField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothL2Field V) (n : ℕ) : (A.subField B).jetLp n = A.jetLp n - B.jetLp n

theorem EulerLpTranslation.SmoothL2Field.norm_jetLp_scale_sub_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (A B : SmoothL2Field V) (n : ℕ) : ‖(scaleField ell hell A).jetLp n - (scaleField ell hell B).jetLp n‖ ≤ ell⁻¹ ^ n * ‖A.jetLp n - B.jetLp n‖

theorem EulerLpTranslation.SmoothL2Field.continuous_jetLp_scaleField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (A : K → SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (scaleField ell hell (A t)).jetLp n