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

The literal terminal wave yields the actual finite packet, its small normal drift, and its exponentially small residual. Primary bounds and the primary equation are supplied by the construction itself.

The actual finite joined packet, including its terminal corrector, satisfies the lifted constraint.

Every joined high/corrector pair lies in the actual lifted solenoidal space.

noncomputable def EulerPacketCylinderField.joinedPairField (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (κ : ℝ) (p : ℕ) : Field P M.T fun (z : EulerPacketPointJets.Domain) => ((joinedSourceOperators P M D τ hτ hτT B).inverseFrame z) (κ ^ p • (joinedSourceProfiles P M D τ hτ hτT B primary p).high z + κ ^ (p + 1) • (joinedSourceProfiles P M D τ hτ hτT B primary p).corrector z)

Joined pair field used in packet joined source piola.

Equations

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

theorem EulerPacketCylinderField.joinedPairField_mem (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hc : primary.corrector = D.curlCorrector P primary.high) (hm : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, primary.high (↑t, x, θ) = 0) (ht : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (primary.high (↑t, x, θ)) = 0) (κ : ℝ) (p : ℕ) (hp : 1 ≤ p) (t : ↑(Set.Icc 0 M.T)) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hF : ∀ (x : EulerSmoothLimit.Space), fderiv ℝ Ξ x = (D.F.field (sourceTime M D hT t)) x) (hdet : ∀ (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field (sourceTime M D hT t)) x)) = 1) : (joinedPairField P M D hT τ hτ hτT B primary hprimary κ p).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ D.m₀

noncomputable def EulerPacketCylinderField.joinedPacketPullbackField (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (N : ℕ) (κ : ℝ) : Field P M.T fun (z : EulerPacketPointJets.Domain) => ((joinedSourceOperators P M D τ hτ hτT B).inverseFrame z) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N (joinedSourceProfiles P M D τ hτ hτT B primary)) z)

Joined packet pullback field used in packet joined source solenoidal.

Equations

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

theorem EulerPacketCylinderField.joinedPacketPullbackField_path (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (N : ℕ) (κ : ℝ) : (joinedPacketPullbackField P M D hT τ hτ hτT B primary hprimary N κ).path = ∑ i ∈ Finset.range N, ((joinedPairField P M D hT τ hτ hτT B primary hprimary κ (i + 1)).path + κ ^ (i + 1) • (joinedMeanPullbackField P M D hT τ hτ hτT B primary hprimary (i + 1)).path)

theorem EulerPacketCylinderField.joinedPacketPullbackField_mem (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hmean : primary.mean = 0) (hc : primary.corrector = D.curlCorrector P primary.high) (hm : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, primary.high (↑t, x, θ) = 0) (ht : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (primary.high (↑t, x, θ)) = 0) (A : 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 (sourceTime M D hT t)) x) (hdet : ∀ (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field (sourceTime M D hT t)) x)) = 1) : (joinedPacketPullbackField P M D hT τ hτ hτT B primary hprimary N κ).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ D.m₀

Actual tail-grade and full residual fields for the joined source construction.

The actual finite packet built by the complete joined inverse has precisely the uncancelled tail. The primary field and its homogeneous equation are inputs; every nonprimary regularity and equation is discharged by construction.

@[reducible, inline]

noncomputable abbrev EulerPacketCylinderField.joinedPrimaryProfiles (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : EulerPacketProfileRecursion.VectorField) (π : EulerPacketProfileRecursion.ScalarField) : ℕ → EulerPacketProfileRecursion.Profile

Joined primary profiles: an abbreviation for joinedSourceProfiles P M D τ hτ hτT B (primaryProfile (joinedSourceOperators P M D τ hτ hτT B) A π).

Equations

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

