The literal initialized packet supplies a complete drift-aware all-order correction budget, from fixed source data and explicit scalar frequency guards. No solution or energy estimate is assumed.
Actual finite-order correction budgets for the initialized packet. All coefficient and field bounds are supplied by the checked constructions.
Cutoff-independent background, derivative, drift and residual budgets for the actual initialized correction data.
theorem
EulerPacketTerminalDatum.initializedCorrection_background
(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)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(s Q : ℕ)
(hQ : Q + 6 ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(hsmall : ρ * (4 * L.R) ≤ 1 / 2)
(t : ↑(Set.Icc 0 D.T))
:
EulerSobolevGevreyOperators.weightedNorm period 6 Q ρ
(((initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).approximation.realization s) t) ≤ 2 * EulerPacketCorrectionConstants.velocity L.R S.H0 BC.multiplierCost
theorem
EulerPacketTerminalDatum.initializedCorrection_background_derivative
(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)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(s Q : ℕ)
(hQ : Q + 6 ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(hsmall : ρ * (4 * L.R) ≤ 1 / 2)
(t : ↑(Set.Icc 0 D.T))
:
∑ i : Fin 4,
EulerSobolevGevreyOperators.weightedNorm period 6 Q ρ
((EulerCylinderSobolevSpace.derivativeOperator period s i)
(((initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).approximation.realization
(s + 1))
t)) ≤ 12 * EulerPacketCorrectionConstants.velocity L.R S.H0 BC.multiplierCost * (4 * L.R)
theorem
EulerPacketTerminalDatum.initializedCorrection_drift
(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)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(s Q : ℕ)
(hQ : Q + 6 ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(hsmall : ρ * (4 * L.R) ≤ 1 / 2)
(t : ↑(Set.Icc 0 D.T))
:
EulerSobolevDriftNorm.weightedDriftNorm period 6 Q ρ
(EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents k⁻¹ D.m₀))
(((initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).approximation.realization s) t) ≤ EulerPacketCorrectionConstants.drift L.R S.H0 BC.multiplierCost / k
theorem
EulerPacketTerminalDatum.initializedCorrection_residual
(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)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(X : ℝ)
(hcoef : BC.multiplierCost ≤ k ^ (1 / 100))
(hX : 6 ≤ X)
(hNX : X - 1 ≤ ↑N)
(s Q : ℕ)
(hQ : Q + 6 ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(hsmall : ρ * (4 * L.R) ≤ 1 / 2)
(t : ↑(Set.Icc 0 D.T))
:
EulerSobolevGevreyOperators.weightedNorm period 6 Q ρ
(((initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).residual.realization s) t) ≤ 2 * Real.exp (-(7 / 10) * X * Real.log k)
noncomputable def
EulerPacketTerminalDatum.initializedMetricBudget
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(q : ℕ)
:
EulerCorrectionEnergyData.MetricBudget period D.T ⋯
(EulerAllOrderCorrectionData.Data.atOrder period
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk) (q + 1))
Initialized metric budget, constructed using sourceMetricBudgetOfFields.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedSpatialBudget
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(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)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(X : ℝ)
(hcoef : BC.multiplierCost ≤ k ^ (1 / 100))
(hX : 6 ≤ X)
(hNX : X - 1 ≤ ↑N)
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D period)
(ρ : C(↑(Set.Icc 0 D.T), ℝ))
(hρ : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < ρ t)
(hpacket : ∀ (t : ↑(Set.Icc 0 D.T)), ρ t * (4 * L.R) ≤ 1 / 2)
(hpressure : ∀ (t : ↑(Set.Icc 0 D.T)), 4 * Kc.M * (ρ t * Kc.Rc) ≤ 1)
(q : ℕ)
(hq : 6 ≤ q)
:
EulerCorrectionEnergyData.SpatialBudget period ⋯
(EulerAllOrderCorrectionData.Data.atOrder period
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk) (q + 1 + 1))
(q - 4) ρ
All four field estimates and all coefficient estimates are actual properties of the initialized source data at this finite Sobolev order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedDriftBudget
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(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)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(X : ℝ)
(hcoef : BC.multiplierCost ≤ k ^ (1 / 100))
(hX : 6 ≤ X)
(hNX : X - 1 ≤ ↑N)
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D period)
(ρ : C(↑(Set.Icc 0 D.T), ℝ))
(hρ : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < ρ t)
(hpacket : ∀ (t : ↑(Set.Icc 0 D.T)), ρ t * (4 * L.R) ≤ 1 / 2)
(hpressure : ∀ (t : ↑(Set.Icc 0 D.T)), 4 * Kc.M * (ρ t * Kc.Rc) ≤ 1)
(q : ℕ)
(hq : 6 ≤ q)
:
EulerDriftCorrectionBudget.Budget period ⋯
(EulerAllOrderCorrectionData.Data.atOrder period
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk) (q + 1 + 1))
(q - 4) ρ
The small drift envelope is kept separate from the full background.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedDriftBudget_growth
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(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)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(X : ℝ)
(hcoef : BC.multiplierCost ≤ k ^ (1 / 100))
(hX : 6 ≤ X)
(hNX : X - 1 ≤ ↑N)
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D period)
(ρ : C(↑(Set.Icc 0 D.T), ℝ))
(hρ : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < ρ t)
(hpacket : ∀ (t : ↑(Set.Icc 0 D.T)), ρ t * (4 * L.R) ≤ 1 / 2)
(hpressure : ∀ (t : ↑(Set.Icc 0 D.T)), 4 * Kc.M * (ρ t * Kc.Rc) ≤ 1)
(q : ℕ)
(hq : 6 ≤ q)
:
EulerCorrectionEnergyMajorants.combinedConstant period
(initializedDriftBudget M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk L H NB W LM WM BC hRc hcost hδ1 hα hR WP S
hgrowth hbase X hcoef hX hNX Kc ρ hρ hpacket hpressure q hq).full
(EulerAllOrderCorrectionData.Data.metricBudget period
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk) ⋯
(initializedMetricBudget M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk 0) (q + 1)) = EulerPacketCorrectionCoefficients.growthCoefficient D period Kc
(2 * EulerPacketCorrectionConstants.velocity L.R S.H0 BC.multiplierCost)
(12 * EulerPacketCorrectionConstants.velocity L.R S.H0 BC.multiplierCost * (4 * L.R))
The initialized approximation satisfies the actual lifted divergence constraint whenever the source deformation is a volume-preserving Jacobian.
theorem
EulerPacketTerminalDatum.initializedPacketField_mem
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(κ : ℝ)
(t : ↑(Set.Icc 0 M.T))
(Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hΞ : ContDiff ℝ (↑⊤) Ξ)
(hF : ∀ (x : EulerSmoothLimit.Space), fderiv ℝ Ξ x = (D.F.field (EulerPacketCylinderField.sourceTime M D hTime t)) x)
(hdet :
∀ (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field (EulerPacketCylinderField.sourceTime M D hTime t)) x)) = 1)
:
(initializedPacketField M D hTime τ hτ hτT B δ hδ ξ hs α N κ).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ D.m₀
theorem
EulerPacketTerminalDatum.initializedCorrectionData_divergence
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Ξ : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hΞ : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (Ξ t))
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (Ξ t) x = (D.F.field t) x)
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
(t : ↑(Set.Icc 0 D.T))
:
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).approximation.field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period k⁻¹ D.m₀
noncomputable def
EulerPacketCorrectionConstants.growth
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(P : ℝ)
[Fact (0 < P)]
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P)
(R H C : ℝ)
:
Growth, given by growthCoefficient D P Kc (2*velocity R H C) (12*velocity R H C*(4*R)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCorrectionConstants.growth_pos
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(P : ℝ)
[Fact (0 < P)]
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P)
(R H C : ℝ)
(hR : 0 ≤ R)
(hC : 0 ≤ C)
:
noncomputable def
EulerPacketTerminalDatum.initializedAllOrderBudget
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(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)
(Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D period)
(k : ℝ)
(hk : 4 ≤ k)
(hX : 64 ≤ EulerPacketSourceFrequency.expansion k)
(hlog : 1 ≤ Real.log k)
(htail :
EulerPacketCoarseMajorant.tailPolynomialConstant L.R S.H0 BC.termCost ≤ EulerPacketSourceFrequency.smallPower k)
(hcoefficient : BC.multiplierCost ≤ EulerPacketSourceFrequency.smallPower k)
(hgrowthCost :
12 * EulerPacketCorrectionConstants.growth D period Kc L.R S.H0 BC.multiplierCost * D.T ≤ EulerPacketSourceFrequency.smallPower k)
(hdriftCost :
8 * EulerPacketCorrectionConstants.growth D period Kc L.R S.H0 BC.multiplierCost * D.T * EulerPacketCorrectionConstants.drift L.R S.H0 BC.multiplierCost / EulerPacketCorrectionScalar.initialRadius L.R Kc.M Kc.Rc ≤ EulerPacketSourceFrequency.smallPower k)
(herrorCost :
8 * EulerPacketCorrectionConstants.growth D period Kc L.R S.H0 BC.multiplierCost * D.T / EulerPacketCorrectionScalar.initialRadius L.R Kc.M Kc.Rc ≤ EulerPacketSourceFrequency.smallPower k)
(Ξ : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hΞ : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (Ξ t))
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (Ξ t) x = (D.F.field t) x)
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
:
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) ⋯ k hk)
Explicit scalar guards suffice because every analytic input to the all-order correction theorem is supplied by the constructed packet.
Equations
- One or more equations did not get rendered due to their size.