The real periodic lift of a genuine cylinder H3 field is bounded and continuous. This construction uses the cylinder norm, never an L² norm on the full real covering space.

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover1 (P : ℝ) [Fact (0 < P)] : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)

Cache the standard NormedAddCommGroup (SobolevSpace P 3) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover2 (P : ℝ) [Fact (0 < P)] : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)

Cache the standard NormedSpace ℝ (SobolevSpace P 3) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover3 : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover3 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover4 : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover4 = inferInstance

noncomputable def EulerCylinderBoundedCover.cover (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) : BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space

Cover, constructed using BoundedContinuousFunction.ofNormedAddCommGroup.

Equations

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

@[simp]

theorem EulerCylinderBoundedCover.cover_apply (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (x : EulerLiftedGradientSpace.LiftTangent) : (cover P u) x = (EulerSobolevPointEvaluation.pointEvaluation P (EulerLiftedGradientSpace.coveringMap P x)) u

theorem EulerCylinderBoundedCover.cover_norm_le (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) : ‖cover P u‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * ‖u‖

noncomputable def EulerCylinderBoundedCover.coverLinear (P : ℝ) [Fact (0 < P)] : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3) →ₗ[ℝ] BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space

Cover linear, bundling toFun, map_add, map_smul.

Equations

• EulerCylinderBoundedCover.coverLinear P = { toFun := EulerCylinderBoundedCover.cover P, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerCylinderBoundedCover.coverMap (P : ℝ) [Fact (0 < P)] : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3) →L[ℝ] BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space

Cover map, bundling toLinearMap, cont.

Equations

• EulerCylinderBoundedCover.coverMap P = { toLinearMap := EulerCylinderBoundedCover.coverLinear P, cont := ⋯ }

theorem EulerCylinderBoundedCover.coverMap_norm_le (P : ℝ) [Fact (0 < P)] : ‖coverMap P‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover5 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 3))

Cache the standard NormedAddCommGroup C(K, SobolevSpace P 3) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover5 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover6 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 3))

Cache the standard NormedSpace ℝ C(K, SobolevSpace P 3) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover6 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover7 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup C(K, LiftTangent →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover7 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderBoundedCover.instCylinderBoundedCover8 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ C(K, LiftTangent →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• EulerCylinderBoundedCover.instCylinderBoundedCover8 = inferInstance

noncomputable def EulerCylinderBoundedCover.coverPathMap (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) →L[ℝ] C(K, BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Cover path map, given by (coverMap P).compLeftContinuous ℝ K.

Equations

• EulerCylinderBoundedCover.coverPathMap P = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderBoundedCover.coverMap P)

theorem EulerCylinderBoundedCover.coverPathMap_norm_le (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : ‖coverPathMap P‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3

noncomputable def EulerCylinderBoundedCover.coverPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : C(K, BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Cover path, given by coverPathMap P (sobolevPath P 3 p hp).

Equations

• EulerCylinderBoundedCover.coverPath P p hp = (EulerCylinderBoundedCover.coverPathMap P) (EulerCylinderSmoothOrbit.sobolevPath P 3 p hp)

@[simp]

theorem EulerCylinderBoundedCover.coverPath_apply (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) (x : EulerLiftedGradientSpace.LiftTangent) : ((coverPath P p hp) t) x = EulerCylinderSmoothOrbit.pointField P p hp t (EulerLiftedGradientSpace.coveringMap P x)

noncomputable def EulerCylinderBoundedCover.coverOrbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (a : EulerLiftedGradientSpace.LiftTangent) : C(K, BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Cover orbit, given by coverPathMap P (sobolevOrbit P 3 p hp a).

Equations

• EulerCylinderBoundedCover.coverOrbit P p hp a = (EulerCylinderBoundedCover.coverPathMap P) (EulerCylinderSmoothOrbit.sobolevOrbit P 3 p hp a)

theorem EulerCylinderBoundedCover.coverOrbit_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ (↑⊤) (coverOrbit P p hp)

theorem EulerCylinderBoundedCover.coverOrbit_apply (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (a : EulerLiftedGradientSpace.LiftTangent) (t : K) (x : EulerLiftedGradientSpace.LiftTangent) : ((coverOrbit P p hp a) t) x = ((coverPath P p hp) t) (x + a)

@[simp]

theorem EulerCylinderBoundedCover.coverOrbit_zero (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : coverOrbit P p hp 0 = coverPath P p hp