Localized H3 gives actual mixed cylinder L² fixed-Hq forward estimates

The coefficient is the literal bounded matrix field, the homogeneous and forced solutions are constructed, and the final derivative block is the actual mixed R³×R translation orbit of the actual solution. A compact support inside an open subset of the H3 ball supplies only a qualitative neighborhood. The radius and polynomial constants do not depend on that support margin.

Local equality preserves genuine fixed-Sobolev external derivative blocks.

Actual ordered derivative sums depend only on the local function germ.

theorem EulerParameterWordGevrey.wordDerivative_eq_of_eventuallyEq {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) {f g : P → E} {x : P} (h : f =ᶠ[nhds x] g) {n : ℕ} (w : Fin n → ι) : wordDerivative directions f w x = wordDerivative directions g w x

Equality on a genuine neighborhood identifies every actual ordered word derivative.

theorem EulerParameterWordGevrey.wordSum_eq_of_eventuallyEq {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) {f g : P → E} {x : P} (h : f =ᶠ[nhds x] g) (n : ℕ) : wordSum directions f n x = wordSum directions g n x

The identical external-word sum transfers across local equality, with no radius factor.

theorem EulerParameterWordGevrey.baseSize_eq_of_eventuallyEq {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) {f g : P → E} {x : P} (h : f =ᶠ[nhds x] g) : baseSize directions q f x = baseSize directions q g x

A fixed finite Sobolev sum depends only on the actual function germ.

theorem EulerParameterWordGevrey.block_eq_of_eventuallyEq {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) {f g : P → E} {x : P} (h : f =ᶠ[nhds x] g) (n : ℕ) : block directions q f n x = block directions q g n x

All inner and external word derivatives agree under equality on a neighborhood.

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev1 {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.instLpCylinderRegularSobolev1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev2 {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.instLpCylinderRegularSobolev2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev3 (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.instLpCylinderRegularSobolev3 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev4 (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.instLpCylinderRegularSobolev4 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev5 (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.instLpCylinderRegularSobolev5 period Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev6 (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.instLpCylinderRegularSobolev6 period Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev7 (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.instLpCylinderRegularSobolev7 period T = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev8 (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.instLpCylinderRegularSobolev8 period T = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev9 (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.instLpCylinderRegularSobolev9 period T Ω hΩ = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRegularForward.instLpCylinderRegularSobolev10 (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.instLpCylinderRegularSobolev10 period T Ω hΩ = inferInstance

theorem EulerLpCylinderRegularForward.solutionFamily_block_bound (period : ℝ) [Fact (0 < period)] {V : Type u_1} {ι : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (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) (hg₀ : g ⟨0, ⋯⟩ = 1) (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₀) (C A D CB Rc R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hD : 0 ≤ D) (hCB : 0 ≤ CB) (hRc : 0 ≤ Rc) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q T C A D CB Rc * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hBb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath B) x‖ ≤ CB * EulerGevrey.majorant Rc 0 n) (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) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) n 0 ≤ D * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) a₀) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (solutionFamily period T hT Ω hΩ B g hg f a₀) n 0 ≤ EulerGevrey.majorant R (d + 1) n

The constructed fixed-space family has a true fixed-Sobolev word bound at the base parameter, with the same radius as the data.

theorem EulerLpCylinderRegularForward.source_forward_block_bound (period : ℝ) [Fact (0 < period)] {V : Type u_1} {ι : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (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) (hg₀ : g ⟨0, ⋯⟩ = 1) (K : Set EulerSmoothLimit.Space) (hK : MeasurableSet K) (hKc : IsCompact K) (hΩo : IsOpen Ω) (hsub : K ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (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₀) (C A D CB Rc R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hD : 0 ≤ D) (hCB : 0 ≤ CB) (hRc : 0 ≤ Rc) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q T C A D CB Rc * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hBb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath B) x‖ ≤ CB * EulerGevrey.majorant Rc 0 n) (hH3 : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath T hT B).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath T hT B).backward s) x‖ ≤ C * g t / g s) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period K hK) f)) n 0 ≤ D * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (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₀))) n 0 ≤ EulerGevrey.majorant R (d + 1) n

The actual cylinder-L² solution has the source's fixed-Hq external-word bound. H3 is used only on its stated ball of radius one half.