The uniform source comparison gives the actual child label estimate at exponent 10(q+2), retaining the same exact correction and its errors.

The actual derivative of the zero-history initialized normalized approximation has a source-dependent Gevrey bound uniform in the truncation frequency. The time derivative of the inverse deformation is included explicitly.

noncomputable def EulerPacketTerminalDatum.forwardInitializedNormalizedDerivativeField (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 : ℕ) (k : ℝ) : EulerPacketCylinderField.Field period D.T (EulerPacketCoordinates.coordinateTime D k (forwardInitializedVelocity M D δ hδ ξ hs α N k⁻¹) (forwardInitializedVelocityDerivative M D δ hδ ξ hs α N k⁻¹))

Forward initialized normalized derivative field, constructed using coordinateTimeField.

Equations

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

theorem EulerPacketTerminalDatum.forwardInitializedNormalizedField_time (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 : ℕ) (k : ℝ) : EulerPacketCylinderField.TimeDerivative ⋯ (forwardInitializedNormalizedField M D hTime δ hδ ξ hs α N k) (forwardInitializedNormalizedDerivativeField M D hTime δ hδ ξ hs α N k)

theorem EulerPacketTerminalDatum.forwardInitializedNormalizedDerivativeField_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)) : (forwardInitializedNormalizedDerivativeField M D hTime δ hδ ξ hs α N k).WordBound 6 (4 * L.R) (6 * NB.blockAmplitude * (EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 1 + EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 2 + 1)) 0

A single polynomial comparison gives the actual canonical correction, the physical shear and pressure errors, and the three flow fields. Only the displayed numerical frequency margins are independent extra guards.

theorem EulerPacketTerminalDatum.forward_uniform_flow_and_shear (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δ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (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) (W : ℝ) (hW : EulerPacketForwardRadius.RadiusPrimitives L LM NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.g t ≤ W) (k : ℝ) (hk : 4 ≤ k) (hX : 64 ≤ EulerPacketSourceFrequency.expansion k) (hlog : 1 ≤ Real.log k) (hfrequency : EulerPacketInitializedOutputCost.uniformConstant * W ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k) (hdelta : EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ≤ k ^ (-3)) (hroot : 16 ≤ k ^ (1 / 4)) (htrace : max 71 √(2 / period + 2 * period) ≤ k ^ (1 / 24)) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hXs : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (X t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (X t) x = (D.F.field t) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) : ∃ (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk)) (G : EulerPhysicalGraphFlowBounds.Data period D.T), Q.delta = EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ Q.initialRadius = EulerPacketCorrectionScalar.initialRadius (forwardInitializedRadius LM L NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ) (L.correctionCoefficients NB period).M (L.correctionCoefficients NB period).Rc ∧ G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient period Q (forwardInitializedNormalizedField M D hTime δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ G.A₁ = EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient period Q (forwardInitializedNormalizedDerivativeField M D hTime δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k D.m₀) ((G.A.field t) z) = 0) ∧ (∀ (s n : ℕ), n + 6 ≤ s → ∀ (t : ↑(Set.Icc 0 D.T)), EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.fieldTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.pressureTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.timeDerivativeTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k)) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t)) x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4)) ∧ ‖fderiv ℝ (gradient (forwardInitializedExactPhysicalPressure M D hTime δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t))) x - (EulerPacketForwardShear.pressureCoefficient D ξ α t (Y t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4))) ∧ ∀ (ell : ℝ) (hell : 0 < ell), ell ≤ 1 → ∀ (t : ↑(Set.Icc 0 D.T)), (G.displacementField k D.m₀ ell hell t).HasJetBound (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ (G.velocityField k D.m₀ ell hell t).HasJetBound (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ (G.accelerationFieldL2 k D.m₀ ell hell t).HasJetBound (k ^ (1 / 4)) (ell⁻¹ * k ^ (5 / 4)) ∧ EulerGevrey.HasSupBound (G.displacementField k D.m₀ ell hell t).field (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ EulerGevrey.HasSupBound (G.velocityField k D.m₀ ell hell t).field (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4))

theorem EulerPacketTerminalDatum.forward_uniform_child_label_bounds (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δ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (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) (W : ℝ) (hW : EulerPacketForwardRadius.RadiusPrimitives L LM NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.g t ≤ W) (k : ℝ) (hk : 4 ≤ k) (hX : 64 ≤ EulerPacketSourceFrequency.expansion k) (hlog : 1 ≤ Real.log k) (hfrequency : EulerPacketInitializedOutputCost.uniformConstant * W ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k) (hdelta : EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ≤ k ^ (-3)) (hroot : 16 ≤ k ^ (1 / 4)) (htrace : max 71 √(2 / period + 2 * period) ≤ k ^ (1 / 24)) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hXs : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (X t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (X t) x = (D.F.field t) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (Dp Vp Wp : ↑(Set.Icc 0 D.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : 1 ≤ K) (hDp : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (Dp t)) (hVp : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (Vp t)) (hWp : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (Wp t)) (q : ℕ) (hk69 : 69 ≤ k) (hKk : K ≤ k) (hbig : 2 + 45 * EulerPacketParentLabelBounds.embeddingCost ≤ k) (hcost : EulerSobolevSourceExponent.fixedCost q ≤ k) (hinv : ell⁻¹ ≤ k ^ (3 / 4)) : ∃ (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk)) (G : EulerPhysicalGraphFlowBounds.Data period D.T) (E : ↑(Set.Icc 0 D.T) → EulerChildParticleFieldBounds.Data), Q.delta = EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ Q.initialRadius = EulerPacketCorrectionScalar.initialRadius (forwardInitializedRadius LM L NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ) (L.correctionCoefficients NB period).M (L.correctionCoefficients NB period).Rc ∧ G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient period Q (forwardInitializedNormalizedField M D hTime δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ G.A₁ = EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient period Q (forwardInitializedNormalizedDerivativeField M D hTime δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k D.m₀) ((G.A.field t) z) = 0) ∧ (∀ (s n : ℕ), n + 6 ≤ s → ∀ (t : ↑(Set.Icc 0 D.T)), EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.fieldTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.pressureTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.timeDerivativeTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k)) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t)) x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4)) ∧ ‖fderiv ℝ (gradient (forwardInitializedExactPhysicalPressure M D hTime δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t))) x - (EulerPacketForwardShear.pressureCoefficient D ξ α t (Y t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4))) ∧ (∀ (t : ↑(Set.Icc 0 D.T)), (E t).parentDisplacement = Dp t ∧ (E t).parentVelocity = Vp t ∧ (E t).parentAcceleration = Wp t ∧ (E t).displacement = G.displacementField k D.m₀ ell hell t ∧ (E t).velocity = G.velocityField k D.m₀ ell hell t ∧ (E t).acceleration = G.accelerationFieldL2 k D.m₀ ell hell t ∧ (E t).inner = (EulerSmoothBanachFlow.flowData D.T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k D.m₀ D.T G.A ell)).forward ↑t) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (n : ℕ), EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q (E t).childDisplacement.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q (E t).childVelocity.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q (E t).childAcceleration.toLp ⋯ n ≤ (k ^ (10 * (q + 2))) ^ (n + 1) * ↑n.factorial ^ 2) ∧ ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(G.displacementField k D.m₀ ell hell t).field x‖ ≤ k ^ (-(1 / 4))