Related estimates used together by the same construction modules.

A fixed actual correction and the derived approximation bounds construct physical graph-flow data. No new solution or inverse is an input.

The actual lifted time coefficient has simultaneous sup and cylinder L² bounds from the genuine approximation and correction time derivatives.

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds1 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (LiftTangent [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds1 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds2 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (LiftTangent [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds2 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds3 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedAddCommGroup (LiftTangent [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds3 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds4 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedSpace ℝ (LiftTangent [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds4 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds5 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds5 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds6 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds6 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds7 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds7 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds8 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds8 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds9 {T : ℝ} (n : ℕ) : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds9 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds10 {T : ℝ} (n : ℕ) : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedTimeBounds10 n = inferInstance

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient_periodic (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw_t : EulerPacketProfileRecursion.VectorField} (H : EulerPacketCylinderField.Field P T raw_t) (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : ((liftedPacketDerivativeCoefficient P B H).field t) (x.1, ↑c + x.2) = ((liftedPacketDerivativeCoefficient P B H).field t) x

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient_jetSeries (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw_t : EulerPacketProfileRecursion.VectorField} (H : EulerPacketCylinderField.Field P T raw_t) (n : ℕ) (t : ↑(Set.Icc 0 T)) : (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑((liftedPacketDerivativeCoefficient P B H).field t)) q n) = EulerCylinderJetLp.tensor P (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerMetricTransport.transportDirection A.κ A.direction (H.toFieldTower.pointField t q + (timeDerivativeTower P B).pointField t q)) n

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient_memLp (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw_t : EulerPacketProfileRecursion.VectorField} (H : EulerPacketCylinderField.Field P T raw_t) (n : ℕ) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑((liftedPacketDerivativeCoefficient P B H).field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient_jet_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw_t : EulerPacketProfileRecursion.VectorField} (H : EulerPacketCylinderField.Field P T raw_t) (R ρ Ch Ce : ℝ) (hκ : |A.κ| ≤ 1) (hm : ‖A.direction‖ ≤ 1) (hR : 0 ≤ R) (hρ : 0 < ρ) (hCh : 0 ≤ Ch) (hCe : 0 ≤ Ce) (hH : H.WordBound 6 R Ch 0) (hE : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((timeDerivativeTower P B).realization (n + 6)) t) ≤ Ce) (n : ℕ) : ‖(liftedPacketDerivativeCoefficient P B H).jet n‖ ≤ 2 * liftedInputConstant P * (Ch + Ce) * liftedInputRadius R ρ ^ n * ↑n.factorial ^ 2

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient_L2_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw_t : EulerPacketProfileRecursion.VectorField} (H : EulerPacketCylinderField.Field P T raw_t) (R ρ Ch Ce : ℝ) (hκ : |A.κ| ≤ 1) (hm : ‖A.direction‖ ≤ 1) (hR : 0 ≤ R) (hρ : 0 < ρ) (hCh : 0 ≤ Ch) (hCe : 0 ≤ Ce) (hH : H.WordBound 6 R Ch 0) (hE : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((timeDerivativeTower P B).realization (n + 6)) t) ≤ Ce) (n : ℕ) (t : ↑(Set.Icc 0 T)) : (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑((liftedPacketDerivativeCoefficient P B H).field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ 2 * liftedInputConstant P * (Ch + Ce) * liftedInputRadius R ρ ^ n * ↑n.factorial ^ 2

noncomputable def EulerAllOrderDriftCorrection.physicalInputRadius (R Rt ρ : ℝ) : ℝ

Physical input radius, given by max (liftedInputRadius R ρ) (liftedInputRadius Rt ρ).

Equations

• EulerAllOrderDriftCorrection.physicalInputRadius R Rt ρ = max (EulerAllOrderDriftCorrection.liftedInputRadius R ρ) (EulerAllOrderDriftCorrection.liftedInputRadius Rt ρ)

noncomputable def EulerAllOrderDriftCorrection.physicalInputSize (P k C0 Cn Ev : ℝ) [Fact (0 < P)] : ℝ

Physical input size, given by liftedInputConstant P*((C0+Cn)/k+2*Ev).

Equations

• EulerAllOrderDriftCorrection.physicalInputSize P k C0 Cn Ev = EulerAllOrderDriftCorrection.liftedInputConstant P * ((C0 + Cn) / k + 2 * Ev)

theorem EulerAllOrderDriftCorrection.envelope_radius_mono {C R S : ℝ} (hC : 0 ≤ C) (hR : 0 ≤ R) (hRS : R ≤ S) (n : ℕ) : C * R ^ n * ↑n.factorial ^ 2 ≤ C * S ^ n * ↑n.factorial ^ 2

noncomputable def EulerAllOrderDriftCorrection.Budget.physicalFlowData (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (H : EulerPacketCylinderField.Field P T raw_t) (hGfield : A.approximation = G.toFieldTower) (htime : EulerPacketCylinderField.TimeDerivative ⋯ G H) (k R Rt ρ C0 Cn Ch Ev Et : ℝ) (hk : 1 ≤ k) (hκ : A.κ = k⁻¹) (hm : ‖A.direction‖ ≤ 1) (hR : 0 ≤ R) (hRt : 0 ≤ Rt) (hρ : 0 < ρ) (hC0 : 0 ≤ C0) (hCn : 0 ≤ Cn) (hCh : 0 ≤ Ch) (hEv : 0 ≤ Ev) (hEt : 0 ≤ Et) (hG : G.WordBound 6 R C0 0) (hN : (G.map (EulerPacketCylinderField.normalComponentMap A.direction)).WordBound 6 R (Cn / k) 0) (hH : H.WordBound 6 Rt Ch 0) (hE : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((fieldTower P B).realization (n + 6)) t) ≤ Ev) (hEtower : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((timeDerivativeTower P B).realization (n + 6)) t) ≤ Et) (hsmall : physicalInputSize P k C0 Cn Ev * physicalInputRadius R Rt ρ * T ≤ 1 / 8) : EulerPhysicalGraphFlowBounds.Data P T

Physical flow data as an element of EulerPhysicalGraphFlowBounds.Data P T.

Equations

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

Actual weighted correction and pressure norms bound the physical velocity gradient and the Hessian of the constructed scalar potential for that same correction.

noncomputable def EulerAllOrderDriftCorrection.weightedPhysicalGradientCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (R CF ρ Cw : ℝ) : ℝ

Weighted physical gradient cost, given by ((1+9*CF)*physicalFixedCost D R CF ρ⁻¹ 1)*(sobolevEmbeddingConstant P 3*Cw).

Equations

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

theorem EulerAllOrderDriftCorrection.weightedPhysicalGradientCost_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (R CF ρ Cw : ℝ) (hR : 0 ≤ R) (hCF : 0 ≤ CF) (hρ : 0 < ρ) (hCw : 0 ≤ Cw) : 0 ≤ weightedPhysicalGradientCost D P R CF ρ Cw

theorem EulerAllOrderDriftCorrection.Budget.physical_gradient_hessian_of_weighted {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {A : EulerAllOrderCorrectionData.Data P D.T} (Q : Budget P ⋯ A) (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)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (R CF : ℝ) (hR : 0 ≤ R) (hCF : 0 ≤ CF) (hFb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ CF * EulerGevrey.majorant R 0 n) (k ρ Cw d : ℝ) (hk : 1 ≤ k) (hκ : A.κ = k⁻¹) (hm : A.direction = D.m₀) (hρ : 0 < ρ) (hCw : 0 ≤ Cw) (hd : 0 ≤ d) (he : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((fieldTower P Q).realization (n + 6)) t) ≤ Cw * d) (hp : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((pressureTower P Q).realization (n + 6)) t) ≤ Cw * d) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => k⁻¹ • ((D.F.field t) (Y t y)) (pointField P Q t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y t y)))) x‖ ≤ weightedPhysicalGradientCost D P R CF ρ Cw * k * d ∧ ‖fderiv ℝ (gradient (physicalPotential D P Q k Y t)) x‖ ≤ weightedPhysicalGradientCost D P R CF ρ Cw * k * d

Fixed polynomial envelopes for the physical remainder, correction error and lifted-flow input costs. All spatial derivative orders here are fixed (H6 and one physical derivative).

The actual finite and exact packets have the source shear at every physical point. The slow primary derivative and finite tail contribute only a fixed source constant divided by the frequency.

noncomputable def EulerPacketTerminalDatum.initializedGlobalShearCost (R H0 C : ℝ) : ℝ

Initialized global shear cost as an element of ℝ.

Equations

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

theorem EulerPacketTerminalDatum.initializedPrimary_global_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 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (H : EulerTransversePacketPrimary.Budget L) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : EulerPacketCylinderField.CoefficientBudget (EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖)) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile) : (EulerTransversePacketPrimary.vectorField τ hτ hτT B (initialData D δ hδ (α • ξ) hs)).WordBound 6 (4 * L.R) (EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 1) 0

