All-grade bounds for the actual zero-history source recursion, initialized by the literal compact periodic wave. Every later forcing and solution is constructed, and the primary budget is discharged from its actual datum.
noncomputable def
EulerPacketTerminalDatum.forwardInitializedProfiles
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
:
Forward initialized profiles, given by sourceProfiles period M D (InitialData.zero period D) (initialData D δ hδ (α • ξ) hs).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.forwardInitializedProfileWitness
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(p : ℕ)
:
EulerPacketCylinderField.ProfileRegularity period M.T ⋯ D.support (forwardInitializedProfiles M D δ hδ ξ hs α p)
Forward initialized profile witness, given by sourceProfileWitness period M D hTime (InitialData.zero period D) (initialData D δ hδ (α • ξ) hs) p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.forwardInitialized_primary_budget
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
:
EulerPacketCylinderField.ProfileBudget
(EulerPacketCylinderField.forwardSourcePrimaryWitness period M D hTime (initialData D δ hδ (α • ξ) hs)) S L.R 1
theorem
EulerPacketTerminalDatum.forwardInitialized_profile_budgets
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
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 : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
(p : ℕ)
(hp : 1 ≤ p)
:
EulerPacketCylinderField.ProfileBudget (forwardInitializedProfileWitness M D hTime δ hδ ξ hs α p) S L.R p