The literal forward finite packet is its actual primary plus a remainder with a proved physical C1 bound.

theorem EulerPacketTerminalDatum.forwardInitializedProfiles_zero (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) (α : ℝ) : forwardInitializedProfiles M D δ hδ ξ hs α 0 = 0

theorem EulerPacketTerminalDatum.forwardInitializedProfiles_one_high (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) (α : ℝ) : (forwardInitializedProfiles M D δ hδ ξ hs α 1).high = EulerPacketForwardPrimary.vector D (initialData D δ hδ (α • ξ) hs)

theorem EulerPacketTerminalDatum.forwardInitializedProfiles_one_mean (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) (α : ℝ) : (forwardInitializedProfiles M D δ hδ ξ hs α 1).mean = 0

noncomputable def EulerPacketTerminalDatum.forwardInitializedPrimaryRemainder (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 : ℕ) (κ : ℝ) : EulerPacketProfileRecursion.VectorField

Forward initialized primary remainder, given by forwardInitializedVelocity M D δ hδ ξ hs α N κ - κ • vector D (initialData D δ hδ (α • ξ) hs).

Equations

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

noncomputable def EulerPacketTerminalDatum.forwardInitializedPrimaryRemainderField (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 : ℕ) (hN : 1 ≤ N) (κ : ℝ) : EulerPacketCylinderField.Field period D.T (forwardInitializedPrimaryRemainder M D δ hδ ξ hs α N κ)

Forward initialized primary remainder field as an element of Field period D.T (forwardInitializedPrimaryRemainder M D δ hδ ξ hs α N κ).

Equations

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

theorem EulerPacketTerminalDatum.forwardInitializedPrimaryRemainder_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)) : (forwardInitializedPrimaryRemainderField M D hTime δ hδ ξ hs α N hN k⁻¹).WordBound 6 (4 * L.R) ((EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 2 + 2) / k ^ 2) 0

theorem EulerPacketTerminalDatum.forwardInitializedPrimaryRemainder_physical_norm (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)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : ‖forwardInitializedPrimaryRemainder M D δ hδ ξ hs α N k⁻¹ (↑t, Y x, k * inner ℝ D.m₀ (Y x))‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 3 * ((EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 2 + 2) / k ^ 2)

theorem EulerPacketTerminalDatum.forwardInitializedPrimaryRemainder_physical_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) (α : ℝ) (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)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : DifferentiableAt ℝ Y x) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => forwardInitializedPrimaryRemainder M D δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y))) x‖ ≤ EulerCylinderPhysicalTensor.frequencyFactor k D.m₀ * (EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 3 * ((EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 2 + 2) / k ^ 2) * (4 * L.R)) * ‖fderiv ℝ Y x‖

noncomputable def EulerPacketTerminalDatum.forwardInitializedRemainderDerivativeCost (R H0 : ℝ) : ℝ

The constant contains no packet frequency or derivative of the inverse flow.

Equations

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

theorem EulerPacketTerminalDatum.forwardInitializedPrimaryRemainder_physical_fderiv_inv (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)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : DifferentiableAt ℝ Y x) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => forwardInitializedPrimaryRemainder M D δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y))) x‖ ≤ forwardInitializedRemainderDerivativeCost L.R S.H0 / k * ‖fderiv ℝ Y x‖