The source Gram generator on the genuine cylinder L²

The generator below is constructed from the actual frame and its first time-derivative field by bounded-field Gram inversion. Its translated coefficient bounds are derived from the frame jets. The forward solution has the localized H3 bound and the true fixed-Hq mixed external-word estimate at the same input/output radius.

@[instance_reducible]

noncomputable def EulerSourceCylinderForward.instSourceCylinderForward1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (U →L[ℝ] U)

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

Equations

• EulerSourceCylinderForward.instSourceCylinderForward1 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceCylinderForward.instSourceCylinderForward2 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

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

Equations

• EulerSourceCylinderForward.instSourceCylinderForward2 = inferInstance

noncomputable def EulerSourceCylinderForward.evolution (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath period S hS T (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ))

Actual homogeneous evolution from the source Gram generator.

Equations

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

theorem EulerSourceCylinderForward.source_coefficient_contDiff {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ))

The source coefficient automatically has the translated regularity needed by the solver.

theorem EulerSourceCylinderForward.source_forward_block_bound (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (Ω K : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hK : MeasurableSet K) (hKc : IsCompact K) (hΩo : IsOpen Ω) (hsub : K ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (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), ↥(EulerLpCylinderPaths.Supported period U K hK))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U 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 Rc C₀ C₁ Ri R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hD : 0 ≤ D) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q T C A D (18 * Ri * C₀ * C₁) (4 * Ri) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) + 1) ≤ R) (hH3 : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath T hT (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath T hT (EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ)).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) ((evolution period T hT Q Q₁ c hc hQ K hK).weightedSolution g hg f a₀))) n 0 ≤ EulerGevrey.majorant R (d + 1) n

Mixed spatial-angular external words, including a fixed Sobolev base, obey the same radius for the actual constructed source solution.