Qualitative admissibility of the actual source packet recursion #
The data are the prescribed coefficients, the common time interval and the initial transverse datum. Every profile and every later forcing witness is constructed; no prefix regularity hypothesis remains.
Actual homogeneous primary and recursively solved profiles #
The initial transverse datum and coefficient data determine every profile. Admissibility at all later grades follows from the genuine nonlinear paths, the source mean inverse and the source transverse inverse.
noncomputable def
EulerPacketCylinderField.constructedProfileWitness
{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)
{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 : ℕ)
:
ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.profiles O (homogeneousPrimary D Iprimary O) p)
Constructed profile witness, constructed using profileWitness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.constructedMeanForcing
{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)
{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 : ℕ)
(hp : 2 ≤ p)
:
Constructed mean forcing, constructed using profilesMeanForcing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.constructedHighForcing
{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)
{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 : ℕ)
(hp : 2 ≤ p)
:
EulerTransversePacketProvider.Forcing P D
(EulerPacketProfileRecursion.highForce O p (EulerPacketProfileRecursion.profiles O (homogeneousPrimary D Iprimary O)))
Constructed high forcing, constructed using profilesHighForcing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceProfiles
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
:
Source profiles, given by profiles (sourceOperators P M D I) (homogeneousPrimary D Iprimary (sourceOperators P M D I)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceProfileWitness
(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)
(p : ℕ)
:
ProfileRegularity P M.T ⋯ D.support (sourceProfiles P M D I Iprimary p)
Source profile witness, given by constructedProfileWitness M D hT I Iprimary (sourceCoefficientData P M D I hT) rfl rfl rfl p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceMeanForcing
(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)
(p : ℕ)
(hp : 2 ≤ p)
:
EulerMeanPacketProvider.Forcing M
(EulerPacketProfileRecursion.meanForce (sourceOperators P M D I) p (sourceProfiles P M D I Iprimary))
Source mean forcing, given by constructedMeanForcing M D hT I Iprimary (sourceCoefficientData P M D I hT) rfl rfl rfl p hp.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.sourceHighForcing
(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)
(p : ℕ)
(hp : 2 ≤ p)
:
EulerTransversePacketProvider.Forcing P D
(EulerPacketProfileRecursion.highForce (sourceOperators P M D I) p (sourceProfiles P M D I Iprimary))
Source high forcing, given by constructedHighForcing M D hT I Iprimary (sourceCoefficientData P M D I hT) rfl rfl rfl p hp.
Equations
- One or more equations did not get rendered due to their size.