Literal known-grade jet data are reconstructed from only the genuine prefix fields.

structure EulerPacketCylinderField.PrefixFields (P T : ℝ) [Fact (0 < P)] (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) : Type

Prefix fields data, collecting high, mean, corrector.

• high (i : ℕ) : i < p → Field P T (a i).high

  High-frequency field of PrefixFields, of type ∀ i, i < p → Field P T (a i).high.

• mean (i : ℕ) : i < p → Field P T (a i).mean

  Mean field of PrefixFields, of type ∀ i, i < p → Field P T (a i).mean.

• corrector (i : ℕ) : i < p → Field P T (a i).corrector

  Correction field of PrefixFields, of type ∀ i, i < p → Field P T (a i).corrector.

noncomputable def EulerPacketCylinderField.PrefixFields.knownJet {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (O : EulerPacketProfileRecursion.Operators) (hp : 1 ≤ p) (i : ℕ) : SpatialJetField P T fun (z : EulerPacketPointJets.Domain) => EulerPacketProfileRecursion.knownJets O p a z i

No grade at or above p is used to obtain the spatial part of the known jets.

Equations

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