The closed lifted gradient space consists of distributionally curl-free fields. The proof uses actual compact scalar tests and mixed derivative symmetry, then passes to the L² closure through continuous inner products.

noncomputable def EulerLiftedCurl.scalarEmbedding : ℝ →L[ℝ] EulerLiftedGradientSpace.Vector3

Isometric inclusion of a scalar into the first Euclidean component.

Equations

• EulerLiftedCurl.scalarEmbedding = ContinuousLinearMap.toSpanSingleton ℝ (EuclideanSpace.single 0 1)

theorem EulerLiftedCurl.scalarEmbedding_inner (r s : ℝ) : inner ℝ (scalarEmbedding r) (scalarEmbedding s) = r * s

theorem EulerLiftedCurl.fieldDerivative_linear (period : ℝ) {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (f : EulerLiftedGradientSpace.LiftDomain period → V) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (a : EulerLiftedGradientSpace.LiftTangent) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerTransportDerivatives.fieldDerivative period a (fun (y : EulerLiftedGradientSpace.LiftDomain period) => L (f y)) x = L (EulerTransportDerivatives.fieldDerivative period a f x)

theorem EulerLiftedCurl.scalar_embedding_smooth (period : ℝ) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period φ x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (fun (y : EulerLiftedGradientSpace.LiftDomain period) => scalarEmbedding (φ y)) x)

theorem EulerLiftedCurl.scalar_embedding_compact (period : ℝ) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφ : HasCompactSupport φ) : HasCompactSupport fun (x : EulerLiftedGradientSpace.LiftDomain period) => scalarEmbedding (φ x)

theorem EulerLiftedCurl.scalar_integration_by_parts (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (φ ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφc : HasCompactSupport φ) (hψc : HasCompactSupport ψ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period φ x)) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), EulerTransportDerivatives.fieldDerivative period a φ x * ψ x ∂EulerLiftedGradientSpace.liftMeasure period = -∫ (x : EulerLiftedGradientSpace.LiftDomain period), φ x * EulerTransportDerivatives.fieldDerivative period a ψ x ∂EulerLiftedGradientSpace.liftMeasure period

Genuine scalar integration by parts on the cylinder in any constant covering direction.

theorem EulerLiftedCurl.fieldDerivatives_commute (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a b : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerTransportDerivatives.fieldDerivative period a (EulerTransportDerivatives.fieldDerivative period b f) x = EulerTransportDerivatives.fieldDerivative period b (EulerTransportDerivatives.fieldDerivative period a f) x

noncomputable def EulerLiftedCurl.curlTest (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

A compact antisymmetric derivative test field for one lifted curl component.

Equations

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

theorem EulerLiftedCurl.curlTest_smooth (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (curlTest period κ m i j ψ) x)

theorem EulerLiftedCurl.curlTest_compact (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hψ : HasCompactSupport ψ) : HasCompactSupport (curlTest period κ m i j ψ)

theorem EulerLiftedCurl.vector_curlTest_inner (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3) : inner ℝ v (curlTest period κ m i j ψ x) = v.ofLp i * EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m j) ψ x - v.ofLp j * EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m i) ψ x

theorem EulerLiftedCurl.liftedGradient_component (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) (i : Fin 3) : (EulerLiftedGradientSpace.liftedGradient period κ m φ x).ofLp i = EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m i) φ x

theorem EulerLiftedCurl.scalar_derivative_product_integrable (period : ℝ) [Fact (0 < period)] (a b : EulerLiftedGradientSpace.LiftTangent) (φ ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφc : HasCompactSupport φ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period φ x)) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerTransportDerivatives.fieldDerivative period a φ x * EulerTransportDerivatives.fieldDerivative period b ψ x) (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerLiftedCurl.test_gradient_curl_integral (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (φ ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφc : HasCompactSupport φ) (hψc : HasCompactSupport ψ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period φ x)) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ (EulerLiftedGradientSpace.liftedGradient period κ m φ x) (curlTest period κ m i j ψ x) ∂EulerLiftedGradientSpace.liftMeasure period = 0

noncomputable def EulerLiftedCurl.curlTestLp (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hψc : HasCompactSupport ψ) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The L² realization of an actual compact lifted curl test.

Equations

• EulerLiftedCurl.curlTestLp period κ m i j ψ hψc hψ = EulerLiftedWeakDerivative.smoothFieldLp period (EulerLiftedCurl.curlTest period κ m i j ψ) ⋯ ⋯

theorem EulerLiftedCurl.curlTestLp_ae (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hψc : HasCompactSupport ψ) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) : ↑↑(curlTestLp period κ m i j ψ hψc hψ) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] curlTest period κ m i j ψ

theorem EulerLiftedCurl.generator_curl_pairing (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hψc : HasCompactSupport ψ) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) {g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hg : g ∈ {g : ↥(EulerLiftedGradientSpace.LiftL2 period) | ∃ (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ), (HasCompactSupport φ ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period φ x)) ∧ ↑↑g =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerLiftedGradientSpace.liftedGradient period κ m φ}) : inner ℝ g (curlTestLp period κ m i j ψ hψc hψ) = 0

theorem EulerLiftedCurl.gradient_curl_pairing (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hψc : HasCompactSupport ψ) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hp : p ∈ EulerLiftedGradientSpace.gradientSpace period κ m) : inner ℝ p (curlTestLp period κ m i j ψ hψc hψ) = 0

theorem EulerLiftedCurl.gradientSpace_weak_curl_zero (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hp : p ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (i j : Fin 3) (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hψc : HasCompactSupport ψ) (hψ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), (↑↑p x).ofLp i * EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m j) ψ x - (↑↑p x).ofLp j * EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m i) ψ x ∂EulerLiftedGradientSpace.liftMeasure period = 0

Every field in the closed lifted gradient space has zero distributional lifted curl.