Genuine smooth ordinary-space representatives reconstructed from smooth L² translation orbits.

An isometric embedding of ordinary R³ L² into the angle-independent part of the unit cylinder.

theorem EulerMeanOrdinaryLift.instMeanOrdinaryLift1 : Fact (0 < 1)

theorem EulerMeanOrdinaryLift.instMeanOrdinaryLift2 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem EulerMeanOrdinaryLift.ordinaryProjection_measurePreserving : MeasureTheory.MeasurePreserving Prod.fst (EulerLiftedGradientSpace.liftMeasure 1) MeasureTheory.volume

noncomputable def EulerMeanOrdinaryLift.ordinaryLift : ↥EulerMeanSolenoidal.L2 →ₗᵢ[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 1)

The added angle has mass one, so this is a genuine L² isometry.

Equations

• EulerMeanOrdinaryLift.ordinaryLift = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ Prod.fst EulerMeanOrdinaryLift.ordinaryProjection_measurePreserving

theorem EulerMeanOrdinaryLift.ordinaryLift_ae (u : ↥EulerMeanSolenoidal.L2) : ↑↑(ordinaryLift u) =ᵐ[EulerLiftedGradientSpace.liftMeasure 1] fun (x : EulerLiftedGradientSpace.LiftDomain 1) => ↑↑u x.1

theorem EulerMeanOrdinaryLift.ordinaryLift_translation (a : EulerLiftedGradientSpace.LiftDomain 1) (u : ↥EulerMeanSolenoidal.L2) : (EulerLiftedGradientSpace.translation 1 a) (ordinaryLift u) = ordinaryLift ((EulerMeanSolenoidal.translation a.1) u)

Every cylinder translation acts through its actual spatial component on this embedding.

theorem EulerMeanOrdinaryLift.smooth_angle_slice (g : EulerLiftedGradientSpace.LiftDomain 1 → EulerSmoothLimit.Space) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain 1), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift 1 g x)) (θ : AddCircle 1) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => g (x, θ)

A smooth cylinder field restricts to a smooth ordinary field at every fixed angle.

theorem EulerMeanOrdinaryLift.exists_smooth_of_lift (u : ↥EulerMeanSolenoidal.L2) (g : EulerLiftedGradientSpace.LiftDomain 1 → EulerSmoothLimit.Space) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain 1), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift 1 g x)) (hrep : ↑↑(ordinaryLift u) =ᵐ[EulerLiftedGradientSpace.liftMeasure 1] g) : ∃ (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space), ContDiff ℝ (↑⊤) f ∧ ↑↑u =ᵐ[MeasureTheory.volume] f

Fubini selects a genuine spatial representative from a smooth representative of the lift.

theorem EulerMeanSmoothRepresentative.instMeanSmoothRepresentative1 : Fact (0 < 1)

@[reducible, inline]

abbrev EulerMeanSmoothRepresentative.SmoothOrbit (u : ↥EulerMeanSolenoidal.L2) : Prop

Smoothness is required only of the actual ordinary L² translation orbit.

Equations

• EulerMeanSmoothRepresentative.SmoothOrbit u = ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u

noncomputable def EulerMeanSmoothRepresentative.orbitDerivative (u : ↥EulerMeanSolenoidal.L2) (v : EulerSmoothLimit.Space) : ↥EulerMeanSolenoidal.L2

Orbit derivative, given by fderiv ℝ (fun a : Space => EulerMeanSolenoidal.translation a u) 0 v.

Equations

• EulerMeanSmoothRepresentative.orbitDerivative u v = (fderiv ℝ (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) 0) v

theorem EulerMeanSmoothRepresentative.orbitDerivative_translation (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v a : EulerSmoothLimit.Space) : (EulerMeanSolenoidal.translation a) (orbitDerivative u v) = (fderiv ℝ (fun (b : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation b) u) a) v

An orbit derivative is itself an actual translated field, at every base point.

theorem EulerMeanSmoothRepresentative.orbitDerivative_smooth (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v : EulerSmoothLimit.Space) : SmoothOrbit (orbitDerivative u v)

theorem EulerMeanSmoothRepresentative.orbitDerivative_hasDerivAt (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (v : EulerSmoothLimit.Space) : HasDerivAt (fun (t : ℝ) => (EulerMeanSolenoidal.translation (t • v)) u) (orbitDerivative u v) 0

theorem EulerMeanSmoothRepresentative.ordinaryLift_hasDerivAt (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (a : EulerLiftedGradientSpace.LiftTangent) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation 1 (EulerPressureSpatialRegularity.translationPath 1 a t)) (EulerMeanOrdinaryLift.ordinaryLift u)) (EulerMeanOrdinaryLift.ordinaryLift (orbitDerivative u a.1)) 0

The cylinder jet uses the actual spatial derivative, with zero angular derivative automatically.

def EulerMeanSmoothRepresentative.ordinarySpatialJet (s : ℕ) (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : EulerSpatialSobolevInverse.SpatialJet 1 EulerCylinderSobolev.standardDirection s (EulerMeanOrdinaryLift.ordinaryLift u)

Every finite cylinder derivative tree is constructed from genuine ordinary L² derivatives.

Equations

• One or more equations did not get rendered due to their size.
• EulerMeanSmoothRepresentative.ordinarySpatialJet 0 u hu = EulerSpatialSobolevInverse.SpatialJet.zero (EulerMeanOrdinaryLift.ordinaryLift u)

theorem EulerMeanSmoothRepresentative.exists_smooth_representative (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : ∃ (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space), ContDiff ℝ (↑⊤) f ∧ ↑↑u =ᵐ[MeasureTheory.volume] f

A smooth genuine L² translation orbit has a genuine C∞ representative on ordinary R³.

noncomputable def EulerMeanSmoothRepresentative.representative (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

The reconstructed representative is independent of all choices, by continuous uniqueness.

Equations

• EulerMeanSmoothRepresentative.representative u hu = Classical.choose ⋯

theorem EulerMeanSmoothRepresentative.representative_smooth (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : ContDiff ℝ (↑⊤) (representative u hu)

theorem EulerMeanSmoothRepresentative.representative_ae (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : ↑↑u =ᵐ[MeasureTheory.volume] representative u hu

theorem EulerMeanSmoothRepresentative.representative_unique (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) : representative u hu = f