One literal profile-recursion step carries genuine path, time-derivative and locality witnesses.
noncomputable def
EulerPacketCylinderField.ProfileRegularity.step
{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 : EulerTransversePacketProvider.InitialData P D)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D I)
(hcorrector : O.curlCorrector = D.curlCorrector P)
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hp : 2 ≤ p)
(G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i))
:
ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.step O p a)
The prefix hypotheses are regularity of known fields, never equations for the new profile.
Equations
- One or more equations did not get rendered due to their size.