theorem EulerPacketCylinderField.joinedSource_residual_tail (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : EulerPacketProfileRecursion.VectorField) (π : EulerPacketProfileRecursion.ScalarField) (hprimary : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.primaryProfile (joinedSourceOperators P M D τ hτ hτT B) A π)) (hπ : ∀ (t : ↑(Set.Icc 0 M.T)), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => π (↑t, y)) (htan : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (A (↑t, x, θ)) = 0) (hprimaryEquation : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) A (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet π (↑t, x, θ)) = 0) (Cagree : SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (κ : ℝ) (hκ : κ ≠ 0) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) κ ((joinedSourceOperators P M D τ hτ hτT B).inverseFrame (↑t, x, θ)) ((joinedSourceOperators P M D τ hτ hτT B).strain (↑t, x, θ)) ((joinedSourceOperators P M D τ hτ hτT B).normal (↑t, x, θ)) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N (joinedPrimaryProfiles P M D τ hτ hτT B A π))) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledPressure N (joinedPrimaryProfiles P M D τ hτ hτT B A π))) (↑t, x, θ) = ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • EulerPacketProfileRecursion.recursiveGrade (joinedSourceOperators P M D τ hτ hτT B) N (joinedPrimaryProfiles P M D τ hτ hτT B A π) (↑t, x, θ) n

noncomputable def EulerPacketCylinderField.joinedTailGradeField (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (N n : ℕ) (hn : N + 1 ≤ n) : Field P M.T fun (z : EulerPacketPointJets.Domain) => EulerPacketProfileRecursion.recursiveGrade (joinedSourceOperators P M D τ hτ hτT B) N (joinedSourceProfiles P M D τ hτ hτT B primary) z n

Joined tail grade field, constructed using ProfileRegularity.tailGradeField.

Equations

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

noncomputable def EulerPacketCylinderField.joinedLiteralTailGradeField (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (N n : ℕ) (hn : N + 1 ≤ n) : Field P M.T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.slicedMomentumGrade (Set.Icc 0 M.T) (N + 1) ((joinedSourceOperators P M D τ hτ hτT B).inverseFrame z) ((joinedSourceOperators P M D τ hτ hτT B).strain z) ((joinedSourceOperators P M D τ hτ hτT B).normal z) (EulerPacketProfileRecursion.assembledVelocity N (joinedSourceProfiles P M D τ hτ hτT B primary)) (EulerPacketProfileRecursion.assembledPressure N (joinedSourceProfiles P M D τ hτ hτT B primary)) z n

Joined literal tail grade field, constructed using ProfileRegularity.literalTailGradeField.

Equations

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

theorem EulerPacketCylinderField.joinedLiteralTailGradeField_path (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (N n : ℕ) (hn : N + 1 ≤ n) : (joinedLiteralTailGradeField P M D hT τ hτ hτT B primary hprimary N n hn).path = (joinedTailGradeField P M D hT τ hτ hτT B primary hprimary N n hn).path

noncomputable def EulerPacketCylinderField.joinedTailSumField (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (N : ℕ) (κ : ℝ) : Field P M.T fun (z : EulerPacketPointJets.Domain) => ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • EulerPacketProfileRecursion.recursiveGrade (joinedSourceOperators P M D τ hτ hτT B) N (joinedSourceProfiles P M D τ hτ hτT B primary) z n

Joined tail sum field, constructed using ProfileRegularity.tailSumField.

Equations

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

noncomputable def EulerPacketCylinderField.joinedResidualField (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (A : EulerPacketProfileRecursion.VectorField) (π : EulerPacketProfileRecursion.ScalarField) (hprimary : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.primaryProfile (joinedSourceOperators P M D τ hτ hτT B) A π)) (hπ : ∀ (t : ↑(Set.Icc 0 M.T)), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => π (↑t, y)) (htan : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (A (↑t, x, θ)) = 0) (hprimaryEquation : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) A (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet π (↑t, x, θ)) = 0) (Cagree : SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (κ : ℝ) (hκ : κ ≠ 0) : Field P M.T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) κ ((joinedSourceOperators P M D τ hτ hτT B).inverseFrame z) ((joinedSourceOperators P M D τ hτ hτT B).strain z) ((joinedSourceOperators P M D τ hτ hτT B).normal z) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N (joinedPrimaryProfiles P M D τ hτ hτT B A π))) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledPressure N (joinedPrimaryProfiles P M D τ hτ hτT B A π))) z

Joined residual field used in packet joined residual fields.

Equations

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

Exponential residual bounds for the actual recursively solved joined packet.

