The actual initialized recursion has both mean and angular pressure budgets at every grade. All bounds are derived from the source solvers.
The angular derivative of the actual recursive high pressure retains the unit grade budget. This is derived from the same source solve used by the velocity recursion.
theorem
EulerPacketCylinderField.ProfileBudget.angularPressure_step_exists
{P : ℝ}
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards N)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(BC : CoefficientBudget C)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hhigh : O.highSolve = EulerTransversePacketJoin.highSolve τ hτ hτT B)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hp : 2 ≤ p)
(G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i))
(hG : ∀ (i : ℕ) (hi : i < p), 1 ≤ i → ProfileBudget (G i hi) S L.R i)
(hc₀ : (a 0).corrector = 0)
(hB₁ : (a 1).mean = 0)
(hA :
∀ i < p,
∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ),
inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0)
(c : ℝ)
(hc : 0 < c)
(hprofile : timeProfileChange (S.high p) hTime = c • L.fullProfile)
:
∃ (Q :
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
(EulerPacketPointJets.pressureJet (EulerPacketProfileRecursion.step O p a).highPressure z).2
EulerPacketPointJets.angleDirection • D.m₀),
(Q.normalized ⋯ (S.high p) ⋯).WordBound 6 L.R 1 (EulerPacketShiftArithmetic.highShift p)
structure
EulerPacketCylinderField.PressureBudget
(P T : ℝ)
[Fact (0 < P)]
(hT : 0 ≤ T)
(m : EulerSmoothLimit.Space)
(a : EulerPacketProfileRecursion.Profile)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(p : ℕ)
:
Pressure budget data, collecting mean, angular, mean_bound, angular_bound.
- mean : Field P T (pressureGradient a.meanPressure)
Mean field of
PressureBudget, of typeField P T (pressureGradient a.meanPressure). - angular : Field P T fun (z : EulerPacketPointJets.Domain) => (EulerPacketPointJets.pressureJet a.highPressure z).2 EulerPacketPointJets.angleDirection • m
Angular of
PressureBudget, of typeField P T (fun z => (pressureJet a.highPressure z).2 angleDirection • m). - mean_bound : (self.mean.normalized hT (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)
- angular_bound : (self.angular.normalized hT (S.high p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift p)
Instances For
theorem
EulerPacketTerminalDatum.initializedPressureBudget_exists
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
(p : ℕ)
:
Nonempty
(EulerPacketCylinderField.PressureBudget period M.T ⋯ D.m₀ (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α p) S L.R p)