The genuine scalar angular primitive on cylinder L²

A fixed unit scalar embedding and its norm-one projection transfer the constructed vector primitive to scalar pressure. Its mixed-translation commutation and fixed-Hq external-word bound have no radius loss.

noncomputable def EulerCylinderScalarPrimitive.unitVector : EulerSmoothLimit.Space

Unit vector, given by EuclideanSpace.single 0 1.

Equations

• EulerCylinderScalarPrimitive.unitVector = EuclideanSpace.single 0 1

theorem EulerCylinderScalarPrimitive.unitVector_norm : ‖unitVector‖ = 1

noncomputable def EulerCylinderScalarPrimitive.scalarEmbed : ℝ →L[ℝ] EulerSmoothLimit.Space

Scalar embed, given by toSpanSingleton ℝ unitVector.

Equations

• EulerCylinderScalarPrimitive.scalarEmbed = ContinuousLinearMap.toSpanSingleton ℝ EulerCylinderScalarPrimitive.unitVector

noncomputable def EulerCylinderScalarPrimitive.scalarProject : EulerSmoothLimit.Space →L[ℝ] ℝ

Scalar project, given by innerSL ℝ unitVector.

Equations

• EulerCylinderScalarPrimitive.scalarProject = (innerSL ℝ) EulerCylinderScalarPrimitive.unitVector

theorem EulerCylinderScalarPrimitive.scalarEmbed_norm : ‖scalarEmbed‖ = 1

theorem EulerCylinderScalarPrimitive.scalarProject_norm : ‖scalarProject‖ = 1

@[simp]

theorem EulerCylinderScalarPrimitive.project_embed (r : ℝ) : scalarProject (scalarEmbed r) = r

noncomputable def EulerCylinderScalarPrimitive.embed (period : ℝ) [Fact (0 < period)] : ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Embed, given by EulerCylinderConstantMap.map period scalarEmbed.

Equations

• EulerCylinderScalarPrimitive.embed period = EulerCylinderConstantMap.map period EulerCylinderScalarPrimitive.scalarEmbed

noncomputable def EulerCylinderScalarPrimitive.project (period : ℝ) [Fact (0 < period)] : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ)

Project, given by EulerCylinderConstantMap.map period scalarProject.

Equations

• EulerCylinderScalarPrimitive.project period = EulerCylinderConstantMap.map period EulerCylinderScalarPrimitive.scalarProject

theorem EulerCylinderScalarPrimitive.embed_norm (period : ℝ) [Fact (0 < period)] : ‖embed period‖ ≤ 1

theorem EulerCylinderScalarPrimitive.project_norm (period : ℝ) [Fact (0 < period)] : ‖project period‖ ≤ 1

noncomputable def EulerCylinderScalarPrimitive.primitive (period : ℝ) [Fact (0 < period)] : ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ)

Primitive, given by (project period).comp ((EulerCylinderAnglePrimitive.primitive period).comp (embed period)).

Equations

• EulerCylinderScalarPrimitive.primitive period = EulerCylinderScalarPrimitive.project period ∘SL EulerCylinderAnglePrimitive.primitive period ∘SL EulerCylinderScalarPrimitive.embed period

theorem EulerCylinderScalarPrimitive.primitive_norm (period : ℝ) [Fact (0 < period)] : ‖primitive period‖ ≤ period

theorem EulerCylinderScalarPrimitive.primitive_translation (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ)) : (primitive period) ((EulerLpCylinderTranslation.translate period a) u) = (EulerLpCylinderTranslation.translate period a) ((primitive period) u)

All mixed translations commute with the actual scalar primitive.

@[instance_reducible]

noncomputable def EulerCylinderScalarPrimitive.instCylinderScalarPrimitive1 (period : ℝ) [Fact (0 < period)] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ)

Cache the standard NormedAddCommGroup (CylinderL2 period ℝ) instance to shorten typeclass synthesis.

Equations

• EulerCylinderScalarPrimitive.instCylinderScalarPrimitive1 period = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderScalarPrimitive.instCylinderScalarPrimitive2 (period : ℝ) [Fact (0 < period)] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ)

Cache the standard NormedSpace ℝ (CylinderL2 period ℝ) instance to shorten typeclass synthesis.

Equations

• EulerCylinderScalarPrimitive.instCylinderScalarPrimitive2 period = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderScalarPrimitive.instCylinderScalarPrimitive3 (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ))

Cache the standard NormedAddCommGroup C(K,CylinderL2 period ℝ) instance to shorten typeclass synthesis.

Equations

• EulerCylinderScalarPrimitive.instCylinderScalarPrimitive3 period = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderScalarPrimitive.instCylinderScalarPrimitive4 (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ))

Cache the standard NormedSpace ℝ C(K,CylinderL2 period ℝ) instance to shorten typeclass synthesis.

Equations

• EulerCylinderScalarPrimitive.instCylinderScalarPrimitive4 period = inferInstance

noncomputable def EulerCylinderScalarPrimitive.pathPrimitive (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ))

Path primitive, given by (primitive period).compLeftContinuous ℝ K.

Equations

• EulerCylinderScalarPrimitive.pathPrimitive period = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderScalarPrimitive.primitive period)

theorem EulerCylinderScalarPrimitive.pathPrimitive_norm (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : ‖pathPrimitive period‖ ≤ period

theorem EulerCylinderScalarPrimitive.pathPrimitive_translation (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] (a : EulerLiftedGradientSpace.LiftTangent) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ))) : (pathPrimitive period) ((EulerLpCylinderTranslation.pathTranslate period a) u) = (EulerLpCylinderTranslation.pathTranslate period a) ((pathPrimitive period) u)

theorem EulerCylinderScalarPrimitive.pathPrimitive_orbit_contDiff (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) u) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((pathPrimitive period) u)

theorem EulerCylinderScalarPrimitive.pathPrimitive_block_le (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period ℝ))) (hu : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) u) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period b) ((pathPrimitive period) u)) n a ≤ period * EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period b) u) n a