theorem EulerPacketTerminalDatum.initializedVelocity_global_gradient_error (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) (α : ℝ) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (H : EulerTransversePacketPrimary.Budget L) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : EulerPacketCylinderField.CoefficientBudget (EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖)) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile) (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 : HasFDerivAt Y ((D.FInv.field t) (Y x)) x) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y))) x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) (Y x))) ((D.normal.field t) (Y x))‖ ≤ initializedGlobalShearCost L.R S.H0 NB.C / k

theorem EulerPacketTerminalDatum.initializedExactPhysicalVelocity_global_gradient_error (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) (α : ℝ) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (H : EulerTransversePacketPrimary.Budget L) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (W : L.GradeGuards NB) (LM : EulerMeanPacketProvider.Budget M 6 L.R) (WM : LM.GradeGuards) (BC : EulerPacketCylinderField.CoefficientBudget (EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B 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 : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖)) (S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T)) (hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile) (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)) (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 : HasFDerivAt Y ((D.FInv.field t) (Y x)) x) : ‖fderiv ℝ (initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk Q t Y) x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) (Y x))) ((D.normal.field t) (Y x))‖ ≤ initializedGlobalShearCost L.R S.H0 NB.C / k + ‖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 EulerPacketPhysicalCost.coordinateCost : ℝ

