The actual total pressure of an exact lifted packet has a canonically normalized scalar pressure on the oscillating graph.

Genuine lifted divergence-free fields remain divergence-free on the oscillating graph.

theorem EulerGraphDivergence.divergenceFree_graph (period : ℝ) [Fact (0 < period)] (κ k : ℝ) (hκ : k * κ = 1) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.Vector3) : ∑ i : Fin 3, ((fderiv ℝ (fun (y : EulerLiftedGradientSpace.Vector3) => g (EulerGraphPressurePotential.cylinderGraph period k m y)) x) (EuclideanSpace.single i 1)).ofLp i = 0

The physical graph of an actual smooth representative of a lifted solenoidal L² field is classically divergence-free.

noncomputable def EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPressure {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3

Graph pressure, given by A.κ • S.pressure.pointField t (cylinderGraph P k A.direction x).

Equations

• S.graphPressure k t x = A.κ • S.pressure.pointField t (EulerGraphPressurePotential.cylinderGraph P k A.direction x)

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPressure_joint_continuous {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) : Continuous (Function.uncurry (S.graphPressure k))

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPressure_has_potential {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) : ∃ (q : EulerLiftedGradientSpace.Vector3 → ℝ), ContDiff ℝ (↑⊤) q ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), _root_.gradient q x = S.graphPressure k t x

noncomputable def EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPotential {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (t : ↑(Set.Icc 0 T)) : EulerLiftedGradientSpace.Vector3 → ℝ

Graph potential, given by radialPotential (S.graphPressure k t).

Equations

• S.graphPotential k t = EulerCanonicalGraphPotential.radialPotential (S.graphPressure k t)

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPotential_zero {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (t : ↑(Set.Icc 0 T)) : S.graphPotential k t 0 = 0

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPotential_joint_continuous {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) : Continuous (Function.uncurry (S.graphPotential k))

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPotential_smooth {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (S.graphPotential k t)

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.graphPotential_gradient {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : _root_.gradient (S.graphPotential k t) x = A.κ • S.pressure.pointField t (EulerGraphPressurePotential.cylinderGraph P k A.direction x)

noncomputable def EulerAllOrderDriftCorrection.ExactLiftedPacket.rawGraphPotential {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (q : ℝ × EulerLiftedGradientSpace.Vector3) : ℝ

Raw graph potential, given by S.graphPotential k (projIcc 0 T hT.le q.1) q.2.

Equations

• S.rawGraphPotential k q = S.graphPotential k (Set.projIcc 0 T ⋯ q.1) q.2

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.rawGraphPotential_smooth {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (hk : k * A.κ = 1) (t : ℝ) : ContDiff ℝ ↑⊤ fun (x : EulerLiftedGradientSpace.Vector3) => S.rawGraphPotential k (t, x)

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.rawGraphPotential_gradient {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (hk : k * A.κ = 1) (t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : _root_.gradient (fun (y : EulerLiftedGradientSpace.Vector3) => S.rawGraphPotential k (t, y)) x = A.κ • S.rawPressure (t, x, k * inner ℝ A.direction x)

theorem EulerAllOrderDriftCorrection.ExactLiftedPacket.graphVelocity_divergence {P T : ℝ} [Fact (0 < P)] {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} {B : Budget P hT A} (S : ExactLiftedPacket P hT A B) (k : ℝ) (hk : k * A.κ = 1) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ∑ i : Fin 3, ((fderiv ℝ (fun (y : EulerLiftedGradientSpace.Vector3) => S.velocity.pointField t (EulerGraphPressurePotential.cylinderGraph P k A.direction y)) x) (EuclideanSpace.single i 1)).ofLp i = 0