The actual pointwise equation of the exact packet, expressed with the prescribed deformation and its genuine time and spatial derivatives.
theorem
EulerPacketPhysicalTransform.source_frame_time
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(F : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hmatch : ∀ (s : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), F (↑s, x) = (D.F.field s) x)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 D.T)
(x : EulerSmoothLimit.Space)
(DF : ℝ × EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hF : HasFDerivAt F DF (t, x))
:
theorem
EulerPacketPhysicalTransform.source_frame_spatial
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(F : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hmatch : ∀ (s : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), F (↑s, x) = (D.F.field s) x)
(t : ↑(Set.Icc 0 D.T))
(x v : EulerSmoothLimit.Space)
(DF : ℝ × EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hF : HasFDerivAt F DF (↑t, x))
:
theorem
EulerAllOrderDriftCorrection.ExactLiftedPacket.source_equation
{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 : Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R)}
(S : ExactLiftedPacket P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R) B)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 D.T)
(z : EulerLiftedGradientSpace.LiftTangent)
:
(fderiv ℝ S.rawVelocity (t, z)) (1, 0) + 2 • ((D.FInv.field ⟨t, ⋯⟩) z.1) (((D.F₁.field ⟨t, ⋯⟩) z.1) (S.rawVelocity (t, z))) + (fderiv ℝ S.rawVelocity (t, z)) (0, κ • S.rawVelocity (t, z), inner ℝ D.m₀ (S.rawVelocity (t, z))) + κ • ((D.FInv.field ⟨t, ⋯⟩) z.1)
(((fderiv ℝ (⇑(D.F.field ⟨t, ⋯⟩)) z.1) (S.rawVelocity (t, z))) (S.rawVelocity (t, z))) + ((D.FInv.field ⟨t, ⋯⟩) z.1) ((ContinuousLinearMap.adjoint ((D.FInv.field ⟨t, ⋯⟩) z.1)) (S.rawPressure (t, z))) = 0
theorem
EulerAllOrderDriftCorrection.ExactLiftedPacket.source_equation_of_frame
{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 : Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R)}
(S : ExactLiftedPacket P ⋯ (EulerPacketCorrectionCoefficients.correctionData D P κ hκ Z R) B)
(F : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hmatch : ∀ (s : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), F (↑s, x) = (D.F.field s) x)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 D.T)
(z : EulerLiftedGradientSpace.LiftTangent)
(DF : ℝ × EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hF : HasFDerivAt F DF (t, z.1))
:
(fderiv ℝ S.rawVelocity (t, z)) (1, 0) + 2 • (D.deformationEquiv ⟨t, ⋯⟩ z.1).symm ((DF (1, 0)) (S.rawVelocity (t, z))) + (fderiv ℝ S.rawVelocity (t, z)) (0, κ • S.rawVelocity (t, z), inner ℝ D.m₀ (S.rawVelocity (t, z))) + κ • (D.deformationEquiv ⟨t, ⋯⟩ z.1).symm ((DF (0, S.rawVelocity (t, z))) (S.rawVelocity (t, z))) + (D.deformationEquiv ⟨t, ⋯⟩ z.1).symm
((ContinuousLinearMap.adjoint ↑(D.deformationEquiv ⟨t, ⋯⟩ z.1).symm) (S.rawPressure (t, z))) = 0