The actual fixed-space family for a genuinely regular bounded forward coefficient

The family is constructed from translated coefficient fields and projected translations of the original data. All homogeneous evolutions are obtained from the proved Picard construction. On the support-margin neighborhood it is exactly the mixed cylinder translation orbit of the original solution. Only the zero-parameter propagator uses the quantitative H3 assumption.

The cylinder forward solution has its actual mixed translation orbit

The coefficient intertwining identity and uniqueness identify the translated initial-value problem with the genuine mixed translation of the original solution. Compact support gives an equality on a neighborhood of the zero translation. No norm estimate depends on the size of that neighborhood.

Genuine scalar-profile normalization commutes with bounded linear intertwiners.

theorem EulerLinearDuhamel.Evolution.weightedSolution_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} {D : C(↑(Set.Icc 0 T), F →L[ℝ] F)} (U : Evolution T hT B) (V : Evolution T hT D) (L : E →L[ℝ] F) (hL : ∀ (t : ↑(Set.Icc 0 T)) (u : E), (D t) (L u) = L ((B t) u)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : V.weightedSolution g hg ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) L) f) (L a₀) = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) L) (U.weightedSolution g hg f a₀)

Exact naturality of the actual normalized Duhamel solution.

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation1 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period V)

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

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation1 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation2 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period V)

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

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation2 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation3 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (K : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period V K hK)

Cache the standard NormedAddCommGroup (Supported period V K hK) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation3 period K hK = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation4 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (K : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported period V K hK)

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

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation4 period K hK = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation5 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period V Ω hΩ)

Cache the standard NormedAddCommGroup (Supported period V Ω hΩ) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation5 period Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation6 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported period V Ω hΩ)

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

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation6 period Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation7 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 period V))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation7 period T = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation8 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 period V))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation8 period T = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation9 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (K : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V K hK))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,Supported period V K hK) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation9 period T K hK = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation10 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (K : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V K hK))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,Supported period V K hK) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation10 period T K hK = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation11 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V Ω hΩ))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,Supported period V Ω hΩ) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation11 period T Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation12 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V Ω hΩ))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,Supported period V Ω hΩ) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderSolutionTranslation.instLpCylinderSolutionTranslation12 period T Ω hΩ = inferInstance

theorem EulerLpCylinderSolutionTranslation.weighted_solution_translation (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (K Ω : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath period K hK T B)) (a : EulerLiftedGradientSpace.LiftTangent) (ha : EulerLpSupportedTranslation.shiftedSet a.1 K ⊆ Ω) (W : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath period Ω hΩ T (EulerMeanCoefficients.translateCoefficientPath B a.1))) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V K hK))) (a₀ : ↥(EulerLpCylinderPaths.Supported period V K hK)) : (EulerLpCylinderPaths.includePath period Ω hΩ) (W.weightedSolution g hg (EulerLpCylinderPaths.translatedForcing period Ω hΩ ((EulerLpCylinderPaths.includePath period K hK) f) a) (EulerLpCylinderPaths.translatedData period Ω hΩ (↑a₀) a)) = (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period K hK) (U.weightedSolution g hg f a₀))

The normalized supported solution has the actual normalized translation orbit.

theorem EulerLpCylinderSolutionTranslation.weighted_solution_translation_eventually (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (K Ω : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), EulerLpSupportedMultiplier.Field)) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath period K hK T B)) (hKc : IsCompact K) (hΩo : IsOpen Ω) (hsub : K ⊆ Ω) (W : (a : EulerLiftedGradientSpace.LiftTangent) → EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath period Ω hΩ T (EulerMeanCoefficients.translateCoefficientPath B a.1))) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V K hK))) (a₀ : ↥(EulerLpCylinderPaths.Supported period V K hK)) : (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderPaths.includePath period Ω hΩ) ((W a).weightedSolution g hg (EulerLpCylinderPaths.translatedForcing period Ω hΩ ((EulerLpCylinderPaths.includePath period K hK) f) a) (EulerLpCylinderPaths.translatedData period Ω hΩ (↑a₀) a))) =ᶠ[nhds 0] fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period K hK) (U.weightedSolution g hg f a₀))

Normalization preserves the exact local translation identification.

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward1 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedRing (V →L[ℝ] V)

Cache the standard NormedRing (V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward2 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedRing (BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))