theorem EulerPacketCylinderField.joinedTailSum_normalized_bound (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) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : CoefficientBudget (joinedSourceCoefficientData P M D τ hτ hτT B hTime)) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R) (hcost : BC.termCost ≤ L.R) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (α : ℝ) (hα : 0 < α) (hgrowth : timeProfileChange S.growth hTime = α • L.fullProfile) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hprimaryBudget : ProfileBudget hprimary S L.R 1) (hprimaryMean : primary.mean = 0) (hprimaryTangent : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (primary.high (↑t, x, θ)) = 0) (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) : (((joinedSourceCoefficientData P M D τ hτ hτT B hTime).inverse.multiply (joinedTailSumField P M D hTime τ hτ hτT B primary hprimary N k⁻¹)).smul k).WordBound 6 (4 * L.R) (Real.exp (-(7 / 10) * X * Real.log k)) 0

theorem EulerPacketCylinderField.joinedResidual_normalized_bound (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) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : CoefficientBudget (joinedSourceCoefficientData P M D τ hτ hτT B hTime)) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R) (hcost : BC.termCost ≤ L.R) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (α : ℝ) (hα : 0 < α) (hgrowth : timeProfileChange S.growth hTime = α • L.fullProfile) (A : EulerPacketProfileRecursion.VectorField) (π : EulerPacketProfileRecursion.ScalarField) (hp : ProfileRegularity P M.T ⋯ D.support (EulerPacketProfileRecursion.primaryProfile (joinedSourceOperators P M D τ hτ hτT B) A π)) (hpBudget : ProfileBudget hp S L.R 1) (hπ : ∀ (t : ↑(Set.Icc 0 M.T)), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => π (↑t, y)) (htan : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (A (↑t, x, θ)) = 0) (hpEquation : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) A (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet π (↑t, x, θ)) = 0) (Cagree : 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) : (((joinedSourceCoefficientData P M D τ hτ hτT B hTime).inverse.multiply (joinedResidualField P M D hTime τ hτ hτT B A π hp hπ htan hpEquation Cagree N hN k⁻¹ ⋯)).smul k).WordBound 6 (4 * L.R) (Real.exp (-(7 / 10) * X * Real.log k)) 0

All later-grade bounds and equations are proved by the actual source recursion. The remaining hypotheses are the fixed source and primary data, and the explicit scalar frequency guards.

The actual joined packet has a bounded normalized velocity and a small normal drift.

theorem EulerPacketCylinderField.joinedPacket_normalized_bound (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) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : CoefficientBudget (joinedSourceCoefficientData P M D τ hτ hτT B hTime)) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R) (hcost : BC.termCost ≤ L.R) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (α : ℝ) (hα : 0 < α) (hgrowth : timeProfileChange S.growth hTime = α • L.fullProfile) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hprimaryBudget : ProfileBudget hprimary S L.R 1) (hprimaryMean : primary.mean = 0) (hprimaryTangent : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (primary.high (↑t, x, θ)) = 0) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : ((joinedPacketPullbackField P M D hTime τ hτ hτT B primary hprimary N k⁻¹).smul k).WordBound 6 (4 * L.R) (BC.multiplierCost * (fixedVelocityGradeCost L.R S.H0 1 + fixedVelocityGradeCost L.R S.H0 2 + 1)) 0

theorem EulerPacketCylinderField.joinedPacket_normal_bound (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) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : CoefficientBudget (joinedSourceCoefficientData P M D τ hτ hτT B hTime)) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R) (hcost : BC.termCost ≤ L.R) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (α : ℝ) (hα : 0 < α) (hgrowth : timeProfileChange S.growth hTime = α • L.fullProfile) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hprimaryBudget : ProfileBudget hprimary S L.R 1) (hprimaryMean : primary.mean = 0) (hprimaryTangent : ∀ (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (D.normalField (↑t, x, θ)) (primary.high (↑t, x, θ)) = 0) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : (((joinedPacketPullbackField P M D hTime τ hτ hτT B primary hprimary N k⁻¹).smul k).map (normalComponentMap D.m₀)).WordBound 6 (4 * L.R) (BC.multiplierCost * (fixedVelocityGradeCost L.R S.H0 2 + 2) / k) 0

noncomputable def EulerPacketTerminalDatum.initializedPacketField (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) (α : ℝ) (N : ℕ) (κ : ℝ) : EulerPacketCylinderField.Field period M.T fun (z : EulerPacketPointJets.Domain) => ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).inverseFrame z) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.joinedSourceProfiles period M D τ hτ hτT B (EulerPacketCylinderField.joinedTerminalPrimary period M D τ hτ hτT B (initialData D δ hδ (α • ξ) hs)))) z)

