Smoothness of the actual translated continuous Sobolev path

The finite Sobolev array consists of genuine derivative words of the given L² orbit. A bounded retraction of the closed compatible-array space proves its smoothness in the complete Hq path norm. It is used qualitatively only.

Every closed subspace of a finite product of Hilbert spaces has a bounded retraction. We use the equivalent Hilbert product norm only to construct the retraction; all stated spaces retain their original sup norms.

def EulerHilbertProductSubspace.hilbertEquiv {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : (ι → E) ≃L[ℝ] PiLp 2 fun (x : ι) => E

Hilbert equiv, given by (PiLp.continuousLinearEquiv 2 ℝ (fun _ : ι => E)).symm.

Equations

• EulerHilbertProductSubspace.hilbertEquiv = (PiLp.continuousLinearEquiv 2 ℝ fun (x : ι) => E).symm

def EulerHilbertProductSubspace.hilbertSubspace {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : ClosedSubmodule ℝ (ι → E)) : ClosedSubmodule ℝ (PiLp 2 fun (x : ι) => E)

Hilbert subspace, given by S.mapEquiv hilbertEquiv.

Equations

• EulerHilbertProductSubspace.hilbertSubspace S = (ClosedSubmodule.mapEquiv EulerHilbertProductSubspace.hilbertEquiv) S

def EulerHilbertProductSubspace.restriction {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : ClosedSubmodule ℝ (ι → E)) : ↥(hilbertSubspace S) →L[ℝ] ↥S

Restriction as an element of hilbertSubspace S →L[ℝ] S.

Equations

• EulerHilbertProductSubspace.restriction S = (↑EulerHilbertProductSubspace.hilbertEquiv.symm ∘SL (↑(EulerHilbertProductSubspace.hilbertSubspace S)).subtypeL).codRestrict ↑S ⋯

noncomputable def EulerHilbertProductSubspace.retraction {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : ClosedSubmodule ℝ (ι → E)) : (ι → E) →L[ℝ] ↥S

A genuine bounded retraction, obtained from orthogonal projection in the equivalent Hilbert norm.

Equations

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

@[simp]

theorem EulerHilbertProductSubspace.retraction_subtype {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : ClosedSubmodule ℝ (ι → E)) (u : ↥S) : (retraction S) ↑u = u

noncomputable def EulerHilbertProductSubspace.packPaths {ι : Type u_1} [Fintype ι] {K : Type u_3} {V : Type u_4} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] : (ι → C(K, V)) →L[ℝ] C(K, ι → V)

Interchange a finite tuple and a continuous path by a bounded linear map.

Equations

• EulerHilbertProductSubspace.packPaths = ∑ i : ι, ContinuousLinearMap.compLeftContinuous ℝ K (ContinuousLinearMap.single ℝ (fun (x : ι) => V) i) ∘SL ContinuousLinearMap.proj i

@[simp]

theorem EulerHilbertProductSubspace.packPaths_apply {ι : Type u_1} [Fintype ι] {K : Type u_3} {V : Type u_4} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (p : ι → C(K, V)) (t : K) (i : ι) : (packPaths p) t i = (p i) t

noncomputable def EulerCylinderSmoothOrbit.sobolevPathTranslate (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (q : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) →L[ℝ] C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P q))

Sobolev path translate, given by (sobolevTranslation P q (coveringMap P a)).compLeftContinuous ℝ K.

Equations

• EulerCylinderSmoothOrbit.sobolevPathTranslate P q a = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderSobolevSpace.sobolevTranslation P q (EulerLiftedGradientSpace.coveringMap P a))

noncomputable def EulerCylinderSmoothOrbit.sobolevOrbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (a : EulerLiftedGradientSpace.LiftTangent) : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P q))

Sobolev orbit, given by sobolevPathTranslate P q a (sobolevPath P q p hp).

Equations

• EulerCylinderSmoothOrbit.sobolevOrbit P q p hp a = (EulerCylinderSmoothOrbit.sobolevPathTranslate P q a) (EulerCylinderSmoothOrbit.sobolevPath P q p hp)

@[simp]

theorem EulerCylinderSmoothOrbit.sobolevOrbit_value (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (a : EulerLiftedGradientSpace.LiftTangent) (t : K) : EulerCylinderSobolevSpace.value P ((sobolevOrbit P q p hp a) t) = ((EulerLpCylinderTranslation.pathTranslate P a) p) t

theorem EulerCylinderSmoothOrbit.sobolevOrbit_coordinate (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (a : EulerLiftedGradientSpace.LiftTangent) (t : K) (w : EulerCylinderSobolevSpace.SobolevWord q) : ↑((sobolevOrbit P q p hp a) t) w = (EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) w.snd a) t

noncomputable def EulerCylinderSmoothOrbit.assembleSobolevPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (q : ℕ) : (EulerCylinderSobolevSpace.SobolevWord q → C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) →L[ℝ] C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P q))

Assemble sobolev path, given by ((retraction (sobolevSubspace P q)).compLeftContinuous ℝ K).comp packPaths.

Equations

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

theorem EulerCylinderSmoothOrbit.sobolevOrbit_eq_assemble (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (a : EulerLiftedGradientSpace.LiftTangent) : sobolevOrbit P q p hp a = (assembleSobolevPath P q) fun (w : EulerCylinderSobolevSpace.SobolevWord q) => EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) w.snd a

theorem EulerCylinderSmoothOrbit.sobolevOrbit_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ (↑⊤) (sobolevOrbit P q p hp)

Actual L² orbit smoothness promotes to every fixed complete Sobolev path space.