Exact identification of ordinary spatial derivatives with all translation jets in L².

theorem EulerLpTranslation.SmoothL2Field.jetLp_ae {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) : ↑↑(A.jetLp n) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n A.field

theorem EulerLpTranslation.SmoothL2Field.iteratedFDeriv_translation_ae {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) (a : EulerSmoothLimit.Space) (v : Fin n → EulerSmoothLimit.Space) : ↑↑((iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (translation b) A.toLp) a) v) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => (iteratedFDeriv ℝ n A.field (x + a)) v

theorem EulerLpTranslation.SmoothL2Field.iteratedFDeriv_translation_eq {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) (a : EulerSmoothLimit.Space) : iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (translation b) A.toLp) a = (EulerLpDerivative.multilinearBundling MeasureTheory.volume n) ((translation a) (A.jetLp n))

The entire parameter derivative tensor is a bounded linear image of the actual spatial L² tensor.