Literal spatial parts of the packet jets

The nonlinear terms use the value and spatial/angular part of each jet. These are reconstructed from actual raw-path witnesses and finite sums.

structure EulerPacketCylinderField.SpatialJetField (P T : ℝ) [Fact (0 < P)] (J : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet) : Type

Spatial jet field data, collecting raw, field, value_eq, spatial_eq.

• raw : EulerPacketProfileRecursion.VectorField

  Raw of SpatialJetField, of type VectorField.

• field : Field P T self.raw

  Underlying field of SpatialJetField, of type Field P T raw.

• value_eq (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (J (↑t, x, θ)).1 = self.raw (↑t, x, θ)
• spatial_eq (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) (v : EulerPacketPointJets.SpatialDomain) : (J (↑t, x, θ)).2 (0, v) = (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => self.raw (↑t, y)) (x, θ)) v

def EulerPacketCylinderField.SpatialJetField.ofField {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (s : Set ℝ) (G : Field P T raw) : SpatialJetField P T (EulerPacketPointJets.slicedJet s raw)

Of field, bundling raw, field, value_eq, spatial_eq.

Equations

• EulerPacketCylinderField.SpatialJetField.ofField s G = { raw := raw, field := G, value_eq := ⋯, spatial_eq := ⋯ }

noncomputable def EulerPacketCylinderField.SpatialJetField.zero (P T : ℝ) [Fact (0 < P)] : SpatialJetField P T 0

Zero, bundling raw, field, value_eq, spatial_eq.

Equations

• EulerPacketCylinderField.SpatialJetField.zero P T = { raw := 0, field := EulerPacketCylinderField.Field.zero P T, value_eq := ⋯, spatial_eq := ⋯ }

def EulerPacketCylinderField.SpatialJetField.congr {P T : ℝ} [Fact (0 < P)] {J J' : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), J' (↑t, x, θ) = J (↑t, x, θ)) : SpatialJetField P T J'

Congr, bundling raw, field, value_eq, spatial_eq.

Equations

• G.congr he = { raw := G.raw, field := G.field, value_eq := ⋯, spatial_eq := ⋯ }

noncomputable def EulerPacketCylinderField.SpatialJetField.add {P T : ℝ} [Fact (0 < P)] {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (H : SpatialJetField P T K) : SpatialJetField P T (J + K)

Add, bundling raw, field, value_eq, spatial_eq and the required compatibility proofs.

Equations

• G.add H = { raw := G.raw + H.raw, field := G.field.add H.field, value_eq := ⋯, spatial_eq := ⋯ }