The initialized zero-history finite packet supplies the actual all-order data of the correction equation, with its derived word estimates.

Actual finite velocity, normal drift and residual estimates for the zero-history recursion initialized by the literal compact periodic wave.

noncomputable def EulerPacketTerminalDatum.forwardInitializedPacketField (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) (α : ℝ) (N : ℕ) (κ : ℝ) : EulerPacketCylinderField.Field period M.T fun (z : EulerPacketPointJets.Domain) => ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).inverseFrame z) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.sourceProfiles period M D (EulerTransversePacketProvider.InitialData.zero period D) (initialData D δ hδ (α • ξ) hs))) z)

Forward initialized packet field, given by sourcePacketPullbackField period M D hTime (InitialData.zero period D) (initialData D δ hδ (α • ξ) hs) N κ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketTerminalDatum.forwardInitializedResidualField (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) (α : ℝ) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (κ : ℝ) (hκ : κ ≠ 0) : EulerPacketCylinderField.Field period M.T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) κ ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).inverseFrame z) ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).strain z) ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).normal z) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.sourceProfiles period M D (EulerTransversePacketProvider.InitialData.zero period D) (initialData D δ hδ (α • ξ) hs)))) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledPressure N (EulerPacketCylinderField.sourceProfiles period M D (EulerTransversePacketProvider.InitialData.zero period D) (initialData D δ hδ (α • ξ) hs)))) z

Forward initialized residual field, given by sourceResidualField period M D hTime (InitialData.zero period D) (initialData D δ hδ (α • ξ) hs) Cagree N hN κ hκ.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketTerminalDatum.forwardInitializedPacket_normalized_bound (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : ((forwardInitializedPacketField M D hTime δ hδ ξ hs α N k⁻¹).smul k).WordBound 6 (4 * L.R) (BC.multiplierCost * (EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 1 + EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 2 + 1)) 0

theorem EulerPacketTerminalDatum.forwardInitializedPacket_normal_bound (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : (((forwardInitializedPacketField M D hTime δ hδ ξ hs α N k⁻¹).smul k).map (EulerPacketCylinderField.normalComponentMap D.m₀)).WordBound 6 (4 * L.R) (BC.multiplierCost * (EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 2 + 2) / k) 0

theorem EulerPacketTerminalDatum.forwardInitializedResidual_normalized_bound (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) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k X : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) (hcoef : BC.multiplierCost ≤ k ^ (1 / 100)) (hX : 6 ≤ X) (hNX : X - 1 ≤ ↑N) : (((EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D) hTime).inverse.multiply (forwardInitializedResidualField M D hTime δ hδ ξ hs α Cagree N hN k⁻¹ ⋯)).smul k).WordBound 6 (4 * L.R) (Real.exp (-(7 / 10) * X * Real.log k)) 0

noncomputable def EulerPacketTerminalDatum.forwardInitializedNormalizedField (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) (α : ℝ) (N : ℕ) (k : ℝ) : EulerPacketCylinderField.Field period D.T (k • fun (z : EulerPacketPointJets.Domain) => ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).inverseFrame z) (EulerPacketPointJets.fieldSum (N + 1) k⁻¹ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.sourceProfiles period M D (EulerTransversePacketProvider.InitialData.zero period D) (initialData D δ hδ (α • ξ) hs))) z))

Forward initialized normalized field, given by ((forwardInitializedPacketField M D hTime δ hδ ξ hs α N k⁻¹).smul k).changeTime hTime.

Equations

• EulerPacketTerminalDatum.forwardInitializedNormalizedField M D hTime δ hδ ξ hs α N k = ((EulerPacketTerminalDatum.forwardInitializedPacketField M D hTime δ hδ ξ hs α N k⁻¹).smul k).changeTime hTime

noncomputable def EulerPacketTerminalDatum.forwardInitializedNormalizedResidualField (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) (α : ℝ) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) : EulerPacketCylinderField.Field period D.T (k • fun (z : EulerPacketPointJets.Domain) => ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).inverseFrame z) (EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) k⁻¹ ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).inverseFrame z) ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).strain z) ((EulerPacketCylinderField.sourceOperators period M D (EulerTransversePacketProvider.InitialData.zero period D)).normal z) (EulerPacketPointJets.fieldSum (N + 1) k⁻¹ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.sourceProfiles period M D (EulerTransversePacketProvider.InitialData.zero period D) (initialData D δ hδ (α • ξ) hs)))) (EulerPacketPointJets.fieldSum (N + 1) k⁻¹ (EulerPacketProfileRecursion.assembledPressure N (EulerPacketCylinderField.sourceProfiles period M D (EulerTransversePacketProvider.InitialData.zero period D) (initialData D δ hδ (α • ξ) hs)))) z))

Forward initialized normalized residual field used in packet forward initialized correction data.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketTerminalDatum.forwardInitializedCorrectionData (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) (α : ℝ) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) : EulerAllOrderCorrectionData.Data period D.T

Forward initialized correction data, constructed using EulerPacketCorrectionCoefficients.correctionDataOfFields.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketTerminalDatum.forwardInitializedNormalizedField_bound (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : (forwardInitializedNormalizedField M D hTime δ hδ ξ hs α N k).WordBound 6 (4 * L.R) (EulerPacketCorrectionConstants.velocity L.R S.H0 BC.multiplierCost) 0

theorem EulerPacketTerminalDatum.forwardInitializedNormalizedField_normal_bound (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : ((forwardInitializedNormalizedField M D hTime δ hδ ξ hs α N k).map (EulerPacketCylinderField.normalComponentMap D.m₀)).WordBound 6 (4 * L.R) (EulerPacketCorrectionConstants.normal L.R S.H0 BC.multiplierCost / k) 0

theorem EulerPacketTerminalDatum.forwardInitializedNormalizedResidualField_bound (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) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k X : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) (hcoef : BC.multiplierCost ≤ k ^ (1 / 100)) (hX : 6 ≤ X) (hNX : X - 1 ≤ ↑N) : (forwardInitializedNormalizedResidualField M D hTime δ hδ ξ hs α Cagree N hN k hk).WordBound 6 (4 * L.R) (Real.exp (-(7 / 10) * X * Real.log k)) 0