Actual tail-grade and full residual fields for the source construction. The full residual is identified with its finite tail by the equations of the constructed mean and forward solutions.
The actual constructed source packet has only the uncancelled residual tail #
All profile regularity, tangency, and defining equations in the generic algebraic expansion are discharged by the actual recursive source solves.
theorem
EulerPacketCylinderField.source_residual_tail
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(A : SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(κ : ℝ)
(hκ : κ ≠ 0)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) κ ((sourceOperators P M D I).inverseFrame (↑t, x, θ))
((sourceOperators P M D I).strain (↑t, x, θ)) ((sourceOperators P M D I).normal (↑t, x, θ))
(EulerPacketPointJets.fieldSum (N + 1) κ
(EulerPacketProfileRecursion.assembledVelocity N (sourceProfiles P M D I Iprimary)))
(EulerPacketPointJets.fieldSum (N + 1) κ
(EulerPacketProfileRecursion.assembledPressure N (sourceProfiles P M D I Iprimary)))
(↑t, x, θ) = ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3),
κ ^ n • EulerPacketProfileRecursion.recursiveGrade (sourceOperators P M D I) N (sourceProfiles P M D I Iprimary)
(↑t, x, θ) n
noncomputable def
EulerPacketCylinderField.sourceTailGradeField
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(N n : ℕ)
(hn : N + 1 ≤ n)
:
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
EulerPacketProfileRecursion.recursiveGrade (sourceOperators P M D I) N (sourceProfiles P M D I Iprimary) z n
Source tail grade field, constructed using ProfileRegularity.tailGradeField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceLiteralTailGradeField
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(N n : ℕ)
(hn : N + 1 ≤ n)
:
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
EulerPacketPointJets.slicedMomentumGrade (Set.Icc 0 M.T) (N + 1) ((sourceOperators P M D I).inverseFrame z)
((sourceOperators P M D I).strain z) ((sourceOperators P M D I).normal z)
(EulerPacketProfileRecursion.assembledVelocity N (sourceProfiles P M D I Iprimary))
(EulerPacketProfileRecursion.assembledPressure N (sourceProfiles P M D I Iprimary)) z n
Source literal tail grade field, constructed using
ProfileRegularity.literalTailGradeField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.sourceLiteralTailGradeField_path
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(N n : ℕ)
(hn : N + 1 ≤ n)
:
(sourceLiteralTailGradeField P M D hT I Iprimary N n hn).path = (sourceTailGradeField P M D hT I Iprimary N n hn).path
noncomputable def
EulerPacketCylinderField.sourceTailSumField
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(N : ℕ)
(κ : ℝ)
:
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
∑ n ∈ Finset.Ico (N + 1) (2 * N + 3),
κ ^ n • EulerPacketProfileRecursion.recursiveGrade (sourceOperators P M D I) N (sourceProfiles P M D I Iprimary) z n
Source tail sum field, constructed using ProfileRegularity.tailSumField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceResidualField
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(Cagree : SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(κ : ℝ)
(hκ : κ ≠ 0)
:
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) κ ((sourceOperators P M D I).inverseFrame z)
((sourceOperators P M D I).strain z) ((sourceOperators P M D I).normal z)
(EulerPacketPointJets.fieldSum (N + 1) κ
(EulerPacketProfileRecursion.assembledVelocity N (sourceProfiles P M D I Iprimary)))
(EulerPacketPointJets.fieldSum (N + 1) κ
(EulerPacketProfileRecursion.assembledPressure N (sourceProfiles P M D I Iprimary)))
z
Source residual field, given by (sourceTailSumField P M D hT I Iprimary N κ).congr (source_residual_tail P M D hT I Iprimary Cagree N hN κ hκ).
Equations
- EulerPacketCylinderField.sourceResidualField P M D hT I Iprimary Cagree N hN κ hκ = (EulerPacketCylinderField.sourceTailSumField P M D hT I Iprimary N κ).congr ⋯