Initialized packet field, constructed using joinedPacketPullbackField.

Equations

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

noncomputable def EulerPacketTerminalDatum.initializedResidualField (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) (κ : ℝ) (hκ : κ ≠ 0) : EulerPacketCylinderField.Field period M.T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) κ ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).inverseFrame z) ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).strain z) ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).normal z) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.joinedPrimaryProfiles period M D τ hτ hτT B (EulerTransversePacketPrimary.vector τ hτ hτT B (initialData D δ hδ (α • ξ) hs)) (EulerTransversePacketPrimary.scalar τ hτ hτT B (initialData D δ hδ (α • ξ) hs))))) (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledPressure N (EulerPacketCylinderField.joinedPrimaryProfiles period M D τ hτ hτT B (EulerTransversePacketPrimary.vector τ hτ hτT B (initialData D δ hδ (α • ξ) hs)) (EulerTransversePacketPrimary.scalar τ hτ hτT B (initialData D δ hδ (α • ξ) hs))))) z

Initialized residual field, constructed using joinedResidualField.

Equations

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

theorem EulerPacketTerminalDatum.initializedPacket_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 < τ) (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : ((initializedPacketField M D hTime τ hτ hτT B δ 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.initializedPacket_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 < τ) (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : (((initializedPacketField M D hTime τ hτ hτT B δ 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.initializedResidual_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 < τ) (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 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.joinedSourceCoefficientData period M D τ hτ hτT B hTime).inverse.multiply (initializedResidualField M D hTime τ hτ hτT B δ 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.initializedNormalizedField (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) (α : ℝ) (N : ℕ) (k : ℝ) : EulerPacketCylinderField.Field period D.T (k • fun (z : EulerPacketPointJets.Domain) => ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).inverseFrame z) (EulerPacketPointJets.fieldSum (N + 1) k⁻¹ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.joinedSourceProfiles period M D τ hτ hτT B (EulerPacketCylinderField.joinedTerminalPrimary period M D τ hτ hτT B (initialData D δ hδ (α • ξ) hs)))) z))

Initialized normalized field, given by ((initializedPacketField M D hTime τ hτ hτT B δ hδ ξ hs α N k⁻¹).smul k).changeTime hTime.

Equations

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

noncomputable def EulerPacketTerminalDatum.initializedNormalizedResidualField (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) : EulerPacketCylinderField.Field period D.T (k • fun (z : EulerPacketPointJets.Domain) => ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).inverseFrame z) (EulerPacketPointJets.slicedMomentumResidual (Set.Icc 0 M.T) k⁻¹ ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).inverseFrame z) ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).strain z) ((EulerPacketCylinderField.joinedSourceOperators period M D τ hτ hτT B).normal z) (EulerPacketPointJets.fieldSum (N + 1) k⁻¹ (EulerPacketProfileRecursion.assembledVelocity N (EulerPacketCylinderField.joinedPrimaryProfiles period M D τ hτ hτT B (EulerTransversePacketPrimary.vector τ hτ hτT B (initialData D δ hδ (α • ξ) hs)) (EulerTransversePacketPrimary.scalar τ hτ hτT B (initialData D δ hδ (α • ξ) hs))))) (EulerPacketPointJets.fieldSum (N + 1) k⁻¹ (EulerPacketProfileRecursion.assembledPressure N (EulerPacketCylinderField.joinedPrimaryProfiles period M D τ hτ hτT B (EulerTransversePacketPrimary.vector τ hτ hτT B (initialData D δ hδ (α • ξ) hs)) (EulerTransversePacketPrimary.scalar τ hτ hτT B (initialData D δ hδ (α • ξ) hs))))) z))

Initialized normalized residual field used in packet initialized correction data.

Equations

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

noncomputable def EulerPacketTerminalDatum.initializedCorrectionData (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) : EulerAllOrderCorrectionData.Data period D.T

Initialized correction data, constructed using EulerPacketCorrectionCoefficients.correctionDataOfFields.

Equations

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

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

theorem EulerPacketTerminalDatum.initializedNormalizedField_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 < τ) (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : ((initializedNormalizedField M D hTime τ hτ hτT B δ 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.initializedNormalizedResidualField_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 < τ) (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 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) : (initializedNormalizedResidualField M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).WordBound 6 (4 * L.R) (Real.exp (-(7 / 10) * X * Real.log k)) 0