The pressure entry contains only actual space/angle derivatives used by the PDE.

Actual PDE jets on a closed time interval. Time derivatives are within the interval, while space and angle derivatives are ordinary Fréchet derivatives. No smooth extension across a time endpoint is assumed.

@[reducible, inline]

abbrev EulerPacketPointJets.SpatialDomain : Type

Spatial domain: an abbreviation for Space × ℝ.

Equations

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

def EulerPacketPointJets.joinDerivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : E) (D : SpatialDomain →L[ℝ] E) : Domain →L[ℝ] E

Join derivative, given by (ContinuousLinearMap.fst ℝ ℝ SpatialDomain).smulRight v + D.comp (ContinuousLinearMap.snd ℝ ℝ SpatialDomain).

Equations

• EulerPacketPointJets.joinDerivative v D = (ContinuousLinearMap.fst ℝ ℝ EulerPacketPointJets.SpatialDomain).smulRight v + D ∘SL ContinuousLinearMap.snd ℝ ℝ EulerPacketPointJets.SpatialDomain

theorem EulerPacketPointJets.joinDerivative_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : E) (D : SpatialDomain →L[ℝ] E) (h : Domain) : (joinDerivative v D) h = h.1 • v + D h.2

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

Sliced jet, given by (f z, joinDerivative (derivWithin (fun t => f (t,z.2)) s z.1) (fderiv ℝ (fun y => f (z.1,y)) z.2)).

Equations

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

theorem EulerPacketPointJets.slicedJet_time {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (f : Domain → E) (z : Domain) : (slicedJet s f z).2 timeDirection = derivWithin (fun (t : ℝ) => f (t, z.2)) s z.1

theorem EulerPacketPointJets.slicedJet_space {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (f : Domain → E) (z : Domain) (v : EulerSmoothLimit.Space) : (slicedJet s f z).2 (spatialInjection v) = (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => f (z.1, y)) z.2) (v, 0)

theorem EulerPacketPointJets.slicedJet_angle {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (f : Domain → E) (z : Domain) : (slicedJet s f z).2 angleDirection = (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => f (z.1, y)) z.2) (0, 1)

theorem EulerPacketPointJets.slicedJet_time_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (f : Domain → E) (z : Domain) (v : E) (hs : UniqueDiffWithinAt ℝ s z.1) (ht : HasDerivWithinAt (fun (t : ℝ) => f (t, z.2)) v s z.1) : (slicedJet s f z).2 timeDirection = v

The time entry is the derivative furnished by the actual interval evolution.

theorem EulerPacketPointJets.slicedJet_fieldSum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (M : ℕ) (κ : ℝ) (u : ℕ → Domain → E) (z : Domain) (hs : UniqueDiffWithinAt ℝ s z.1) (ht : ∀ n ≤ M, DifferentiableWithinAt ℝ (fun (t : ℝ) => u n (t, z.2)) s z.1) (hx : ∀ n ≤ M, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => u n (z.1, y)) z.2) : slicedJet s (fieldSum M κ u) z = EulerFiniteGrades.evaluate M κ fun (n : ℕ) => slicedJet s (u n) z

noncomputable def EulerPacketPointJets.pressureJet (p : Domain → ℝ) (z : Domain) : ScalarJet

The unused time slot is zero: no time derivative of the scalar potential is required.

Equations

• EulerPacketPointJets.pressureJet p z = (p z, EulerPacketPointJets.joinDerivative 0 (fderiv ℝ (fun (y : EulerPacketPointJets.SpatialDomain) => p (z.1, y)) z.2))

theorem EulerPacketPointJets.pressureJet_space (p : Domain → ℝ) (z : Domain) (v : EulerSmoothLimit.Space) : (pressureJet p z).2 (spatialInjection v) = (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2) (v, 0)

theorem EulerPacketPointJets.pressureJet_angle (p : Domain → ℝ) (z : Domain) : (pressureJet p z).2 angleDirection = (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2) (0, 1)

theorem EulerPacketPointJets.pressureJet_fieldSum (M : ℕ) (κ : ℝ) (p : ℕ → Domain → ℝ) (z : Domain) (hp : ∀ n ≤ M, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p n (z.1, y)) z.2) : pressureJet (fieldSum M κ p) z = EulerFiniteGrades.evaluate M κ fun (n : ℕ) => pressureJet (p n) z