Measure-preserving Euclidean coordinates and the actual L² bridge to the cylinder.

noncomputable def EulerCylinderCoordinates.coordinateLinearEquiv : EulerSobolev.Domain 4 ≃ₗ[ℝ] EulerLiftedGradientSpace.LiftTangent

Euclidean coordinate zero is the angle; coordinates one through three are spatial.

Equations

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

noncomputable def EulerCylinderCoordinates.coordinateEquiv : EulerSobolev.Domain 4 ≃L[ℝ] EulerLiftedGradientSpace.LiftTangent

The coordinate isomorphism, continuous in both directions.

Equations

• EulerCylinderCoordinates.coordinateEquiv = EulerCylinderCoordinates.coordinateLinearEquiv.toContinuousLinearEquiv

@[simp]

theorem EulerCylinderCoordinates.coordinateEquiv_apply (z : EulerSobolev.Domain 4) : coordinateEquiv z = (WithLp.toLp 2 fun (i : Fin 3) => z.ofLp i.succ, z.ofLp 0)

@[simp]

theorem EulerCylinderCoordinates.coordinateEquiv_symm_apply (p : EulerLiftedGradientSpace.LiftTangent) : coordinateEquiv.symm p = WithLp.toLp 2 (Fin.cons p.2 fun (i : Fin 3) => p.1.ofLp i)

theorem EulerCylinderCoordinates.coordinateEquiv_measurePreserving : MeasureTheory.MeasurePreserving (⇑coordinateEquiv) MeasureTheory.volume (MeasureTheory.volume.prod MeasureTheory.volume)

The coordinate change preserves the genuine product Lebesgue measure exactly.

noncomputable def EulerCylinderCoordinates.fundamentalMeasure (period a : ℝ) : MeasureTheory.Measure EulerLiftedGradientSpace.LiftTangent

A fundamental strip in the real covering space.

Equations

• EulerCylinderCoordinates.fundamentalMeasure period a = MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a (a + period)))

theorem EulerCylinderCoordinates.covering_fundamental_measurePreserving (period : ℝ) [Fact (0 < period)] (a : ℝ) : MeasureTheory.MeasurePreserving (EulerLiftedGradientSpace.coveringMap period) (fundamentalMeasure period a) (EulerLiftedGradientSpace.liftMeasure period)

Covering coordinates restricted to one period preserve the cylinder's measure.

noncomputable def EulerCylinderCoordinates.euclideanCover (period : ℝ) : EulerSobolev.Domain 4 → EulerLiftedGradientSpace.LiftDomain period

Euclidean coordinates for the actual quotient covering map.

Equations

• EulerCylinderCoordinates.euclideanCover period = EulerLiftedGradientSpace.coveringMap period ∘ ⇑EulerCylinderCoordinates.coordinateEquiv

noncomputable def EulerCylinderCoordinates.stripMeasure (period a : ℝ) : MeasureTheory.Measure (EulerSobolev.Domain 4)

Euclidean measure restricted to one fundamental angular strip.

Equations

• EulerCylinderCoordinates.stripMeasure period a = MeasureTheory.volume.restrict {z : EulerSobolev.Domain 4 | z.ofLp 0 ∈ Set.Ioc a (a + period)}

theorem EulerCylinderCoordinates.coordinateEquiv_fundamental_measurePreserving (period a : ℝ) : MeasureTheory.MeasurePreserving (⇑coordinateEquiv) (stripMeasure period a) (fundamentalMeasure period a)

theorem EulerCylinderCoordinates.euclideanCover_fundamental_measurePreserving (period : ℝ) [Fact (0 < period)] (a : ℝ) : MeasureTheory.MeasurePreserving (euclideanCover period) (stripMeasure period a) (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerCylinderCoordinates.eLpNorm_cover (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.AEStronglyMeasurable f (EulerLiftedGradientSpace.liftMeasure period)) (a : ℝ) (p : ENNReal) : MeasureTheory.eLpNorm (f ∘ euclideanCover period) p (stripMeasure period a) = MeasureTheory.eLpNorm f p (EulerLiftedGradientSpace.liftMeasure period)

The fundamental-strip Lᵖ seminorm is exactly the Lᵖ seminorm on the cylinder.

theorem EulerCylinderCoordinates.memLp_cover (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) (a : ℝ) : MeasureTheory.MemLp (f ∘ euclideanCover period) 2 (stripMeasure period a)

Square integrability of actual fields transfers to their Euclidean periodic lifts.

noncomputable def EulerCylinderCoordinates.chartMeasure (period : ℝ) : MeasureTheory.Measure (EulerSobolev.Domain 4)

Six consecutive fundamental strips, retaining the actual Euclidean measures.

Equations

• EulerCylinderCoordinates.chartMeasure period = MeasureTheory.Measure.sum fun (i : Fin 6) => EulerCylinderCoordinates.stripMeasure period ((↑↑i - 3) * period)

theorem EulerCylinderCoordinates.chartSupport_cover (period : ℝ) [Fact (0 < period)] : {z : EulerSobolev.Domain 4 | |z.ofLp 0| ≤ 2 * period} ⊆ ⋃ (i : Fin 6), {z : EulerSobolev.Domain 4 | z.ofLp 0 ∈ Set.Ioc ((↑↑i - 3) * period) ((↑↑i - 3) * period + period)}

theorem EulerCylinderCoordinates.chartSupport_measure_le (period : ℝ) [Fact (0 < period)] : MeasureTheory.volume.restrict {z : EulerSobolev.Domain 4 | |z.ofLp 0| ≤ 2 * period} ≤ chartMeasure period

theorem EulerCylinderCoordinates.euclideanCover_chart_measurePreserving (period : ℝ) [Fact (0 < period)] : MeasureTheory.MeasurePreserving (euclideanCover period) (chartMeasure period) (6 • EulerLiftedGradientSpace.liftMeasure period)

The finite chart cover has exactly six times the cylinder measure.

theorem EulerCylinderCoordinates.eLpNorm_cover_chart (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.AEStronglyMeasurable f (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.eLpNorm (f ∘ euclideanCover period) 2 (chartMeasure period) = 6 ^ (1 / 2) * MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerCylinderCoordinates.eLpNorm_localized_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.AEStronglyMeasurable f (EulerLiftedGradientSpace.liftMeasure period)) (g : EulerSobolev.Domain 4 → G) (hsupp : Function.support g ⊆ {z : EulerSobolev.Domain 4 | |z.ofLp 0| ≤ 2 * period}) (B : NNReal) (hb : ∀ (z : EulerSobolev.Domain 4), ‖g z‖ ≤ ↑B * ‖f (euclideanCover period z)‖) : MeasureTheory.eLpNorm g 2 MeasureTheory.volume ≤ ↑B * 6 ^ (1 / 2) * MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period)

A localized lift is controlled by the genuine cylinder norm, with explicit chart multiplicity.

theorem EulerCylinderCoordinates.localized_L2_le (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) (g : SchwartzMap (EulerSobolev.Domain 4) ℂ) (hsupp : Function.support ⇑g ⊆ {z : EulerSobolev.Domain 4 | |z.ofLp 0| ≤ 2 * period}) (B : NNReal) (hb : ∀ (z : EulerSobolev.Domain 4), ‖g z‖ ≤ ↑B * ‖f (euclideanCover period z)‖) : ‖g.toLp 2 MeasureTheory.volume‖ ≤ ↑B * 6 ^ (1 / 2) * ‖MeasureTheory.MemLp.toLp f hf‖

The localized-lift estimate as an inequality between ordinary real L² norms.