The complete physical forward bound at one mixed-word radius

Physical forcing is projected by the actual Gram left inverse, the supported coordinate equation is solved by the constructed evolution, and the result is multiplied by the physical frame. All three operations use the same external radius R. Only the solve spends one shift.

@[instance_reducible]

noncomputable def EulerSourceCylinderForwardSobolev.instSourceCylinderForwardSobolev1 {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

• EulerSourceCylinderForwardSobolev.instSourceCylinderForwardSobolev1 = inferInstance

@[instance_reducible]

noncomputable def EulerSourceCylinderForwardSobolev.instSourceCylinderForwardSobolev2 {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

• EulerSourceCylinderForwardSobolev.instSourceCylinderForwardSobolev2 = inferInstance

noncomputable def EulerSourceCylinderForwardSobolev.normalizedCoordinates (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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (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) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period U S hS))

Actual profile-normalized coordinates with physical forcing as input.

Equations

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

noncomputable def EulerSourceCylinderForwardSobolev.normalizedVelocity (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) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (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) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))

The corresponding actual profile-normalized physical velocity.

Equations

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

def EulerSourceCylinderForwardSobolev.forcingCost (ι : Type u_4) [Fintype ι] (q : ℕ) (Ri C₀ : ℝ) : ℝ

Explicit coefficient cost of projecting a physical forcing at the fixed base order.

Equations

• EulerSourceCylinderForwardSobolev.forcingCost ι q Ri C₀ = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q (4 * Ri) (3 * Ri * C₀)

theorem EulerSourceCylinderForwardSobolev.physical_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 ι] (T : ℝ) (hT : 0 ≤ T) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (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) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hSc : IsCompact S) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hg₀ : g ⟨0, ⋯⟩ = 1) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) 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) (hRforcing : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hRframe : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hR : 2 * EulerLinearDuhamel.forwardSobolevCost ι q T C A (forcingCost ι q Ri C₀ * 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 S hS) 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 S hS) (normalizedVelocity period T hT S hS Q Q₁ c hc hQ g hg f a₀))) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₀ * EulerGevrey.majorant R (d + 1) n

The physical solution has the source's genuine fixed-Hq mixed-word bound, without changing the input external radius.