The actual sliced momentum coefficient equals the tail decomposition using only finite velocity regularity. No regularity of the lower scalar pressures is needed, because their coefficients are already outside the tail support.

theorem EulerPacketProfileRecursion.slicedJet_assembledVelocity_finite (O : Operators) (N : ℕ) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) (hA : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).high z) (hB : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).mean z) (hC : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).corrector z) (i : ℕ) : EulerPacketPointJets.slicedJet O.interval (assembledVelocity N a i) z = assembledJets O N a z i

theorem EulerPacketProfileRecursion.slicedMomentumGrade_tail_eq_recursive (O : Operators) (N n : ℕ) (hn : N + 1 ≤ n) (a : ℕ → Profile) (z : EulerPacketPointJets.Domain) (hA : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).high z) (hB : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).mean z) (hC : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).corrector z) : EulerPacketPointJets.slicedMomentumGrade O.interval (N + 1) (O.inverseFrame z) (O.strain z) (O.normal z) (assembledVelocity N a) (assembledPressure N a) z n = recursiveGrade O N a z n

theorem EulerPacketProfileRecursion.slicedMomentumGrade_tail (O : Operators) (N n : ℕ) (hn : N + 1 ≤ n) (a : ℕ → Profile) (ha : a 0 = 0) (z : EulerPacketPointJets.Domain) (hA : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).high z) (hB : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).mean z) (hC : ∀ i ≤ N, EulerPacketPointJets.SliceDifferentiable O.interval (a i).corrector z) : EulerPacketPointJets.slicedMomentumGrade O.interval (N + 1) (O.inverseFrame z) (O.strain z) (O.normal z) (assembledVelocity N a) (assembledPressure N a) z n = (if n = N + 1 then (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (a N).corrector z) + (EulerPacketPointJets.slowPressure (O.inverseFrame z)) (EulerPacketPointJets.pressureJet (a N).highPressure z) else 0) + EulerPacketPointJets.nonlinearGrade (N + 1) n (O.inverseFrame z) (O.normal z) (knownJets O (N + 1) a z)

noncomputable def EulerPacketCylinderField.ProfileRegularity.literalTailGradeField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {S : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ S (a i)) (C : CoefficientData P T O) (ha : a 0 = 0) (n : ℕ) (hn : N + 1 ≤ n) : Field P T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.slicedMomentumGrade O.interval (N + 1) (O.inverseFrame z) (O.strain z) (O.normal z) (EulerPacketProfileRecursion.assembledVelocity N a) (EulerPacketProfileRecursion.assembledPressure N a) z n

Literal tail grade field used in packet residual tail actual.

Equations

• EulerPacketCylinderField.ProfileRegularity.literalTailGradeField hT G C ha n hn = (EulerPacketCylinderField.ProfileRegularity.tailGradeField hT G C ha n hn).congr ⋯

theorem EulerPacketCylinderField.ProfileRegularity.literalTailGradeField_path {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {S : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ S (a i)) (C : CoefficientData P T O) (ha : a 0 = 0) (n : ℕ) (hn : N + 1 ≤ n) : (literalTailGradeField hT G C ha n hn).path = (tailGradeField hT G C ha n hn).path