Actual mixed spatial/angular translations on the cylinder

The parameter is the real covering space R³×R. Its action on ordinary L²(R³×AddCircle) is the genuine measure-preserving translation, for arbitrary Hilbert-valued fields. A spatial support condition is preserved under the same qualitative margin as before; angular translation costs no margin.

Actual spatial translations between supported L² spaces

Translation is the genuine measure-preserving action on ordinary R³ L². A compact support inside an open set has a translation neighborhood in which the translated data lie in one fixed larger supported space. This margin is qualitative and does not occur in any operator-norm constant.

def EulerLpSupportedTranslation.shiftedSet (a : EulerSmoothLimit.Space) (S : Set EulerSmoothLimit.Space) : Set EulerSmoothLimit.Space

The exact support set of a translated field.

Equations

• EulerLpSupportedTranslation.shiftedSet a S = {x : EulerSmoothLimit.Space | x + a ∈ S}

theorem EulerLpSupportedTranslation.shiftedSet_measurable (a : EulerSmoothLimit.Space) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : MeasurableSet (shiftedSet a S)

Translated supports remain measurable.

theorem EulerLpSupportedTranslation.translation_mem {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerSmoothLimit.Space) (S Ω : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hΩ : MeasurableSet Ω) (hsub : shiftedSet a S ⊆ Ω) (u : ↥(EulerLpSupportedSubspace.supportedSpace MeasureTheory.volume S hS)) : (EulerLpTranslation.translation a) ↑u ∈ EulerLpSupportedSubspace.supportedSpace MeasureTheory.volume Ω hΩ

Translation carries an actual supported L² field into its translated support set.

noncomputable def EulerLpSupportedTranslation.intoLarger {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerSmoothLimit.Space) (S Ω : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hΩ : MeasurableSet Ω) (hsub : shiftedSet a S ⊆ Ω) : ↥(EulerLpSupportedSubspace.supportedSpace MeasureTheory.volume S hS) →ₗᵢ[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace MeasureTheory.volume Ω hΩ)

Actual isometric translation into a fixed larger supported space.

Equations

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

@[simp]

theorem EulerLpSupportedTranslation.intoLarger_coe {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerSmoothLimit.Space) (S Ω : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hΩ : MeasurableSet Ω) (hsub : shiftedSet a S ⊆ Ω) (u : ↥(EulerLpSupportedSubspace.supportedSpace MeasureTheory.volume S hS)) : ↑((intoLarger a S Ω hS hΩ hsub) u) = (EulerLpTranslation.translation a) ↑u

noncomputable def EulerLpSupportedTranslation.translatedField {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A : EulerLpSupportedMultiplier.Field) (a : EulerSmoothLimit.Space) : EulerLpSupportedMultiplier.Field

The translated coefficient is the literal original field at x+a.

Equations

• EulerLpSupportedTranslation.translatedField A a = EulerMeanCoefficients.translated A a

theorem EulerLpSupportedTranslation.operator_intertwines {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerSmoothLimit.Space) (S Ω : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hΩ : MeasurableSet Ω) (hsub : shiftedSet a S ⊆ Ω) (A : EulerLpSupportedMultiplier.Field) (u : ↥(EulerLpSupportedSubspace.supportedSpace MeasureTheory.volume S hS)) : (EulerLpSupportedMultiplier.operator MeasureTheory.volume Ω hΩ (translatedField A a)) ((intoLarger a S Ω hS hΩ hsub) u) = (intoLarger a S Ω hS hΩ hsub) ((EulerLpSupportedMultiplier.operator MeasureTheory.volume S hS A) u)

Actual coefficient multiplication intertwines the support-changing translation.

theorem EulerLpSupportedTranslation.compact_support_translation_margin (K Ω : Set EulerSmoothLimit.Space) (hK : IsCompact K) (hΩ : IsOpen Ω) (hsub : K ⊆ Ω) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (a : EulerSmoothLimit.Space), ‖a‖ < δ → shiftedSet a K ⊆ Ω

Compactly supported data have a qualitative translation neighborhood inside any prescribed larger open support region.

@[reducible, inline]

noncomputable abbrev EulerLpCylinderTranslation.CylinderL2 (period : ℝ) [Fact (0 < period)] (V : Type u_1) [NormedAddCommGroup V] : AddSubgroup (EulerLiftedGradientSpace.LiftDomain period →ₘ[EulerLiftedGradientSpace.liftMeasure period] V)

Cylinder L²: an abbreviation for Lp V 2 (liftMeasure period).

Equations

• EulerLpCylinderTranslation.CylinderL2 period V = MeasureTheory.Lp V 2 (EulerLiftedGradientSpace.liftMeasure period)

noncomputable def EulerLpCylinderTranslation.translate (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : EulerLiftedGradientSpace.LiftTangent) : ↥(CylinderL2 period V) →ₗᵢ[ℝ] ↥(CylinderL2 period V)

Actual translation by a real covering-space parameter.

Equations

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

