The exact zero-history packet has its literal finite velocity and scalar pressure plus the actual correction. These identities use the canonical pressure potential and therefore also identify its Hessian.

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

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

Forward initialized exact packet, given by exactPacketOfResidual period Q (forwardInitializedApproximationResidual M D hTime δ hδ ξ hs α Cagree N hN k hk).

Equations

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

theorem EulerPacketTerminalDatum.forwardInitializedExactPacket_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 < δ) (ξ : 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) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)) (t : ↑(Set.Icc 0 D.T)) : -(EulerCylinderReflection.reflection period) ((forwardInitializedExactPacket M D hTime δ hδ ξ hs α Cagree N hN k hk Q).velocity.field t) = (forwardInitializedExactPacket M D hTime δ hδ ξ hs α Cagree N hN k hk Q).velocity.field t

theorem EulerPacketTerminalDatum.forwardInitialized_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 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hδ1 : δ ≤ 1) (hα : 0 < α) (L : EulerTransversePacketForward.Budget D (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 ⋯ (forwardInitializedCorrectionData M D hTime δ 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 ⋯ (forwardInitializedCorrectionData M D hTime δ 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.

noncomputable def EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity (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) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Forward initialized exact physical velocity as an element of Space.

Equations

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

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity_eq (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) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree N hN k hk Q t Y x = forwardInitializedVelocity M D δ hδ ξ hs α N k⁻¹ (↑t, Y x, k * inner ℝ D.m₀ (Y x)) + k⁻¹ • ((D.F.field t) (Y x)) (EulerAllOrderDriftCorrection.Budget.pointField period Q t (EulerGraphPressurePotential.cylinderGraph period k D.m₀ (Y x)))

The approximation is exactly the finite physical velocity after undoing its true normalized coordinate transformation.

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity_fderiv (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) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : DifferentiableAt ℝ Y x) : fderiv ℝ (forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree N hN k hk Q t Y) x = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => forwardInitializedVelocity M D δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y))) x + fderiv ℝ (fun (y : EulerSmoothLimit.Space) => k⁻¹ • ((D.F.field t) (Y y)) (EulerAllOrderDriftCorrection.Budget.pointField period Q t (EulerGraphPressurePotential.cylinderGraph period k D.m₀ (Y y)))) x

noncomputable def EulerPacketTerminalDatum.forwardInitializedExactPhysicalPressure (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) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) : EulerSmoothLimit.Space → ℝ

Forward initialized exact physical pressure, given by (forwardInitializedExactPacket M D hTime δ hδ ξ hs α Cagree N hN k hk Q).graphPotential k t ∘ Y.

Equations

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

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalPressure_gradient (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) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : gradient (forwardInitializedExactPhysicalPressure M D hTime δ hδ ξ hs α Cagree N hN k hk Q t (Y t)) x = gradient (fun (y : EulerSmoothLimit.Space) => forwardInitializedPressure M D δ hδ ξ hs α N k⁻¹ (↑t, Y t y, k * inner ℝ D.m₀ (Y t y))) x + gradient (EulerAllOrderDriftCorrection.Budget.physicalPotential D period Q k Y t) x

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalPressure_hessian (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) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk)) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : fderiv ℝ (gradient (forwardInitializedExactPhysicalPressure M D hTime δ hδ ξ hs α Cagree N hN k hk Q t (Y t))) x = fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => forwardInitializedPressure M D δ hδ ξ hs α N k⁻¹ (↑t, Y t y, k * inner ℝ D.m₀ (Y t y))) x + fderiv ℝ (gradient (EulerAllOrderDriftCorrection.Budget.physicalPotential D period Q k Y t)) x