The literal linear, pressure and nonlinear jet expressions have actual cylinder-path witnesses.

noncomputable def EulerPacketCylinderField.SpatialJetField.slowAdvection {P T : ℝ} [Fact (0 < P)] {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} {inverse : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T inverse) (G : SpatialJetField P T J) (H : SpatialJetField P T K) : Field P T fun (z : EulerPacketPointJets.Domain) => ((EulerPacketPointJets.slowAdvection (inverse z)) (J z)) (K z)

Slow advection as an element of Field P T (fun z => EulerPacketPointJets.slowAdvection (inverse z) (J z) (K z)).

Equations

• EulerPacketCylinderField.SpatialJetField.slowAdvection A G H = ((A.multiply G.field).spatialTransport H.field).congr ⋯

noncomputable def EulerPacketCylinderField.SpatialJetField.fastAdvection {P T : ℝ} [Fact (0 < P)] {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} {normal : EulerPacketProfileRecursion.VectorField} (N : VectorCoefficient T normal) (G : SpatialJetField P T J) (H : SpatialJetField P T K) : Field P T fun (z : EulerPacketPointJets.Domain) => ((EulerPacketPointJets.fastAdvection (normal z)) (J z)) (K z)

Fast advection as an element of Field P T (fun z => EulerPacketPointJets.fastAdvection (normal z) (J z) (K z)).

Equations

• EulerPacketCylinderField.SpatialJetField.fastAdvection N G H = (G.field.angularTransport H.field N.path ⋯ normal ⋯).congr ⋯

noncomputable def EulerPacketCylinderField.pressureGradient (p : EulerPacketProfileRecursion.ScalarField) : EulerPacketProfileRecursion.VectorField

The actual spatial pressure gradient encoded by the pressure-only jet.

Equations

• EulerPacketCylinderField.pressureGradient p z = (InnerProductSpace.toDual ℝ EulerSmoothLimit.Space).symm ((EulerPacketPointJets.pressureJet p z).2 ∘SL EulerPacketPointJets.spatialInjection)

noncomputable def EulerPacketCylinderField.Field.slowPressure {P T : ℝ} [Fact (0 < P)] {inverse : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T inverse) (p : EulerPacketProfileRecursion.ScalarField) (G : Field P T (pressureGradient p)) : Field P T fun (z : EulerPacketPointJets.Domain) => (EulerPacketPointJets.slowPressure (inverse z)) (EulerPacketPointJets.pressureJet p z)

Slow pressure, given by (A.adjoint.multiply G).congr (fun _ _ _ => rfl).

Equations

• EulerPacketCylinderField.Field.slowPressure A p G = (A.adjoint.multiply G).congr ⋯

noncomputable def EulerPacketCylinderField.Field.linearPart {P T : ℝ} [Fact (0 < P)] {strain : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T strain) {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (hT : 0 < T) (hd : TimeDerivative ⋯ G H) (s : Set ℝ) (hs : s = Set.Icc 0 T) : Field P T fun (z : EulerPacketPointJets.Domain) => (EulerPacketPointJets.linearPart (strain z)) (EulerPacketPointJets.slicedJet s raw z)

The linear time term uses a genuine L² time derivative of the old corrector.

Equations

• EulerPacketCylinderField.Field.linearPart A G H hT hd s hs = (H.add (A.multiply G)).congr ⋯