Algebra of literal smooth square-integrable spatial fields

All jets below remain actual Fréchet derivatives. The operations preserve their genuine L² classes and continuity in an external parameter.

noncomputable def EulerLpTranslation.SmoothL2Field.jetPostcompose {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (n : ℕ) : (EulerSmoothLimit.Space [×n]→L[ℝ] V) →L[ℝ] EulerSmoothLimit.Space [×n]→L[ℝ] W

Jet postcompose, given by compContinuousMultilinearMapL ℝ (fun _ : Fin n => Space) V W L.

Equations

• EulerLpTranslation.SmoothL2Field.jetPostcompose L n = (ContinuousLinearMap.compContinuousMultilinearMapL ℝ (fun (x : Fin n) => EulerSmoothLimit.Space) V W) L

def EulerLpTranslation.SmoothL2Field.mapField {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothL2Field V) : SmoothL2Field W

Map field, bundling field, smooth, integrable.

Equations

• EulerLpTranslation.SmoothL2Field.mapField L A = { field := ⇑L ∘ A.field, smooth := ⋯, integrable := ⋯ }

@[simp]

theorem EulerLpTranslation.SmoothL2Field.mapField_field {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothL2Field V) (x : EulerSmoothLimit.Space) : (mapField L A).field x = L (A.field x)

theorem EulerLpTranslation.SmoothL2Field.toLp_mapField {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothL2Field V) : (mapField L A).toLp = (ContinuousLinearMap.compLpL 2 MeasureTheory.volume L) A.toLp

theorem EulerLpTranslation.SmoothL2Field.jetLp_mapField {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothL2Field V) (n : ℕ) : (mapField L A).jetLp n = (ContinuousLinearMap.compLpL 2 MeasureTheory.volume (jetPostcompose L n)) (A.jetLp n)

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

Add field, bundling field, smooth, integrable.

Equations

• A.addField B = { field := A.field + B.field, smooth := ⋯, integrable := ⋯ }

@[simp]

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

theorem EulerLpTranslation.SmoothL2Field.toLp_addField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothL2Field V) : (A.addField B).toLp = A.toLp + B.toLp

theorem EulerLpTranslation.SmoothL2Field.jetLp_addField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : SmoothL2Field V) (n : ℕ) : (A.addField B).jetLp n = A.jetLp n + B.jetLp n

def EulerLpTranslation.SmoothL2Field.zeroField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : SmoothL2Field V

Zero field, bundling field, smooth, integrable.

Equations

• EulerLpTranslation.SmoothL2Field.zeroField = { field := 0, smooth := ⋯, integrable := ⋯ }

theorem EulerLpTranslation.SmoothL2Field.jetLp_derivative {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) : A.derivative.jetLp n = (ContinuousLinearMap.compLpL 2 MeasureTheory.volume ↑↑(continuousMultilinearCurryRightEquiv' ℝ n EulerSmoothLimit.Space V)) (A.jetLp (n + 1))

noncomputable def EulerLpTranslation.SmoothL2Field.directionalField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (v : EulerSmoothLimit.Space) : SmoothL2Field V

Directional field, given by mapField (ContinuousLinearMap.apply ℝ V v) A.derivative.

Equations

• A.directionalField v = EulerLpTranslation.SmoothL2Field.mapField ((ContinuousLinearMap.apply ℝ V) v) A.derivative

@[simp]

theorem EulerLpTranslation.SmoothL2Field.directionalField_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (v x : EulerSmoothLimit.Space) : (A.directionalField v).field x = (fderiv ℝ A.field x) v

theorem EulerLpTranslation.SmoothL2Field.toLp_eq_jet_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) : A.toLp = (ContinuousLinearMap.compLpL 2 MeasureTheory.volume ↑↑(continuousMultilinearCurryFin0 ℝ EulerSmoothLimit.Space V)) (A.jetLp 0)

theorem EulerLpTranslation.SmoothL2Field.continuous_toLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_3} [TopologicalSpace K] (A : K → SmoothL2Field V) (hA : Continuous fun (t : K) => (A t).jetLp 0) : Continuous fun (t : K) => (A t).toLp

theorem EulerLpTranslation.SmoothL2Field.continuous_jetLp_mapField {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {K : Type u_3} [TopologicalSpace K] (L : V →L[ℝ] W) (A : K → SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (mapField L (A t)).jetLp n

theorem EulerLpTranslation.SmoothL2Field.continuous_jetLp_addField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_3} [TopologicalSpace K] (A B : K → SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : K) => (B t).jetLp n) (n : ℕ) : Continuous fun (t : K) => ((A t).addField (B t)).jetLp n

theorem EulerLpTranslation.SmoothL2Field.continuous_jetLp_derivative {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_3} [TopologicalSpace K] (A : K → SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (A t).derivative.jetLp n

theorem EulerLpTranslation.SmoothL2Field.continuous_jetLp_directionalField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_3} [TopologicalSpace K] (A : K → SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (v : EulerSmoothLimit.Space) (n : ℕ) : Continuous fun (t : K) => ((A t).directionalField v).jetLp n