Cache the standard NormedRing (Space →ᵇ V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward3 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period V)

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

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward3 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward4 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period V)

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

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward4 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward5 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period V Ω hΩ)

Cache the standard NormedAddCommGroup (Supported period V Ω hΩ) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward5 period Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward6 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported period V Ω hΩ)

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

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward6 period Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward7 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 period V))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward7 period T = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward8 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 period V))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 period V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward8 period T = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward9 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V Ω hΩ))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,Supported period V Ω hΩ) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward9 period T Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularForward10 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V Ω hΩ))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,Supported period V Ω hΩ) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRegularForward.instLpCylinderRegularForward10 period T Ω hΩ = inferInstance

noncomputable def EulerLpCylinderRegularForward.coefficientFamily (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (a : EulerLiftedGradientSpace.LiftTangent) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V Ω hΩ) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V Ω hΩ))

The actual multiplication coefficient on the one fixed supported space.

Equations

• EulerLpCylinderRegularForward.coefficientFamily period T Ω hΩ B a = EulerLpCylinderCoefficients.liftedOperatorPath period Ω hΩ T (EulerMeanCoefficients.translateCoefficientPath B a.1)

noncomputable def EulerLpCylinderRegularForward.evolutionFamily (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (a : EulerLiftedGradientSpace.LiftTangent) : EulerLinearDuhamel.Evolution T hT (coefficientFamily period T Ω hΩ B a)

Its homogeneous evolution is constructed, not assumed.

Equations

• EulerLpCylinderRegularForward.evolutionFamily period T hT Ω hΩ B a = EulerLpCylinderCoefficients.constructedEvolution period Ω hΩ T hT (EulerMeanCoefficients.translateCoefficientPath B a.1)

noncomputable def EulerLpCylinderRegularForward.solutionFamily (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 period V))) (a₀ : ↥(EulerLpCylinderTranslation.CylinderL2 period V)) (a : EulerLiftedGradientSpace.LiftTangent) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V Ω hΩ))

The genuine profile-normalized forced solution in this fixed space.

Equations

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

theorem EulerLpCylinderRegularForward.solutionFamily_contDiff (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 period V))) (a₀ : ↥(EulerLpCylinderTranslation.CylinderL2 period V)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) a₀) : ContDiff ℝ (↑⊤) (solutionFamily period T hT Ω hΩ B g hg f a₀)

Actual coefficient and data regularity give actual smoothness of the solved family.

theorem EulerLpCylinderRegularForward.evolutionFamily_propagator_zero (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (g : ↑(Set.Icc 0 T) → ℝ) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (C : ℝ) (hC : 0 ≤ C) (hprop : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ x ∈ Ω, ‖((EulerLinearFundamentalExistence.fundamentalPath T hT B).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath T hT B).backward s) x‖ ≤ C * g t / g s) (t s : ↑(Set.Icc 0 T)) (hst : s ≤ t) : ‖(evolutionFamily period T hT Ω hΩ B 0).propagator t s‖ ≤ C * g t / g s

Localized pointwise H3 is precisely the needed base-parameter L² bound.

theorem EulerLpCylinderRegularForward.solutionFamily_translation_eventually (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (K : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) (hKc : IsCompact K) (hΩo : IsOpen Ω) (hsub : K ⊆ Ω) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V K hK))) (a₀ : ↥(EulerLpCylinderPaths.Supported period V K hK)) : (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderPaths.includePath period Ω hΩ) (solutionFamily period T hT Ω hΩ B g hg ((EulerLpCylinderPaths.includePath period K hK) f) (↑a₀) a)) =ᶠ[nhds 0] fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period K hK) ((EulerLpCylinderCoefficients.constructedEvolution period K hK T hT B).weightedSolution g hg f a₀))

The locally translated family equals the actual cylinder L² mixed translation orbit of the actual normalized source solution.

theorem EulerLpCylinderRegularForward.source_solution_contDiff (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (K : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) (hKc : IsCompact K) (hΩo : IsOpen Ω) (hsub : K ⊆ Ω) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V K hK))) (a₀ : ↥(EulerLpCylinderPaths.Supported period V K hK)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period K hK) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period K hK) ((EulerLpCylinderCoefficients.constructedEvolution period K hK T hT B).weightedSolution g hg f a₀))

The locally constructed family proves genuine smoothness of the entire mixed translation orbit of the actual solution.