Source budgets and the actual initialized residual construct exact corrected lifted packets at every sufficiently large frequency.

structure EulerAllOrderDriftCorrection.ExactLiftedPacket (P : ℝ) [Fact (0 < P)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data P T) (B : Budget P hT A) : Type

The output fields and all their properties are conclusions of the constructed correction and the verified approximate residual.

• velocity : EulerAllOrderCorrectionData.FieldTower P T

  Velocity field of ExactLiftedPacket, of type FieldTower P T.

• pressure : EulerAllOrderCorrectionData.FieldTower P T

  Pressure field of ExactLiftedPacket, of type FieldTower P T.

• zero_initial_correction (q : ℕ) : (self.velocity.realization q) ⟨0, ⋯⟩ - (A.approximation.realization q) ⟨0, ⋯⟩ = 0
• divergence (t : ↑(Set.Icc 0 T)) : self.velocity.field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P A.κ A.direction
• gradient (t : ↑(Set.Icc 0 T)) : self.pressure.field t ∈ EulerLiftedGradientSpace.gradientSpace P A.κ A.direction
• energy (n : ℕ) (t : ↑(Set.Icc 0 T)) : EulerGevreyMetricEstimate.energyNorm P n ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath P B.metric) t) ((self.velocity.realization (n + 6 + 1)) t - (A.approximation.realization (n + 6 + 1)) t) ≤ 2 * (B.spatial (n + 6) ⋯).full.residual * Real.exp (3 * B.growthCoefficient * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm P n ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath P B.metric) t) ((self.velocity.realization (n + 6 + 1)) t - (A.approximation.realization (n + 6 + 1)) t) ≤ B.delta / 2
• equation (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (self.velocity.realization q)) (-EulerCorrectionResidualCancellation.nonlinearity P (EulerAllOrderCorrectionData.Data.atOrder P A q) hq ⟨t, ⋯⟩ ((self.velocity.realization (q + 1)) ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator P (A.metric.jet q ⟨t, ⋯⟩)) ((self.pressure.realization q) ⟨t, ⋯⟩)) t

noncomputable def EulerAllOrderDriftCorrection.exactPacketOfResidual (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (R : ApproximationResidual P hT A) : ExactLiftedPacket P hT A B

Exact packet of residual, bundling velocity, pressure, zero_initial_correction, divergence and the required compatibility proofs.

Equations

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

theorem EulerAllOrderDriftCorrection.exactPacketOfResidual_velocity_odd (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (R : ApproximationResidual P hT A) (E : EulerCorrectionAssembly.ParityData P A) (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection P) ((exactPacketOfResidual P B R).velocity.field t) = (exactPacketOfResidual P B R).velocity.field t

noncomputable def EulerPacketTerminalDatum.initializedExactPacket (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 : EulerAllOrderDriftCorrection.Budget period ⋯ (initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk)) : EulerAllOrderDriftCorrection.ExactLiftedPacket period ⋯ (initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk) Q

Initialized exact packet, given by exactPacketOfResidual period Q (initializedApproximationResidual M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).

Equations

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

theorem EulerPacketTerminalDatum.initializedExactPacket_velocity_odd (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) (α : ℝ) (eM : EulerMeanPacketProvider.EvenData M) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk)) (t : ↑(Set.Icc 0 D.T)) : -(EulerCylinderReflection.reflection period) ((initializedExactPacket M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk Q).velocity.field t) = (initializedExactPacket M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk Q).velocity.field t

theorem EulerPacketTerminalDatum.initialized_exact_lifted_packets_eventually (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) (α : ℝ) (hδ1 : δ ≤ 1) (hα : 0 < α) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (Ξ : ↑(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) : ∃ (ρ0 : ℝ) (C : ℝ), 0 < ρ0 ∧ 0 < C ∧ ∀ᶠ (k : ℝ) in Filter.atTop, ∃ (hk : 4 ≤ k) (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk)), Q.delta = EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ Q.initialRadius = ρ0 ∧ Q.growthCoefficient = C ∧ Nonempty (EulerAllOrderDriftCorrection.ExactLiftedPacket period ⋯ (initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk) Q)

No inverse budget, residual equation or pressure is postulated here. The original source data construct the budget and the exact corrected pair for every sufficiently large frequency, with fixed positive radius and cost.