Literal agreement between the exact physical Euler fields and their constructed smooth L² representatives, including the scalar pressure.
theorem
EulerPacketPhysicalTransform.exact_physicalVelocity_eq
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
{P : ℝ}
[Fact (0 < P)]
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower P D.T}
{B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R)}
(S :
EulerAllOrderDriftCorrection.ExactLiftedPacket P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R) B)
(k : ℝ)
(F : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(Y : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), F (↑t, x) = (D.F.field t) x)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
physicalVelocity κ k D.m₀ F S.rawVelocity Y (↑t, x) = κ • ((D.F.field t) (Y (↑t, x)))
(S.velocity.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y (↑t, x))))
theorem
EulerPacketPhysicalTransform.exact_physicalPressure_gradient
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
{P : ℝ}
[Fact (0 < P)]
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower P D.T}
{B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R)}
(S :
EulerAllOrderDriftCorrection.ExactLiftedPacket P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R) B)
(X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x)
(hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t))
(hY : Continuous (Function.uncurry Y))
(k : ℝ)
(hk : k * κ = 1)
(Yraw : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hYraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Yraw (↑t, x) = Y t x)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
gradient (fun (y : EulerLiftedGradientSpace.Vector3) => physicalPressure (S.rawGraphPotential k) Yraw (↑t, y)) x = κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y t x)))
(S.pressure.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y t x)))
theorem
EulerPacketPhysicalTransform.exact_physicalPressure_smooth
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
{P : ℝ}
[Fact (0 < P)]
{κ : ℝ}
{hκ : |κ| ≤ 1}
{Z R : EulerAllOrderCorrectionData.FieldTower P D.T}
{B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R)}
(S :
EulerAllOrderDriftCorrection.ExactLiftedPacket P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R) B)
(X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x)
(hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t))
(hY : Continuous (Function.uncurry Y))
(k : ℝ)
(hk : k * κ = 1)
(Yraw : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hYraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Yraw (↑t, x) = Y t x)
(t : ↑(Set.Icc 0 D.T))
:
ContDiff ℝ ↑⊤ fun (y : EulerLiftedGradientSpace.Vector3) => physicalPressure (S.rawGraphPotential k) Yraw (↑t, y)