Coordinate cost, given by ‖coordinateEquiv.symm.toContinuousLinearMap‖.

Equations

• EulerPacketPhysicalCost.coordinateCost = ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖

noncomputable def EulerPacketPhysicalCost.physicalEnvelope (X S : ℝ) : ℝ

Physical envelope, given by 3*X*((1+18*X^2*X)*(9*X^2*(X+coordinateCost*2*S)+2)).

Equations

• EulerPacketPhysicalCost.physicalEnvelope X S = 3 * X * ((1 + 18 * X ^ 2 * X) * (9 * X ^ 2 * (X + EulerPacketPhysicalCost.coordinateCost * 2 * S) + 2))

noncomputable def EulerPacketPhysicalCost.shearEnvelope (X : ℝ) : ℝ

Shear envelope as an element of ℝ.

Equations

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

noncomputable def EulerPacketPhysicalCost.hessianEnvelope (X : ℝ) : ℝ

Hessian envelope, constructed using sobolevEmbeddingConstant.

Equations

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

def EulerPacketPhysicalCost.timeEnvelope (X : ℝ) : ℝ

Time envelope, given by 6*EulerPacketRadiusPolynomial.normalEnvelope X * (fixedVelocityGradeCost X X 1+fixedVelocityGradeCost X X 2+1).

Equations

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

noncomputable def EulerPacketPhysicalCost.radiusEnvelope (X : ℝ) : ℝ

Radius envelope, given by 1+coordinateCost*(4*X+4*inverseRadiusEnvelope X).

Equations

• EulerPacketPhysicalCost.radiusEnvelope X = 1 + EulerPacketPhysicalCost.coordinateCost * (4 * X + 4 * EulerPacketFiveCost.inverseRadiusEnvelope X)

noncomputable def EulerPacketPhysicalCost.velocityInputEnvelope (X : ℝ) : ℝ

Velocity input envelope, given by liftedInputConstant period*(velocity X X X+normal X X X).

Equations

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

noncomputable def EulerPacketPhysicalCost.errorInputEnvelope (X : ℝ) : ℝ

Error input envelope, given by 2*liftedInputConstant period*outputEnvelope period X.

Equations

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

noncomputable def EulerPacketPhysicalCost.timeInputEnvelope (X : ℝ) : ℝ

Time input envelope, given by 2*liftedInputConstant period*(timeEnvelope X+outputEnvelope period X).

