The recursive mean forcing is sent to the actual source inverse, then returned as a true cylinder field.
noncomputable def
EulerPacketCylinderField.PrefixFields.meanForcing
{P : ℝ}
[Fact (0 < P)]
(D : EulerMeanPacketProvider.Data)
{O : EulerPacketProfileRecursion.Operators}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P D.T p a)
(C : CoefficientData P D.T O)
(hp : 1 ≤ p)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P D.T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct)
(pressure : Field P D.T (pressureGradient (a (p - 1)).highPressure))
:
Mean forcing as an element of EulerMeanPacketProvider.Forcing D (EulerPacketProfileRecursion.meanForce O p a).
Equations
- EulerPacketCylinderField.PrefixFields.meanForcing D F C hp Ct hCt pressure = ⋯.mpr (EulerPacketCylinderField.Field.meanForcing D (F.knownForce C hp ⋯ Ct hCt pressure))
Instances For
noncomputable def
EulerPacketCylinderField.PrefixFields.meanResultField
{P : ℝ}
[Fact (0 < P)]
(D : EulerMeanPacketProvider.Data)
{O : EulerPacketProfileRecursion.Operators}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P D.T p a)
(C : CoefficientData P D.T O)
(hp : 1 ≤ p)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P D.T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct)
(pressure : Field P D.T (pressureGradient (a (p - 1)).highPressure))
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve D)
:
Field P D.T (EulerPacketProfileRecursion.meanResult O p a).1
Mean result field as an element of Field P D.T (meanResult O p a).1.
Equations
- EulerPacketCylinderField.PrefixFields.meanResultField D F C hp Ct hCt pressure hmean = (EulerMeanPacketProvider.meanSolveCylinderField P D (EulerPacketProfileRecursion.meanForce O p a) ⋯).congr ⋯
Instances For
theorem
EulerPacketCylinderField.PrefixFields.meanResult_angleIndependent
{P : ℝ}
[Fact (0 < P)]
(D : EulerMeanPacketProvider.Data)
{O : EulerPacketProfileRecursion.Operators}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P D.T p a)
(C : CoefficientData P D.T O)
(hp : 1 ≤ p)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P D.T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct)
(pressure : Field P D.T (pressureGradient (a (p - 1)).highPressure))
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
noncomputable def
EulerPacketCylinderField.PrefixFields.actualHighForce
{P : ℝ}
[Fact (0 < P)]
(D : EulerMeanPacketProvider.Data)
{O : EulerPacketProfileRecursion.Operators}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P D.T p a)
(C : CoefficientData P D.T O)
(hp : 2 ≤ p)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P D.T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct)
(pressure : Field P D.T (pressureGradient (a (p - 1)).highPressure))
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve D)
:
Field P D.T (EulerPacketProfileRecursion.highForce O p a)
The new mean in this witness is obtained from the constructed source mean inverse.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.PrefixFields.actualHighForce_mean_zero
{P : ℝ}
[Fact (0 < P)]
(D : EulerMeanPacketProvider.Data)
{O : EulerPacketProfileRecursion.Operators}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P D.T p a)
(C : CoefficientData P D.T O)
(hp : 2 ≤ p)
{correctorT : EulerPacketProfileRecursion.VectorField}
(Ct : Field P D.T correctorT)
(hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct)
(pressure : Field P D.T (pressureGradient (a (p - 1)).highPressure))
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
: