Classical lifted closedness of actual smooth representatives of the closed L² gradient space.

instance EulerClassicalPressureCurl.liftMeasure_openPos (period : ℝ) [Fact (0 < period)] : (EulerLiftedGradientSpace.liftMeasure period).IsOpenPosMeasure

Product cylinder volume assigns positive measure to every nonempty open set.

theorem EulerClassicalPressureCurl.fieldDerivative_mul (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (f g : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerTransportDerivatives.fieldDerivative period a (fun (y : EulerLiftedGradientSpace.LiftDomain period) => f y * g y) x = EulerTransportDerivatives.fieldDerivative period a f x * g x + f x * EulerTransportDerivatives.fieldDerivative period a g x

The scalar directional product rule in the genuine cylinder covering coordinates.

theorem EulerClassicalPressureCurl.scalar_product_integrable (period : ℝ) [Fact (0 < period)] (f g : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x * g x) (EulerLiftedGradientSpace.liftMeasure period)

A smooth scalar field times a compact smooth scalar field is integrable.

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

Scalar integration by parts with only the test factor compactly supported.

theorem EulerClassicalPressureCurl.smooth_eq_zero_of_compact_test_integrals (period : ℝ) [Fact (0 < period)] (q : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hq : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period q x)) (htest : ∀ (ψ : EulerLiftedGradientSpace.LiftDomain period → ℝ), HasCompactSupport ψ → (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period ψ x)) → ∫ (x : EulerLiftedGradientSpace.LiftDomain period), q x * ψ x ∂EulerLiftedGradientSpace.liftMeasure period = 0) (x : EulerLiftedGradientSpace.LiftDomain period) : q x = 0

A smooth scalar cylinder field annihilating every compact smooth test is pointwise zero.

theorem EulerClassicalPressureCurl.gradientSpace_classical_curl_zero (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (p : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hp : p ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑p =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) (i j : Fin 3) : (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m i) g x).ofLp j = (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m j) g x).ofLp i

Every smooth representative of an element of the closed lifted gradient space is classically closed.