Equations

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

noncomputable def EulerPacketPhysicalCost.weightedErrorEnvelope (X : ℝ) : ℝ

Weighted error envelope, given by (1+9*X)*physicalEnvelope X (4*inverseRadiusEnvelope X)*sobolevEmbeddingConstant period 3 * outputEnvelope period X.

Equations

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

noncomputable def EulerPacketPhysicalCost.extraEnvelope (X : ℝ) : ℝ

Extra envelope as an element of ℝ.

Equations

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

noncomputable def EulerPacketPhysicalCost.extraPolynomial : Polynomial ℝ

Extra polynomial as an element of Polynomial ℝ.

theorem EulerPacketPhysicalCost.extraPolynomial_eval (X : ℝ) : Polynomial.eval X extraPolynomial = extraEnvelope X

noncomputable def EulerPacketPhysicalCost.extraConstant : ℝ

Extra constant, given by coefficientCost extraPolynomial.

Equations

• EulerPacketPhysicalCost.extraConstant = EulerPolynomialCost.coefficientCost EulerPacketPhysicalCost.extraPolynomial

noncomputable def EulerPacketPhysicalCost.extraPower : ℕ

Extra power, given by extraPolynomial.natDegree.

Equations

• EulerPacketPhysicalCost.extraPower = EulerPacketPhysicalCost.extraPolynomial.natDegree

theorem EulerPacketPhysicalCost.extraConstant_pos : 0 < extraConstant

theorem EulerPacketPhysicalCost.extraEnvelope_power (X : ℝ) (hX : 1 ≤ X) : extraEnvelope X ≤ extraConstant * X ^ extraPower

theorem EulerPacketPhysicalCost.physicalEnvelope_nonneg (X S : ℝ) (hX : 0 ≤ X) (hS : 0 ≤ S) : 0 ≤ physicalEnvelope X S

theorem EulerPacketPhysicalCost.extra_components (X : ℝ) (hX : 0 ≤ X) : EulerPacketCorrectionOutput.outputEnvelope EulerPacketTerminalDatum.period X ≤ extraEnvelope X ∧ radiusEnvelope X ≤ extraEnvelope X ∧ velocityInputEnvelope X ≤ extraEnvelope X ∧ errorInputEnvelope X ≤ extraEnvelope X ∧ timeInputEnvelope X ≤ extraEnvelope X ∧ weightedErrorEnvelope X ≤ extraEnvelope X ∧ shearEnvelope X ≤ extraEnvelope X ∧ hessianEnvelope X ≤ extraEnvelope X

theorem EulerPacketPhysicalCost.gradeCost_mono (R H X : ℝ) (hR : 0 ≤ R) (hH : 0 ≤ H) (hRX : R ≤ X) (hHX : H ≤ X) (n : ℕ) : EulerPacketCylinderField.fixedVelocityGradeCost R H n ≤ EulerPacketCylinderField.fixedVelocityGradeCost X X n

theorem EulerPacketPhysicalCost.physicalFixedCost_one_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C S X Y : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hS : 0 ≤ S) (hRX : R ≤ X) (hCX : C ≤ X) (hSY : S ≤ Y) : EulerPacketPhysicalGevrey.physicalFixedCost D R C S 1 ≤ physicalEnvelope X Y

theorem EulerPacketPhysicalCost.shearCost_le (R H C X : ℝ) (hR : 0 ≤ R) (hH : 0 ≤ H) (hC : 0 ≤ C) (hRX : R ≤ X) (hHX : H ≤ X) (hCX : C ≤ X) : EulerPacketTerminalDatum.initializedGlobalShearCost R H C ≤ shearEnvelope X

theorem EulerPacketPhysicalCost.hessianCost_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {q : ℕ} {R₀ : ℝ} (N : EulerTransversePacketJoin.NormalBudget D q R₀) (R H Rc C X : ℝ) (hR : 0 ≤ R) (hH : 0 ≤ H) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hRX : R ≤ X) (hHX : H ≤ X) (hRcX : Rc ≤ X) (hCX : C ≤ X) (hNR : N.Rc ≤ X) (hNC : N.C ≤ X) : EulerPacketTerminalDatum.initializedPressureHessianCost N R H Rc C ≤ hessianEnvelope X