Angle-independent coefficients acting on the genuine cylinder L²

Spatial coefficient fields act on R³×AddCircle by pointwise multiplication. The mixed translation covariance is an equality of actual L² operators. The homogeneous evolution is constructed from the spatial coefficient's Banach-algebra fundamental fields. Its H3 bound is used only on spatial support; no angular regularity or global extension of H3 is assumed.

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients1 {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

• EulerLpCylinderCoefficients.instLpCylinderCoefficients1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients2 {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

• EulerLpCylinderCoefficients.instLpCylinderCoefficients2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients3 (period : ℝ) {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedRing (BoundedContinuousFunction (EulerLiftedGradientSpace.LiftDomain period) (V →L[ℝ] V))

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderCoefficients3 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients4 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period V S hS)

Cache the standard NormedAddCommGroup (Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderCoefficients.instLpCylinderCoefficients4 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients5 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : InnerProductSpace ℝ ↥(EulerLpCylinderPaths.Supported period V S hS)

Cache the standard InnerProductSpace ℝ (Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderCoefficients.instLpCylinderCoefficients5 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients6 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup (↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

Cache the standard NormedAddCommGroup (Supported period V S hS →L[ℝ] Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderCoefficients.instLpCylinderCoefficients6 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients7 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ (↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

Cache the standard NormedSpace ℝ (Supported period V S hS →L[ℝ] Supported period V S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderCoefficients.instLpCylinderCoefficients7 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderCoefficients8 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedRing (↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderCoefficients8 period S hS = inferInstance

noncomputable def EulerLpCylinderCoefficients.liftedOperator (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (A : BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V)) : ↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS)

The actual cylinder operator of a spatial coefficient.

Equations

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

theorem EulerLpCylinderCoefficients.operator_intertwines (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (a : EulerLiftedGradientSpace.LiftTangent) (ha : EulerLpSupportedTranslation.shiftedSet a.1 S ⊆ Ω) (A : BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V)) (u : ↥(EulerLpCylinderPaths.Supported period V S hS)) : (liftedOperator period Ω hΩ (EulerMeanCoefficients.translated A a.1)) ((EulerLpCylinderTranslation.intoLarger period a S Ω hS hΩ ha) u) = (EulerLpCylinderTranslation.intoLarger period a S Ω hS hΩ ha) ((liftedOperator period S hS A) u)

Mixed translation intertwines the actual spatial multiplication operators.

noncomputable def EulerLpCylinderCoefficients.liftedOperatorPath (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (A : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

The entire coefficient time path, acting on the supported cylinder.

Equations

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

theorem EulerLpCylinderCoefficients.liftedOperatorPath_norm (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (A : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) : ‖liftedOperatorPath period S hS T A‖ ≤ ‖A‖

Pointwise operator lifting does not enlarge the uniform coefficient norm.

noncomputable def EulerLpCylinderCoefficients.liftedOperatorPathLinear (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V)) →ₗ[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

The literal linear map underlying coefficient-path lifting.

Equations

• EulerLpCylinderCoefficients.liftedOperatorPathLinear period S hS T = { toFun := EulerLpCylinderCoefficients.liftedOperatorPath period S hS T, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerLpCylinderCoefficients.liftedOperatorPathMap (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V)) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

Lifting spatial coefficient paths to actual cylinder operators is a linear contraction.

Equations

• EulerLpCylinderCoefficients.liftedOperatorPathMap period S hS T = (EulerLpCylinderCoefficients.liftedOperatorPathLinear period S hS T).mkContinuous 1 ⋯

@[simp]

theorem EulerLpCylinderCoefficients.liftedOperatorPathMap_apply (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (A : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) : (liftedOperatorPathMap period S hS T) A = liftedOperatorPath period S hS T A

theorem EulerLpCylinderCoefficients.liftedOperatorPathMap_norm (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) : ‖liftedOperatorPathMap period S hS T‖ ≤ 1

No coefficient amplitude is lost in the actual L² lifting.

theorem EulerLpCylinderCoefficients.mixedOperator_contDiff (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (B : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (V →L[ℝ] V)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => liftedOperatorPath period S hS T (EulerMeanCoefficients.translateCoefficientPath B.field a.1)

The actual cylinder coefficient varies smoothly with all four covering parameters.

theorem EulerLpCylinderCoefficients.mixedOperator_bound (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (B : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (V →L[ℝ] V)) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(B.field t)) x‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => liftedOperatorPath period S hS T (EulerMeanCoefficients.translateCoefficientPath B.field b.1)) a‖ ≤ C

Mixed coefficient jets obey the original spatial tensor bound, with constant one.

noncomputable def EulerLpCylinderCoefficients.constructedEvolution (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) : EulerLinearDuhamel.Evolution T hT (liftedOperatorPath period S hS T B)

The cylinder evolution is constructed from the genuine spatial fundamental fields.

Equations

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

theorem EulerLpCylinderCoefficients.constructedEvolution_propagator_norm (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (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 ∈ S, ‖((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) : ‖(constructedEvolution period S hS T hT B).propagator t s‖ ≤ C * g t / g s

The cylinder propagator retains the exact relative H3 profile on spatial support.