With the base boundary parameter zero, the entire actual forward initial increment is supported in the small physical packet ball. The exact correction starts from zero, so it adds no initial tail.

noncomputable def EulerPacketTerminalDatum.forwardInitializedInitialHigh (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) (α : ℝ) (N : ℕ) (k : ℝ) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Forward initialized initial high, given by scale M.ℓ (fun x => EulerPacketInitial.high N k⁻¹ 0 (forwardInitializedProfiles M D δ hδ ξ hs α) (0,(x,k*inner ℝ D.m₀ x))).

Equations

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

noncomputable def EulerPacketTerminalDatum.forwardInitializedInitialMean (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) (α : ℝ) (N : ℕ) (k : ℝ) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Forward initialized initial mean, given by scale M.ℓ (fun x => EulerPacketInitial.mean N k⁻¹ 0 (forwardInitializedProfiles M D δ hδ ξ hs α) (0,(x,k*inner ℝ D.m₀ x))).

Equations

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

theorem EulerPacketTerminalDatum.forwardInitializedInitialHigh_support (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) (α : ℝ) (hS : D.support ⊆ Metric.closedBall 0 (1 / 2)) (N : ℕ) (k : ℝ) : tsupport (forwardInitializedInitialHigh M D δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 (M.ℓ / 2)

theorem EulerPacketTerminalDatum.forwardInitializedInitialMean_zero (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) (α : ℝ) (hL : M.L = 0) (N : ℕ) (k : ℝ) : forwardInitializedInitialMean M D δ hδ ξ hs α N k = 0

theorem EulerPacketTerminalDatum.forwardInitializedInitial_split (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) (α : ℝ) (N : ℕ) (k : ℝ) : (EulerPhysicalL2Scaling.scale M.ℓ fun (x : EulerSmoothLimit.Space) => forwardInitializedVelocity M D δ hδ ξ hs α N k⁻¹ (0, x, k * inner ℝ D.m₀ x)) = forwardInitializedInitialHigh M D δ hδ ξ hs α N k + forwardInitializedInitialMean M D δ hδ ξ hs α N k

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity_initial (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 : EulerSmoothLimit.Space) : forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree N hN k hk Q ⟨0, ⋯⟩ id x = forwardInitializedVelocity M D δ hδ ξ hs α N k⁻¹ (0, x, k * inner ℝ D.m₀ x)

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity_initial_split (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)) : EulerPhysicalL2Scaling.scale M.ℓ (forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree N hN k hk Q ⟨0, ⋯⟩ id) = forwardInitializedInitialHigh M D δ hδ ξ hs α N k + forwardInitializedInitialMean M D δ hδ ξ hs α N k

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity_initial_support (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)) (hL : M.L = 0) (hS : D.support ⊆ Metric.closedBall 0 (1 / 2)) : tsupport (EulerPhysicalL2Scaling.scale M.ℓ (forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree N hN k hk Q ⟨0, ⋯⟩ id)) ⊆ Metric.closedBall 0 (M.ℓ / 2)