A genuine smooth scalar graph pressure obtained from the closed lifted L² gradient space.

noncomputable def EulerGraphPressurePotential.cylinderGraph (period k : ℝ) (m x : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.LiftDomain period

The oscillating physical graph in the actual periodic cylinder.

Equations

• EulerGraphPressurePotential.cylinderGraph period k m x = (x, ↑(k * inner ℝ m x))

theorem EulerGraphPressurePotential.lifted_symmetry_of_coordinates (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (L : EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.Vector3) (hL : ∀ (i j : Fin 3), (L (EulerMetricTransport.coordinateDirection κ m i)).ofLp j = (L (EulerMetricTransport.coordinateDirection κ m j)).ofLp i) (a b : EulerLiftedGradientSpace.Vector3) : inner ℝ (L (EulerMetricTransport.transportDirection κ m a)) b = inner ℝ (L (EulerMetricTransport.transportDirection κ m b)) a

Coordinate lifted symmetry implies symmetry on arbitrary spatial vectors.

theorem EulerGraphPressurePotential.gradientSpace_has_graph_potential (period : ℝ) [Fact (0 < period)] (κ k : ℝ) (hκ : k * κ = 1) (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)) : ∃ (q : EulerLiftedGradientSpace.Vector3 → ℝ), ContDiff ℝ (↑⊤) q ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = κ • g (cylinderGraph period k m x)

A smooth representative of a lifted L² gradient has a genuine smooth scalar pressure on every physical graph.

theorem EulerGraphPressurePotential.coercive_pressure_has_graph_potential (period : ℝ) [Fact (0 < period)] (A : EulerSpatialSobolevInverse.SmoothCoefficient period) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (K : (s : ℕ) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (J : (s : ℕ) → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) (κ k : ℝ) (hκ : k * κ = 1) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) : ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (q : EulerLiftedGradientSpace.Vector3 → ℝ), (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) ∧ ↑↑(A.pressure κ m c hc hpos f) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g ∧ ContDiff ℝ (↑⊤) q ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), gradient q x = κ • g (cylinderGraph period k m x)

All-order coefficient and forcing jets yield an actual smooth scalar potential for the coercive graph pressure.