The initial profile and the zero/first grades of the actual recursive packet.

def EulerPacketProfileRecursion.primaryProfile (O : Operators) (A : VectorField) (π : ScalarField) : Profile

Primary profile, given by ⟨A,0,O.curlCorrector A,π,0⟩.

Equations

• EulerPacketProfileRecursion.primaryProfile O A π = { high := A, mean := 0, corrector := O.curlCorrector A, highPressure := π, meanPressure := 0 }

theorem EulerPacketProfileRecursion.assembledJets_zero (O : Operators) (N : ℕ) (a : ℕ → Profile) (ha : a 0 = 0) (z : EulerPacketPointJets.Domain) : assembledJets O N a z 0 = 0

theorem EulerPacketProfileRecursion.pressureJets_zero (N : ℕ) (a : ℕ → Profile) (ha : a 0 = 0) (z : EulerPacketPointJets.Domain) : pressureJets N a z 0 = 0

theorem EulerPacketProfileRecursion.recursiveGrade_zero (O : Operators) (primary : Profile) (N : ℕ) (z : EulerPacketPointJets.Domain) (hqθ : ∀ i ≤ N, (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet (profiles O primary i).meanPressure z) = 0) : recursiveGrade O N (profiles O primary) z 0 = 0

theorem EulerPacketProfileRecursion.nonlinearGrade_one (M : ℕ) (hM : 2 ≤ M) (FInv : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → EulerPacketPointJets.VectorJet) (hu0 : u 0 = 0) (htan : inner ℝ m (u 1).1 = 0) : EulerPacketPointJets.nonlinearGrade M 1 FInv m u = 0

theorem EulerPacketProfileRecursion.recursiveGrade_one (O : Operators) (A : VectorField) (π : ScalarField) (N : ℕ) (hN : 1 ≤ N) (z : EulerPacketPointJets.Domain) (hqθ : ∀ i ≤ N, (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet (profiles O (primaryProfile O A π) i).meanPressure z) = 0) (htan : inner ℝ (O.normal z) (A z) = 0) (hlinear : (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval A z) + (EulerPacketPointJets.fastPressure (O.normal z)) (EulerPacketPointJets.pressureJet π z) = 0) : recursiveGrade O N (profiles O (primaryProfile O A π)) z 1 = 0