A genuine smooth ordinary solenoidal L² field remains solenoidal on the periodic cylinder.
theorem
EulerMeanCylinderSolenoidal.fieldDerivative_spatial
(P : ℝ)
(f : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hf : ContDiff ℝ (↑⊤) f)
(a : EulerLiftedGradientSpace.LiftTangent)
(z : EulerLiftedGradientSpace.LiftDomain P)
:
EulerTransportDerivatives.fieldDerivative P a (fun (x : EulerLiftedGradientSpace.LiftDomain P) => f x.1) z = (fderiv ℝ f z.1) a.1
theorem
EulerMeanCylinderSolenoidal.lift_classical_divergence
(P κ : ℝ)
(m : EulerSmoothLimit.Space)
(f : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hf : ContDiff ℝ (↑⊤) f)
(hd : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence f x = 0)
(z : EulerLiftedGradientSpace.LiftDomain P)
:
∑ i : Fin 3,
(EulerTransportDerivatives.fieldDerivative P (EulerMetricTransport.coordinateDirection κ m i)
(fun (x : EulerLiftedGradientSpace.LiftDomain P) => f x.1) z).ofLp
i = 0
theorem
EulerMeanCylinderSolenoidal.embedding_representative
(P : ℝ)
[Fact (0 < P)]
(u : ↥EulerMeanSolenoidal.L2)
(f : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hrep : ↑↑u =ᵐ[MeasureTheory.volume] f)
:
↑↑((EulerCylinderSpatialEmbedding.embedding P) u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (z : EulerLiftedGradientSpace.LiftDomain P) => f z.1
theorem
EulerMeanCylinderSolenoidal.embedding_mem
(P : ℝ)
[Fact (0 < P)]
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(u : ↥EulerMeanSolenoidal.L2)
(hu : u ∈ EulerMeanSolenoidal.solenoidalSpace)
(f : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hf : ContDiff ℝ (↑⊤) f)
(hrep : ↑↑u =ᵐ[MeasureTheory.volume] f)
:
The conclusion is membership in the actual closed lifted-gradient orthogonal complement.
theorem
EulerMeanCylinderSolenoidal.embedding_mem_of_smooth_orbit
(P : ℝ)
[Fact (0 < P)]
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(u : ↥EulerMeanSolenoidal.L2)
(hu : u ∈ EulerMeanSolenoidal.solenoidalSpace)
(hs : EulerMeanSmoothRepresentative.SmoothOrbit u)
: