Actual differentiation through the oscillating phase graph and a parent flow. These identities convert the normalized lifted equation into the ordinary Euler momentum residual of the physical perturbation.

noncomputable def EulerPacketPhysicalTransform.spaceTimeGraph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (k : ℝ) (m : E) : ℝ × E →L[ℝ] ℝ × E × ℝ

Space time graph, given by (fst ℝ ℝ E).prod ((graphMap k m).comp (snd ℝ ℝ E)).

Equations

• EulerPacketPhysicalTransform.spaceTimeGraph k m = (ContinuousLinearMap.fst ℝ ℝ E).prod (EulerGraphPullback.graphMap k m ∘SL ContinuousLinearMap.snd ℝ ℝ E)

theorem EulerPacketPhysicalTransform.spaceTimeGraph_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (k : ℝ) (m : E) (q : ℝ × E) : (spaceTimeGraph k m) q = (q.1, q.2, k * inner ℝ m q.2)

noncomputable def EulerPacketPhysicalTransform.graphVelocity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ k : ℝ) (m : E) (F : ℝ × E → E →L[ℝ] E) (z : ℝ × E × ℝ → E) (q : ℝ × E) : E

Graph velocity, given by κ • F q (z (spaceTimeGraph k m q)).

Equations

• EulerPacketPhysicalTransform.graphVelocity κ k m F z q = κ • (F q) (z ((EulerPacketPhysicalTransform.spaceTimeGraph k m) q))

theorem EulerPacketPhysicalTransform.graphVelocity_hasFDerivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ k : ℝ) (m : E) (F : ℝ × E → E →L[ℝ] E) (z : ℝ × E × ℝ → E) (q : ℝ × E) (DF : ℝ × E →L[ℝ] E →L[ℝ] E) (Dz : ℝ × E × ℝ →L[ℝ] E) (hF : HasFDerivAt F DF q) (hz : HasFDerivAt z Dz ((spaceTimeGraph k m) q)) : HasFDerivAt (graphVelocity κ k m F z) (κ • (F q ∘SL Dz ∘SL spaceTimeGraph k m + DF.flip (z ((spaceTimeGraph k m) q)))) q

theorem EulerPacketPhysicalTransform.graphVelocity_fderiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ k : ℝ) (m : E) (F : ℝ × E → E →L[ℝ] E) (z : ℝ × E × ℝ → E) (q : ℝ × E) (DF : ℝ × E →L[ℝ] E →L[ℝ] E) (Dz : ℝ × E × ℝ →L[ℝ] E) (hF : HasFDerivAt F DF q) (hz : HasFDerivAt z Dz ((spaceTimeGraph k m) q)) (v : ℝ × E) : (fderiv ℝ (graphVelocity κ k m F z) q) v = κ • ((DF v) (z ((spaceTimeGraph k m) q)) + (F q) (Dz ((spaceTimeGraph k m) v)))

theorem EulerPacketPhysicalTransform.graph_residual_identity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ k : ℝ) (hκ : k * κ = 1) (m : E) (F : ℝ × E → E →L[ℝ] E) (z : ℝ × E × ℝ → E) (q : ℝ × E) (DF : ℝ × E →L[ℝ] E →L[ℝ] E) (Dz : ℝ × E × ℝ →L[ℝ] E) (hF : HasFDerivAt F DF q) (hz : HasFDerivAt z Dz ((spaceTimeGraph k m) q)) (A : E ≃L[ℝ] E) (hA : F q = ↑A) (p : E) : (fderiv ℝ (graphVelocity κ k m F z) q) (1, 0) + (DF (1, 0)) (A.symm (graphVelocity κ k m F z q)) + (fderiv ℝ (graphVelocity κ k m F z) q) (0, A.symm (graphVelocity κ k m F z q)) + (ContinuousLinearMap.adjoint ↑A.symm) (κ • p) = κ • A (Dz (1, 0, 0) + 2 • A.symm ((DF (1, 0)) (z ((spaceTimeGraph k m) q))) + Dz (0, κ • z ((spaceTimeGraph k m) q), inner ℝ m (z ((spaceTimeGraph k m) q))) + κ • A.symm ((DF (0, z ((spaceTimeGraph k m) q))) (z ((spaceTimeGraph k m) q))) + A.symm ((ContinuousLinearMap.adjoint ↑A.symm) p))

The normalized equation is exactly the ordinary Lagrangian perturbation equation after evaluation on the phase graph, with its actual derivatives.

theorem EulerPacketPhysicalTransform.euler_residual_of_pullback {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (u w : ℝ × E → E) (p q : ℝ × E → ℝ) (X G : ℝ × E → E) (Q : ℝ × E → ℝ) (t : ℝ) (x : E) (A : E ≃L[ℝ] E) (Du Dw DG : ℝ × E →L[ℝ] E) (hXtime : HasDerivAt (fun (s : ℝ) => X (s, x)) (u (t, X (t, x))) t) (hXspace : HasFDerivAt (fun (y : E) => X (t, y)) (↑A) x) (hu : HasFDerivAt u Du (t, X (t, x))) (hw : HasFDerivAt w Dw (t, X (t, x))) (hG : HasFDerivAt G DG (t, x)) (hp : DifferentiableAt ℝ (fun (y : E) => p (t, y)) (X (t, x))) (hq : DifferentiableAt ℝ (fun (y : E) => q (t, y)) (X (t, x))) (hwX : ∀ (s : ℝ) (y : E), w (s, X (s, y)) = G (s, y)) (hqX : ∀ (y : E), q (t, X (t, y)) = Q (t, y)) (hparent : EulerLagrangian.momentumResidual u p (t, X (t, x)) = 0) : EulerLagrangian.momentumResidual (fun (y : ℝ × E) => u y + w y) (fun (y : ℝ × E) => p y + q y) (t, X (t, x)) = DG (1, 0) + Du (0, G (t, x)) + DG (0, A.symm (G (t, x))) + (ContinuousLinearMap.adjoint ↑A.symm) (gradient (fun (y : E) => Q (t, y)) x)

A literal pullback identity determines the physical momentum residual. The hypotheses are genuine derivatives of the parent flow and the two fields.

def EulerPacketPhysicalTransform.inverseCoordinates {E : Type u_1} (Y : ℝ × E → E) (q : ℝ × E) : ℝ × E

Inverse coordinates, given by (q.1,Y q).

Equations

• EulerPacketPhysicalTransform.inverseCoordinates Y q = (q.1, Y q)

noncomputable def EulerPacketPhysicalTransform.physicalVelocity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ k : ℝ) (m : E) (F : ℝ × E → E →L[ℝ] E) (z : ℝ × E × ℝ → E) (Y : ℝ × E → E) : ℝ × E → E

Physical velocity, defined pointwise by graphVelocity κ k m F z (inverseCoordinates Y q).

Equations

• EulerPacketPhysicalTransform.physicalVelocity κ k m F z Y q = EulerPacketPhysicalTransform.graphVelocity κ k m F z (EulerPacketPhysicalTransform.inverseCoordinates Y q)

def EulerPacketPhysicalTransform.physicalPressure {E : Type u_1} (Q : ℝ × E → ℝ) (Y : ℝ × E → E) : ℝ × E → ℝ

Physical pressure, defined pointwise by Q (inverseCoordinates Y q).

Equations

• EulerPacketPhysicalTransform.physicalPressure Q Y q = Q (EulerPacketPhysicalTransform.inverseCoordinates Y q)

theorem EulerPacketPhysicalTransform.physical_euler_momentum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (κ k : ℝ) (hκ : k * κ = 1) (m : E) (F : ℝ × E → E →L[ℝ] E) (z : ℝ × E × ℝ → E) (u : ℝ × E → E) (p Q : ℝ × E → ℝ) (X Y : ℝ × E → E) (t : ℝ) (x : E) (A : E ≃L[ℝ] E) (DF : ℝ × E →L[ℝ] E →L[ℝ] E) (Dz : ℝ × E × ℝ →L[ℝ] E) (Du : ℝ × E →L[ℝ] E) (P : E) (hleft : ∀ (s : ℝ) (y : E), Y (s, X (s, y)) = y) (hY : DifferentiableAt ℝ (inverseCoordinates Y) (t, X (t, x))) (hXtime : HasDerivAt (fun (s : ℝ) => X (s, x)) (u (t, X (t, x))) t) (hXspace : HasFDerivAt (fun (y : E) => X (t, y)) (↑A) x) (hF : HasFDerivAt F DF (t, x)) (hz : HasFDerivAt z Dz ((spaceTimeGraph k m) (t, x))) (hA : F (t, x) = ↑A) (hu : HasFDerivAt u Du (t, X (t, x))) (hp : DifferentiableAt ℝ (fun (y : E) => p (t, y)) (X (t, x))) (hQ : DifferentiableAt ℝ (fun (y : E) => Q (t, y)) x) (hstrain : ∀ (v : E), Du (0, v) = (DF (1, 0)) (A.symm v)) (hQgradient : gradient (fun (y : E) => Q (t, y)) x = κ • P) (hparent : EulerLagrangian.momentumResidual u p (t, X (t, x)) = 0) (hlift : Dz (1, 0, 0) + 2 • A.symm ((DF (1, 0)) (z ((spaceTimeGraph k m) (t, x)))) + Dz (0, κ • z ((spaceTimeGraph k m) (t, x)), inner ℝ m (z ((spaceTimeGraph k m) (t, x)))) + κ • A.symm ((DF (0, z ((spaceTimeGraph k m) (t, x)))) (z ((spaceTimeGraph k m) (t, x)))) + A.symm ((ContinuousLinearMap.adjoint ↑A.symm) P) = 0) : EulerLagrangian.momentumResidual (fun (q : ℝ × E) => u q + physicalVelocity κ k m F z Y q) (fun (q : ℝ × E) => p q + physicalPressure Q Y q) (t, X (t, x)) = 0

The physical perturbation is defined by the actual inverse flow. The normalized lifted equation, rather than a physical PDE hypothesis, forces its Euler momentum residual to vanish.