Actual source forcing and physical velocity on cylinder L²

The projected forcing uses the constructed Gram left inverse. The physical velocity uses the actual frame. Both preserve the closed spatial support, actual mixed-orbit smoothness, and the external-word radius at fixed Hq.

noncomputable def EulerSourceCylinderForcing.projectedForcing (period : ℝ) [Fact (0 < period)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))) : C(K, ↥(EulerLpCylinderPaths.Supported period U S hS))

The actual projected forcing on the supported cylinder.

Equations

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

noncomputable def EulerSourceCylinderForcing.physicalVelocity (period : ℝ) [Fact (0 < period)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (u : C(K, ↥(EulerLpCylinderPaths.Supported period U S hS))) : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))

The actual physical velocity associated with the coordinate field.

Equations

• EulerSourceCylinderForcing.physicalVelocity period S hS Q u = ((EulerLpCylinderRectangular.supportedMultiplierMap period S hS) Q.field) u

theorem EulerSourceCylinderForcing.projectedForcing_contDiff (period : ℝ) [Fact (0 < period)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (projectedForcing period S hS Q c hc hQ f))

theorem EulerSourceCylinderForcing.physicalVelocity_contDiff (period : ℝ) [Fact (0 < period)] {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (u : C(K, ↥(EulerLpCylinderPaths.Supported period U S hS))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) u)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (physicalVelocity period S hS Q u))

theorem EulerSourceCylinderForcing.projectedForcing_block_bound (period : ℝ) [Fact (0 < period)] {K : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (f : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (Rc C Ri R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (Rc + 1) ≤ Ri) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * Ri) ≤ R) (hbQ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (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) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (projectedForcing period S hS Q c hc hQ f))) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q (4 * Ri) (3 * Ri * C) * D * EulerGevrey.majorant R d n

The source forcing multiplication costs an explicit coefficient polynomial, with no change to the forcing's radius or shift.

theorem EulerSourceCylinderForcing.physicalVelocity_block_bound (period : ℝ) [Fact (0 < period)] {K : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (u : C(K, ↥(EulerLpCylinderPaths.Supported period U S hS))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) u)) (Rc C R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hbQ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(Q.field t)) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbu : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) u)) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (physicalVelocity period S hS Q u))) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C * D * EulerGevrey.majorant R d n

Reconstruction by the physical frame also preserves the same external radius.