The genuine constant-angle embedding of ordinary spatial L² into cylinder L².

@[reducible, inline]

noncomputable abbrev EulerCylinderSpatialEmbedding.SpatialL2 (V : Type u_1) [NormedAddCommGroup V] : AddSubgroup (EulerSmoothLimit.Space →ₘ[MeasureTheory.volume] V)

Spatial L²: an abbreviation for Lp V 2 (volume : Measure Space).

Equations

• EulerCylinderSpatialEmbedding.SpatialL2 V = MeasureTheory.Lp V 2 MeasureTheory.volume

theorem EulerCylinderSpatialEmbedding.lifted_memLp (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] (u : ↥(SpatialL2 V)) : MeasureTheory.MemLp (fun (z : EulerLiftedGradientSpace.LiftDomain P) => ↑↑u z.1) 2 (EulerLiftedGradientSpace.liftMeasure P)

noncomputable def EulerCylinderSpatialEmbedding.lift (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] (u : ↥(SpatialL2 V)) : ↥(EulerLpCylinderTranslation.CylinderL2 P V)

Lift, given by (lifted_memLp P u).toLp (fun z : LiftDomain P => u z.1).

Equations

• EulerCylinderSpatialEmbedding.lift P u = MeasureTheory.MemLp.toLp (fun (z : EulerLiftedGradientSpace.LiftDomain P) => ↑↑u z.1) ⋯

theorem EulerCylinderSpatialEmbedding.lift_ae (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] (u : ↥(SpatialL2 V)) : ↑↑(lift P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (z : EulerLiftedGradientSpace.LiftDomain P) => ↑↑u z.1

theorem EulerCylinderSpatialEmbedding.lift_add (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] (u v : ↥(SpatialL2 V)) : lift P (u + v) = lift P u + lift P v

theorem EulerCylinderSpatialEmbedding.lift_smul (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (r : ℝ) (u : ↥(SpatialL2 V)) : lift P (r • u) = r • lift P u

theorem EulerCylinderSpatialEmbedding.lift_norm_sq (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] (u : ↥(SpatialL2 V)) : ‖lift P u‖ ^ 2 = P * ‖u‖ ^ 2

The angle factor in the true product-space L² norm is exactly the period.

theorem EulerCylinderSpatialEmbedding.lift_norm_le (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] (u : ↥(SpatialL2 V)) : ‖lift P u‖ ≤ √P * ‖u‖

noncomputable def EulerCylinderSpatialEmbedding.embeddingLinear (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : ↥(SpatialL2 V) →ₗ[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V)

Embedding linear, bundling toFun, map_add, map_smul.

Equations

• EulerCylinderSpatialEmbedding.embeddingLinear P = { toFun := EulerCylinderSpatialEmbedding.lift P, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerCylinderSpatialEmbedding.embedding (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : ↥(SpatialL2 V) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V)

Embedding, given by (embeddingLinear P).mkContinuous (Real.sqrt P) (lift_norm_le P).

Equations

• EulerCylinderSpatialEmbedding.embedding P = (EulerCylinderSpatialEmbedding.embeddingLinear P).mkContinuous √P ⋯

@[simp]

theorem EulerCylinderSpatialEmbedding.embedding_apply (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(SpatialL2 V)) : (embedding P) u = lift P u

theorem EulerCylinderSpatialEmbedding.embedding_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : ‖embedding P‖ ≤ √P

theorem EulerCylinderSpatialEmbedding.embedding_inner (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (u v : ↥(SpatialL2 V)) : inner ℝ ((embedding P) u) ((embedding P) v) = P * inner ℝ u v