The actual parent velocity plus the constructed exact packet satisfies both classical Euler equations in physical coordinates.
The actual exact packet remains incompressible after the genuine unit-Jacobian parent-flow coordinate change.
theorem
EulerPacketPhysicalTransform.exact_source_divergence
{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 : ℝ)
(hk : k * κ = 1)
(F : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(X Y : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(hmatch : ∀ (y : EulerSmoothLimit.Space), F (↑t, y) = (D.F.field t) y)
(hX : ContDiffAt ℝ 2 (fun (y : EulerSmoothLimit.Space) => X (↑t, y)) x)
(hspace : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ (fun (a : EulerSmoothLimit.Space) => X (↑t, a)) y = F (↑t, y))
(hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix (F (↑t, y))) = 1)
(hleft : ∀ (y : EulerSmoothLimit.Space), Y (↑t, X (↑t, y)) = y)
(hY : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => Y (↑t, y)) (X (↑t, x)))
:
EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => physicalVelocity κ k D.m₀ F S.rawVelocity Y (↑t, y))
(X (↑t, x)) = 0
theorem
EulerPacketPhysicalTransform.exact_source_velocity_differentiableAt
{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)
(X Y : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 D.T)
(x : EulerSmoothLimit.Space)
(hleft : Y (t, X (t, x)) = x)
(hY : DifferentiableAt ℝ (inverseCoordinates Y) (t, X (t, x)))
(hX : ContDiffAt ℝ 2 X (t, x))
(hframe :
F =ᶠ[nhds (t, x)] fun (r : ℝ × EulerSmoothLimit.Space) =>
fderiv ℝ X r ∘SL ContinuousLinearMap.inr ℝ ℝ EulerSmoothLimit.Space)
:
DifferentiableAt ℝ (physicalVelocity κ k D.m₀ F S.rawVelocity Y) (t, X (t, x))
theorem
EulerPacketPhysicalTransform.exact_source_euler
{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 : ℝ)
(hk : k * κ = 1)
(F : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(p : ℝ × EulerSmoothLimit.Space → ℝ)
(X Y : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hmatch : ∀ (s : ↑(Set.Icc 0 D.T)) (y : EulerSmoothLimit.Space), F (↑s, y) = (D.F.field s) y)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 D.T)
(x : EulerSmoothLimit.Space)
(hleft : ∀ (s : ℝ) (y : EulerSmoothLimit.Space), Y (s, X (s, y)) = y)
(hY : DifferentiableAt ℝ (inverseCoordinates Y) (t, X (t, x)))
(hX : ContDiffAt ℝ 2 X (t, x))
(hframe :
F =ᶠ[nhds (t, x)] fun (r : ℝ × EulerSmoothLimit.Space) =>
fderiv ℝ X r ∘SL ContinuousLinearMap.inr ℝ ℝ EulerSmoothLimit.Space)
(hflow :
(fun (r : ℝ × EulerSmoothLimit.Space) => (fderiv ℝ X r) (1, 0)) =ᶠ[nhds (t, x)] fun (r : ℝ × EulerSmoothLimit.Space) => u (r.1, X r))
(hspace : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ (fun (a : EulerSmoothLimit.Space) => X (t, a)) y = F (t, y))
(hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix (F (t, y))) = 1)
(hu : DifferentiableAt ℝ u (t, X (t, x)))
(hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => p (t, y)) (X (t, x)))
(hparent : EulerLagrangian.momentumResidual u p (t, X (t, x)) = 0)
(hdiv : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => u (t, y)) (X (t, x)) = 0)
:
EulerLagrangian.momentumResidual
(fun (q : ℝ × EulerSmoothLimit.Space) => u q + physicalVelocity κ k D.m₀ F S.rawVelocity Y q)
(fun (q : ℝ × EulerSmoothLimit.Space) => p q + physicalPressure (S.rawGraphPotential k) Y q) (t, X (t, x)) = 0 ∧ EulerSmoothLimit.divergence
(fun (y : EulerSmoothLimit.Space) => u (t, y) + physicalVelocity κ k D.m₀ F S.rawVelocity Y (t, y)) (X (t, x)) = 0
The classical momentum and incompressibility equations for the actual new velocity, using the constructed normalized scalar pressure.