Genuine cylinder Sobolev jets and smooth representatives from mixed L² orbits

The parameter orbit is the actual R³×R covering action on cylinder L². Every angular derivative is retained. Its genuine strong derivatives construct the existing Sobolev arrays and a smooth representative; no spatial regularity of the solution is assumed separately.

@[reducible, inline]

abbrev EulerCylinderSmoothOrbit.SmoothOrbit (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) : Prop

Smoothness of the actual full mixed L² translation orbit.

Equations

• EulerCylinderSmoothOrbit.SmoothOrbit period u = ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u

noncomputable def EulerCylinderSmoothOrbit.orbitDerivative (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (v : EulerLiftedGradientSpace.LiftTangent) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual L² derivative in a covering-space direction.

Equations

• EulerCylinderSmoothOrbit.orbitDerivative period u v = (fderiv ℝ (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) 0) v

theorem EulerCylinderSmoothOrbit.orbitDerivative_translation (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (v a : EulerLiftedGradientSpace.LiftTangent) : (EulerLpCylinderTranslation.translate period a) (orbitDerivative period u v) = (fderiv ℝ (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) u) a) v

An actual orbit derivative transforms by actual cylinder translation.

theorem EulerCylinderSmoothOrbit.orbitDerivative_smooth (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (v : EulerLiftedGradientSpace.LiftTangent) : SmoothOrbit period (orbitDerivative period u v)

theorem EulerCylinderSmoothOrbit.orbitDerivative_hasDerivAt (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (v : EulerLiftedGradientSpace.LiftTangent) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period v t)) u) (orbitDerivative period u v) 0

These derivatives are exactly the existing strong cylinder directional derivatives.

def EulerCylinderSmoothOrbit.spatialJet (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q u

Every finite tree of genuine mixed strong derivatives is constructed.

Equations

• One or more equations did not get rendered due to their size.
• EulerCylinderSmoothOrbit.spatialJet period 0 u hu = EulerSpatialSobolevInverse.SpatialJet.zero u

theorem EulerCylinderSmoothOrbit.spatialJet_norm (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : (spatialJet period q u hu).sobolevNorm = EulerParameterWordGevrey.baseSize EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) 0

The exact fixed-Hq jet sum equals the full mixed word base norm, with no dimension factor.

noncomputable def EulerCylinderSmoothOrbit.sobolev (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Actual mixed orbit smoothness supplies an existing genuine cylinder Sobolev element.

Equations

• EulerCylinderSmoothOrbit.sobolev period q u hu = EulerCylinderSobolevSpace.ofJet period (EulerCylinderSmoothOrbit.spatialJet period q u hu)

@[simp]

theorem EulerCylinderSmoothOrbit.sobolev_value (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : EulerCylinderSobolevSpace.value period (sobolev period q u hu) = u

theorem EulerCylinderSmoothOrbit.exists_smooth_representative (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space), (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) ∧ ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g

The existing reconstruction theorem now applies to actual full mixed translation derivatives.

noncomputable def EulerCylinderSmoothOrbit.representative (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space

A genuine smooth cylinder representative of the solved L² field.

Equations

• EulerCylinderSmoothOrbit.representative period u hu = Classical.choose ⋯

theorem EulerCylinderSmoothOrbit.representative_smooth (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (representative period u hu) x)

theorem EulerCylinderSmoothOrbit.representative_ae (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure period] representative period u hu