Continuous paths and actual mixed translations in supported cylinder L²

Inclusion and measurable-set projection act on actual continuous L² paths. Projected translations form globally defined parameter families. Whenever a translated compact support lies in the target region, the projection is the identity, so these families are the true mixed translations there.

@[reducible, inline]

noncomputable abbrev EulerLpCylinderPaths.Supported (period : ℝ) [Fact (0 < period)] (V : Type u_1) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : Submodule ℝ ↥(MeasureTheory.Lp V 2 (EulerLiftedGradientSpace.liftMeasure period))

Supported: an abbreviation for supportedSpace (V := V) (liftMeasure period) (spatialSet period S) (spatialSet_measurable period S hS).

Equations

• EulerLpCylinderPaths.Supported period V S hS = EulerLpSupportedSubspace.supportedSpace (EulerLiftedGradientSpace.liftMeasure period) (EulerLpCylinderTranslation.spatialSet period S) ⋯

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths1 (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period V)

Cache the standard NormedAddCommGroup (CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths1 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths2 (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period V)

Cache the standard NormedSpace ℝ (CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths2 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths3 (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(Supported period V S hS)

Cache the standard NormedAddCommGroup (Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths3 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths4 (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ ↥(Supported period V S hS)

Cache the standard NormedSpace ℝ (Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths4 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths5 (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))

Cache the standard NormedAddCommGroup C(K,CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths5 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths6 (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))

Cache the standard NormedSpace ℝ C(K,CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths6 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths7 (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup C(K, ↥(Supported period V S hS))

Cache the standard NormedAddCommGroup C(K,Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths7 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderPaths.instLpCylinderPaths8 (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ C(K, ↥(Supported period V S hS))

Cache the standard NormedSpace ℝ C(K,Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderPaths.instLpCylinderPaths8 period S hS = inferInstance

noncomputable def EulerLpCylinderPaths.includePath (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : C(K, ↥(Supported period V S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))

Inclusion of a supported path into the genuine ordinary L² path space.

Equations

• EulerLpCylinderPaths.includePath period S hS = ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpCylinderPaths.Supported period V S hS).subtypeL

noncomputable def EulerLpCylinderPaths.projectPath (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V)) →L[ℝ] C(K, ↥(Supported period V S hS))

Projection of each ordinary L² value to the fixed supported subspace.

Equations

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

@[simp]

theorem EulerLpCylinderPaths.includePath_apply (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(K, ↥(Supported period V S hS))) (t : K) : ((includePath period S hS) f) t = ↑(f t)

@[simp]

theorem EulerLpCylinderPaths.projectPath_apply (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))) (t : K) : ((projectPath period S hS) f) t = (EulerLpSupportedSubspace.projection (EulerLiftedGradientSpace.liftMeasure period) (EulerLpCylinderTranslation.spatialSet period S) ⋯) (f t)

theorem EulerLpCylinderPaths.includePath_norm (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ‖includePath period S hS‖ ≤ 1

Time-path inclusion is a contraction (indeed an isometry).

theorem EulerLpCylinderPaths.projectPath_norm (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ‖projectPath period S hS‖ ≤ 1

Supported projection is a contraction also in the uniform time norm.

theorem EulerLpCylinderPaths.project_include (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(K, ↥(Supported period V S hS))) : (projectPath period S hS) ((includePath period S hS) f) = f

Projecting an already supported continuous path fixes it.

noncomputable def EulerLpCylinderPaths.translatedData (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period V)) (a : EulerLiftedGradientSpace.LiftTangent) : ↥(Supported period V S hS)

A globally defined actual mixed translation followed by supported projection.

Equations

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

noncomputable def EulerLpCylinderPaths.translatedForcing (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))) (a : EulerLiftedGradientSpace.LiftTangent) : C(K, ↥(Supported period V S hS))

The corresponding globally defined family of actual continuous forcing paths.

Equations

• EulerLpCylinderPaths.translatedForcing period S hS f a = (EulerLpCylinderPaths.projectPath period S hS) ((EulerLpCylinderTranslation.pathTranslate period a) f)

theorem EulerLpCylinderPaths.translatedData_eq_intoLarger (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (S₀ : Set EulerSmoothLimit.Space) (hS₀ : MeasurableSet S₀) (u : ↥(Supported period V S₀ hS₀)) (a : EulerLiftedGradientSpace.LiftTangent) (ha : EulerLpSupportedTranslation.shiftedSet a.1 S₀ ⊆ S) : translatedData period S hS (↑u) a = (EulerLpCylinderTranslation.intoLarger period a S₀ S hS₀ hS ha) u

On the allowed translation neighborhood, projected data are exact translations.

theorem EulerLpCylinderPaths.translatedForcing_eq_intoLarger (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (S₀ : Set EulerSmoothLimit.Space) (hS₀ : MeasurableSet S₀) (f : C(K, ↥(Supported period V S₀ hS₀))) (a : EulerLiftedGradientSpace.LiftTangent) (ha : EulerLpSupportedTranslation.shiftedSet a.1 S₀ ⊆ S) : translatedForcing period S hS ((includePath period S₀ hS₀) f) a = (ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpCylinderTranslation.intoLarger period a S₀ S hS₀ hS ha).toContinuousLinearMap) f

The same exact identity holds for whole continuous forcing paths.

theorem EulerLpCylinderPaths.translatedData_contDiff (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period V)) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) : ContDiff ℝ (↑⊤) (translatedData period S hS u)

Smoothness is inherited from the true ordinary L² translation orbit.

theorem EulerLpCylinderPaths.norm_iteratedFDeriv_translatedData_le (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period V)) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (translatedData period S hS u) a‖ ≤ ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) u) a‖

The supported parameter family has no larger actual derivative norm.

theorem EulerLpCylinderPaths.translatedForcing_contDiff (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) : ContDiff ℝ (↑⊤) (translatedForcing period S hS f)

Uniform-time orbit smoothness is preserved by the fixed support projection.

theorem EulerLpCylinderPaths.norm_iteratedFDeriv_translatedForcing_le (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (f : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (translatedForcing period S hS f) a‖ ≤ ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period b) f) a‖

The projected forcing jets are bounded by the genuine uniform-time spatial orbit jets.

theorem EulerLpCylinderPaths.translatedData_block_le (period : ℝ) [Fact (0 < period)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {ι : Type u_3} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period V)) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (translatedData period S hS u) n a ≤ EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) u) n a

The true mixed initial-data derivative blocks are unchanged by support projection.

theorem EulerLpCylinderPaths.translatedForcing_block_le (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {ι : Type u_3} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (f : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period V))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (translatedForcing period S hS f) n a ≤ EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period b) f) n a

The true mixed forcing derivative blocks are unchanged by support projection.

theorem EulerLpCylinderPaths.includePath_block_le (period : ℝ) [Fact (0 < period)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) {ι : Type u_3} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (u : EulerLiftedGradientSpace.LiftTangent → C(K, ↥(Supported period V S hS))) (hu : ContDiff ℝ (↑⊤) u) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (includePath period S hS) (u b)) n a ≤ EulerParameterWordGevrey.block directions q u n a

Inclusion transfers the same fixed-Hq block to actual cylinder L².