The linear and bilinear packet operators on actual space-time value/derivative jets.

@[reducible, inline]

abbrev EulerPacketPointJets.Domain : Type

Domain: an abbreviation for ℝ × (Space × ℝ).

Equations

• EulerPacketPointJets.Domain = (ℝ × EulerSmoothLimit.Space × ℝ)

@[reducible, inline]

abbrev EulerPacketPointJets.Jet (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type u_1

Jet: an abbreviation for E × (Domain →L[ℝ] E).

Equations

• EulerPacketPointJets.Jet E = (E × (EulerPacketPointJets.Domain →L[ℝ] E))

@[reducible, inline]

abbrev EulerPacketPointJets.VectorJet : Type

Vector jet: an abbreviation for Jet Space.

Equations

• EulerPacketPointJets.VectorJet = EulerPacketPointJets.Jet EulerSmoothLimit.Space

@[reducible, inline]

abbrev EulerPacketPointJets.ScalarJet : Type

Scalar jet: an abbreviation for Jet ℝ.

Equations

• EulerPacketPointJets.ScalarJet = EulerPacketPointJets.Jet ℝ

def EulerPacketPointJets.timeDirection : Domain

Time direction, given by (1, (0, 0)).

Equations

• EulerPacketPointJets.timeDirection = (1, 0, 0)

def EulerPacketPointJets.angleDirection : Domain

Angle direction, given by (0, (0, 1)).

Equations

• EulerPacketPointJets.angleDirection = (0, 0, 1)

def EulerPacketPointJets.spatialInjection : EulerSmoothLimit.Space →L[ℝ] Domain

Spatial injection, given by (0 : Space →L[ℝ] ℝ).prod ((ContinuousLinearMap.id ℝ Space).prod (0 : Space →L[ℝ] ℝ)).

Equations

• EulerPacketPointJets.spatialInjection = ContinuousLinearMap.prod 0 ((ContinuousLinearMap.id ℝ EulerSmoothLimit.Space).prod 0)

noncomputable def EulerPacketPointJets.jet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : Domain → E) (z : Domain) : Jet E

Jet, given by (f z, fderiv ℝ f z).

Equations

• EulerPacketPointJets.jet f z = (f z, fderiv ℝ f z)

noncomputable def EulerPacketPointJets.linearPart (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : VectorJet →ₗ[ℝ] EulerSmoothLimit.Space

Linear part, bundling toFun, map_add, map_smul.

Equations

• EulerPacketPointJets.linearPart M = { toFun := fun (J : EulerPacketPointJets.VectorJet) => J.2 EulerPacketPointJets.timeDirection + M J.1, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerPacketPointJets.slowPressure (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : ScalarJet →ₗ[ℝ] EulerSmoothLimit.Space

Slow pressure, bundling toFun, map_add, map_smul.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketPointJets.fastPressure (m : EulerSmoothLimit.Space) : ScalarJet →ₗ[ℝ] EulerSmoothLimit.Space

Fast pressure, bundling toFun, map_add, map_smul.

Equations

• EulerPacketPointJets.fastPressure m = { toFun := fun (J : EulerPacketPointJets.ScalarJet) => J.2 EulerPacketPointJets.angleDirection • m, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerPacketPointJets.slowAdvection (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : VectorJet →ₗ[ℝ] VectorJet →ₗ[ℝ] EulerSmoothLimit.Space

Slow advection, bundling toFun, map_add, map_smul, map_add and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketPointJets.fastAdvection (m : EulerSmoothLimit.Space) : VectorJet →ₗ[ℝ] VectorJet →ₗ[ℝ] EulerSmoothLimit.Space

Fast advection, bundling toFun, map_add, map_smul, map_add and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

def EulerPacketPointJets.fieldSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℕ) (κ : ℝ) (u : ℕ → Domain → E) (z : Domain) : E

Field sum, given by evaluate M κ (fun n => u n z).

Equations

• EulerPacketPointJets.fieldSum M κ u z = EulerFiniteGrades.evaluate M κ fun (n : ℕ) => u n z

theorem EulerPacketPointJets.jet_fieldSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (M : ℕ) (κ : ℝ) (u : ℕ → Domain → E) (z : Domain) (hu : ∀ n ≤ M, DifferentiableAt ℝ (u n) z) : jet (fieldSum M κ u) z = EulerFiniteGrades.evaluate M κ fun (n : ℕ) => jet (u n) z

Taking the actual first jet commutes with a finite packet sum.

noncomputable def EulerPacketPointJets.momentumResidual (κ : ℝ) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : Domain → EulerSmoothLimit.Space) (p : Domain → ℝ) (z : Domain) : EulerSmoothLimit.Space

This is the literal normalized momentum expression evaluated through its true first derivatives.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketPointJets.momentumResidual_formula (κ : ℝ) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : Domain → EulerSmoothLimit.Space) (p : Domain → ℝ) (z : Domain) : momentumResidual κ FInv M m u p z = (fderiv ℝ u z) timeDirection + M (u z) + (ContinuousLinearMap.adjoint FInv) ((InnerProductSpace.toDual ℝ EulerSmoothLimit.Space).symm (fderiv ℝ p z ∘SL spatialInjection)) + κ⁻¹ • (fderiv ℝ p z) angleDirection • m + (fderiv ℝ u z) (spatialInjection (FInv (u z))) + κ⁻¹ • inner ℝ m (u z) • (fderiv ℝ u z) angleDirection