Actual bounded smooth coefficient paths from smooth L² jets

Finite-dimensional Sobolev evaluation supplies the uniform norm at every spatial order. The resulting coefficient path contains the original field and its actual derivative tensors; no bounded-derivative hypothesis is added.

Every actual spatial derivative tensor remains a smooth L² field.

noncomputable def EulerLpTranslation.SmoothL2Field.jetFieldAux (n : ℕ) (V : Type u) [NormedAddCommGroup V] [NormedSpace ℝ V] : SmoothL2Field V → SmoothL2Field (EulerSmoothLimit.Space [×n]→L[ℝ] V)

Jet field auxiliary, constructed using Nat.rec.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerLpTranslation.SmoothL2Field.jetField (n : ℕ) {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : SmoothL2Field (EulerSmoothLimit.Space [×n]→L[ℝ] V)

Jet field, given by jetFieldAux n V A.

Equations

• EulerLpTranslation.SmoothL2Field.jetField n A = EulerLpTranslation.SmoothL2Field.jetFieldAux n V A

@[simp]

theorem EulerLpTranslation.SmoothL2Field.jetField_zero {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : jetField 0 A = mapField (↑↑(continuousMultilinearCurryFin0 ℝ EulerSmoothLimit.Space V).symm) A

@[simp]

theorem EulerLpTranslation.SmoothL2Field.jetField_succ {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) : jetField (n + 1) A = mapField (↑↑(continuousMultilinearCurryRightEquiv' ℝ n EulerSmoothLimit.Space V).symm) (jetField n A.derivative)

@[simp]

theorem EulerLpTranslation.SmoothL2Field.jetField_field {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) (x : EulerSmoothLimit.Space) : (jetField n A).field x = iteratedFDeriv ℝ n A.field x

theorem EulerLpTranslation.SmoothL2Field.jetField_toLp {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) : (jetField n A).toLp = A.jetLp n

theorem EulerLpTranslation.SmoothL2Field.continuous_jetField_jet {K : Type v} [TopologicalSpace K] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : K → SmoothL2Field V) (hA : ∀ (k : ℕ), Continuous fun (t : K) => (A t).jetLp k) (n k : ℕ) : Continuous fun (t : K) => (jetField n (A t)).jetLp k

theorem EulerMeanSobolevBoundedField.tensorFiniteDimensional {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : FiniteDimensional ℝ (EulerSmoothLimit.Space [×n]→L[ℝ] V)

noncomputable def EulerMeanSobolevBoundedField.coefficientPath {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) : EulerMeanCoefficients.SmoothCoefficientPath K V

The actual raw L² family as a uniformly smooth bounded coefficient path.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerMeanSobolevBoundedField.coefficientPath_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (t : K) (x : EulerSmoothLimit.Space) : ((coefficientPath A hA).field t) x = (A t).field x