theorem EulerLpCylinderTranslation.translate_ae (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : EulerLiftedGradientSpace.LiftTangent) (u : ↥(CylinderL2 period V)) : ↑↑((translate period a) u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => ↑↑u (x + EulerLiftedGradientSpace.coveringMap period a)

@[simp]

theorem EulerLpCylinderTranslation.translate_zero (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(CylinderL2 period V)) : (translate period 0) u = u

theorem EulerLpCylinderTranslation.coveringMap_add (period : ℝ) (a b : EulerLiftedGradientSpace.LiftTangent) : EulerLiftedGradientSpace.coveringMap period (a + b) = EulerLiftedGradientSpace.coveringMap period a + EulerLiftedGradientSpace.coveringMap period b

theorem EulerLpCylinderTranslation.translate_add (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (a b : EulerLiftedGradientSpace.LiftTangent) (u : ↥(CylinderL2 period V)) : (translate period a) ((translate period b) u) = (translate period (a + b)) u

theorem EulerLpCylinderTranslation.translate_continuous (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(CylinderL2 period V)) : Continuous fun (a : EulerLiftedGradientSpace.LiftTangent) => (translate period a) u

This is an actual strongly continuous action on the full cylinder L².

noncomputable def EulerLpCylinderTranslation.pathTranslate (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] (a : EulerLiftedGradientSpace.LiftTangent) : C(K, ↥(CylinderL2 period V)) →L[ℝ] C(K, ↥(CylinderL2 period V))

The same mixed translation on actual continuous time paths.

Equations

• EulerLpCylinderTranslation.pathTranslate period a = ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpCylinderTranslation.translate period a).toContinuousLinearMap

@[simp]

theorem EulerLpCylinderTranslation.pathTranslate_apply (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] (a : EulerLiftedGradientSpace.LiftTangent) (u : C(K, ↥(CylinderL2 period V))) (t : K) : ((pathTranslate period a) u) t = (translate period a) (u t)

theorem EulerLpCylinderTranslation.pathTranslate_norm (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (a : EulerLiftedGradientSpace.LiftTangent) : ‖pathTranslate period a‖ ≤ 1

noncomputable def EulerLpCylinderTranslation.fieldLift (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] : BoundedContinuousFunction EulerSmoothLimit.Space W →L[ℝ] BoundedContinuousFunction (EulerLiftedGradientSpace.LiftDomain period) W

An angle-independent coefficient on the actual cylinder.

Equations

• EulerLpCylinderTranslation.fieldLift period = BoundedContinuousFunction.compContinuousCLM W ℝ { toFun := Prod.fst, continuous_toFun := ⋯ }

@[simp]

theorem EulerLpCylinderTranslation.fieldLift_apply (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (A : BoundedContinuousFunction EulerSmoothLimit.Space W) (x : EulerLiftedGradientSpace.LiftDomain period) : ((fieldLift period) A) x = A x.1

theorem EulerLpCylinderTranslation.fieldLift_norm (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] : ‖fieldLift period‖ ≤ 1

noncomputable def EulerLpCylinderTranslation.fieldPathLift (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {K : Type u_2} [TopologicalSpace K] : C(K, BoundedContinuousFunction EulerSmoothLimit.Space W) →L[ℝ] C(K, BoundedContinuousFunction (EulerLiftedGradientSpace.LiftDomain period) W)

The bounded linear lift of an entire coefficient time path.

Equations

• EulerLpCylinderTranslation.fieldPathLift period = ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpCylinderTranslation.fieldLift period)

@[simp]

theorem EulerLpCylinderTranslation.fieldPathLift_apply (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {K : Type u_2} [TopologicalSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space W)) (t : K) (x : EulerLiftedGradientSpace.LiftDomain period) : (((fieldPathLift period) A) t) x = (A t) x.1

theorem EulerLpCylinderTranslation.fieldPathLift_norm (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {K : Type u_2} [TopologicalSpace K] [CompactSpace K] : ‖fieldPathLift period‖ ≤ 1

def EulerLpCylinderTranslation.spatialSet (period : ℝ) (S : Set EulerSmoothLimit.Space) : Set (EulerLiftedGradientSpace.LiftDomain period)

Support in a set of spatial labels, with arbitrary angular coordinate.

Equations

• EulerLpCylinderTranslation.spatialSet period S = Prod.fst ⁻¹' S

theorem EulerLpCylinderTranslation.spatialSet_measurable (period : ℝ) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : MeasurableSet (spatialSet period S)

theorem EulerLpCylinderTranslation.translate_mem (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerLiftedGradientSpace.LiftTangent) (S Ω : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hΩ : MeasurableSet Ω) (hsub : EulerLpSupportedTranslation.shiftedSet a.1 S ⊆ Ω) (u : ↥(EulerLpSupportedSubspace.supportedSpace (EulerLiftedGradientSpace.liftMeasure period) (spatialSet period S) ⋯)) : (translate period a) ↑u ∈ EulerLpSupportedSubspace.supportedSpace (EulerLiftedGradientSpace.liftMeasure period) (spatialSet period Ω) ⋯

The mixed translated field lies in the spatially enlarged supporting set.

noncomputable def EulerLpCylinderTranslation.intoLarger (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (a : EulerLiftedGradientSpace.LiftTangent) (S Ω : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hΩ : MeasurableSet Ω) (hsub : EulerLpSupportedTranslation.shiftedSet a.1 S ⊆ Ω) : ↥(EulerLpSupportedSubspace.supportedSpace (EulerLiftedGradientSpace.liftMeasure period) (spatialSet period S) ⋯) →ₗᵢ[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace (EulerLiftedGradientSpace.liftMeasure period) (spatialSet period Ω) ⋯)

Actual isometric mixed translation into a fixed spatial support region.

Equations

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

theorem EulerLpCylinderTranslation.compact_support_mixed_margin (S Ω : Set EulerSmoothLimit.Space) (hS : IsCompact S) (hΩ : IsOpen Ω) (hsub : S ⊆ Ω) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (a : EulerLiftedGradientSpace.LiftTangent), ‖a‖ < δ → EulerLpSupportedTranslation.shiftedSet a.1 S ⊆ Ω

Angular displacement costs no support margin; the spatial margin is purely qualitative.