Concrete coefficient and background budgets for the actual nonlinear correction energy theorem.

Fixed continuous majorants for metric growth; no time continuity of arbitrary bound witnesses is required.

noncomputable def EulerGevreyGrowthCoefficient.growthBudgetBase (c D L : ℝ) : ℝ

A fixed bound for the metric derivative and viscosity contribution.

Equations

• EulerGevreyGrowthCoefficient.growthBudgetBase c D L = (D + 4 * L ^ 2 / c ^ 2) / (2 * c ^ 2)

noncomputable def EulerGevreyGrowthCoefficient.growthBudgetSlope (c L : ℝ) : ℝ

A fixed bound for the velocity-dependent metric transport slope.

Equations

• EulerGevreyGrowthCoefficient.growthBudgetSlope c L = 2 * L / (2 * c ^ 2)

theorem EulerGevreyGrowthCoefficient.growthBase_budget (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (c D L : ℝ) (hD : ‖K'‖ ≤ D) (hL : ↑K.firstBound ≤ L) : growthBase period K K' c ≤ growthBudgetBase c D L

Uniform actual coefficient bounds control the constant growth term.

theorem EulerGevreyGrowthCoefficient.growthSlope_budget (period : ℝ) (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c L : ℝ) (hκ : |κ| ≤ 1) (hm : ‖m‖ ≤ 1) (hL : ↑K.firstBound ≤ L) : growthSlope period K κ m c ≤ growthBudgetSlope c L

The actual transport metric slope has a uniform bound for the permitted lifted directions.

theorem EulerGevreyGrowthCoefficient.viscousGrowth_budget (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c ν D L : ℝ) (B : NNReal) (hν : ν ≤ 1) (hκ : |κ| ≤ 1) (hm : ‖m‖ ≤ 1) (hD : ‖K'‖ ≤ D) (hL : ↑K.firstBound ≤ L) : EulerWeightedCylinderEnergy.viscousGrowthCoefficient period K K' κ m c ν B ≤ growthBudgetBase c D L + growthBudgetSlope c L * ↑B

Uniform actual coefficient budgets majorize the complete viscous growth coefficient.

theorem EulerGevreyGrowthCoefficient.viscousGrowth_fixed_metric (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c ν D L B X : ℝ) (hc : 0 < c) (hν : ν ≤ 1) (hκ : |κ| ≤ 1) (hm : ‖m‖ ≤ 1) (hD : ‖K'‖ ≤ D) (hL : ↑K.firstBound ≤ L) (hB : 0 ≤ B) (hX : 0 ≤ X) : EulerWeightedCylinderEnergy.viscousGrowthCoefficient period K K' κ m c ν (EulerGevreyMetricEstimate.metricVelocityBound period c B X) ≤ growthBudgetBase c D L + growthBudgetSlope c L * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 6 * B + growthBudgetSlope c L * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 6 * EulerGevreyMetricEstimate.metricAmplification c * X

The metric PDE growth is bounded by a fixed affine function of the actual metric energy.

structure EulerCorrectionEnergyData.SpatialBudget (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} (hq : 6 ≤ q + 1) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (N : ℕ) (R : C(↑(Set.Icc 0 T), ℝ)) : Type

Actual derivative and residual norm budgets at the chosen cutoff; no energy or nonlinear forcing estimate is assumed.

• Rc : ℝ

  Coefficient derivative radius.

• M : ℝ

  Proven fixed-base pressure inverse bound.

• B : ℝ

  Base coefficient derivative bound.

• B0 : ℝ

  Background velocity norm bound.

• B1 : ℝ

  Background derivative norm bound.

• A0 : ℝ

  Linear coefficient norm bound.

• A2 : ℝ

  Quadratic coefficient norm bound.

• residual : ℝ

  Approximate-equation residual norm bound.

• Rc_nonneg : 0 ≤ self.Rc

  The coefficient radius is nonnegative.

• M_one_le : 1 ≤ self.M

  The pressure bound is at least one.

• B_nonneg : 0 ≤ self.B

  The base coefficient budget is nonnegative.

• B0_nonneg : 0 ≤ self.B0

  The background budget is nonnegative.

• B1_nonneg : 0 ≤ self.B1

  The background derivative budget is nonnegative.

• A0_nonneg : 0 ≤ self.A0

  The linear budget is nonnegative.

• A2_nonneg : 0 ≤ self.A2

  The quadratic budget is nonnegative.

• residual_pos : 0 < self.residual

  The residual budget is strictly positive.

• radius_pos (t : ↑(Set.Icc 0 T)) : 0 < R t

  The actual radius stays positive.

• inverse_five (t : ↑(Set.Icc 0 T)) : (EulerH6Pressure.CoefficientJet.restrict (D.metric.jet t) 5 ⋯).pressureConstant D.coercivity ≤ self.M

  The actual H⁵ projected inverse has the fixed bound.

• inverse_six (t : ↑(Set.Icc 0 T)) : (EulerH6Pressure.CoefficientJet.restrict (D.metric.jet t) 6 hq).pressureConstant D.coercivity ≤ self.M

  The actual H⁶ projected inverse has the fixed bound.

• radius_small (t : ↑(Set.Icc 0 T)) : 4 * self.M * (R t * self.Rc) ≤ 1

  The coefficient series is in the proved inverse absorption regime.

• metric_derivatives (t : ↑(Set.Icc 0 T)) (l : ℕ) : 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period (D.metric.jet t) 6 l ≤ self.Rc ^ l * ↑l.factorial ^ 2

  Actual higher coefficient derivatives satisfy the factorial estimate.

• metric_base (t : ↑(Set.Icc 0 T)) (r : ℕ) : r ≤ 6 → EulerJetProductBounds.boundLevel period (D.metric.jet t) r ≤ self.B

  Actual base coefficient derivatives satisfy the fixed budget.

• background (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N (R t) (D.approximation t) ≤ self.B0

  The actual approximate velocity has the background norm budget.

• background_derivative (t : ↑(Set.Icc 0 T)) : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N (R t) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) (D.approximation t)) ≤ self.B1

  The actual approximate velocity derivatives have the background derivative budget.

• linear (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedCoefficient period (D.linear.jet t) 6 N (R t) ≤ self.A0

  Actual linear multiplier derivatives have the linear budget.

• quadratic (t : ↑(Set.Icc 0 T)) : ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period ((D.quadratic i).jet t) 6 N (R t) ≤ self.A2

  Actual quadratic multiplier derivatives have the quadratic budget.

• residual_bound (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N (R t) (D.residual t) ≤ self.residual

  The literal approximate-equation residual has the residual budget.

structure EulerCorrectionEnergyData.MetricBudget (period : ℝ) [Fact (0 < period)] {q : ℕ} (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) : Type

An actual inverse metric and its uniform first spatial and time derivative budgets.

• metric : ↑(Set.Icc 0 T) → EulerSpatialSobolevInverse.SmoothCoefficient period

  Actual spatial inverse metric at each time.

• continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => (self.metric t).operator

  Its actual L² multiplier path is continuous.

• derivative : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))

  Actual time derivative of the L² metric operator.

• hasDeriv (t : ℝ) : t ∈ Set.Ioo 0 T → HasDerivAt (EulerVolterraConvolution.extendPath T hT (EulerRegularizedMetricPaths.metricOperatorPath period T self.metric ⋯)) (EulerVolterraConvolution.extendPath T hT self.derivative t) t

  The stated time derivative is the genuine derivative at every interior time.

• c : ℝ

  Positive square-root coercivity constant.

• c_pos : 0 < self.c

  Strict metric coercivity.

• symmetric (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3) : inner ℝ (((self.metric t).coefficient x) v) w = inner ℝ v (((self.metric t).coefficient x) w)

  Pointwise symmetry of the actual metric.

• coercive (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3) : self.c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((self.metric t).coefficient x) v) v

  Pointwise positive lower bound for the actual metric.

• inverse (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3) : ((self.metric t).coefficient x) (((D.metric.coefficient t).coefficient x) v) = v

  The actual metric inverts the coefficient in the pressure equation.

• bound : ℝ

  Uniform metric multiplier bound.

• first : ℝ

  Uniform first spatial derivative bound.

• time : ℝ

  Uniform time derivative operator bound.

• bound_nonneg : 0 ≤ self.bound

  The multiplier budget is nonnegative.

• first_nonneg : 0 ≤ self.first

  The spatial derivative budget is nonnegative.

• time_nonneg : 0 ≤ self.time

  The time derivative budget is nonnegative.

• bound_le (t : ↑(Set.Icc 0 T)) : ↑(self.metric t).bound ≤ self.bound

  The actual multiplier witness is bounded uniformly.

• first_le (t : ↑(Set.Icc 0 T)) : ↑(self.metric t).firstBound ≤ self.first

  The actual first derivative witness is bounded uniformly.

• time_le (t : ↑(Set.Icc 0 T)) : ‖self.derivative t‖ ≤ self.time

  The actual time derivative is bounded uniformly.

noncomputable def EulerCorrectionEnergyData.baseMetricJet (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q + 1) {T : ℝ} (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (t : ↑(Set.Icc 0 T)) : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 (D.metric.coefficient t)

The canonical genuine base-order coefficient jet.

Equations

• EulerCorrectionEnergyData.baseMetricJet period hq D t = EulerH6Pressure.CoefficientJet.restrict (D.metric.jet t) 6 hq

noncomputable def EulerCorrectionEnergyData.MetricBudget.operatorPath (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} (K : MetricBudget period T hT D) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))

The actual metric budget determines its concrete continuous L² multiplier path.

Equations

• EulerCorrectionEnergyData.MetricBudget.operatorPath period K = EulerRegularizedMetricPaths.metricOperatorPath period T K.metric ⋯

theorem EulerCorrectionEnergyData.MetricBudget.operator_coercive (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} (K : MetricBudget period T hT D) (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : K.c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((operatorPath period K) t) v) v

The actual metric operator is coercive with the same pointwise constant.

theorem EulerCorrectionEnergyData.SpatialBudget.base_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : SpatialBudget period hq D N R) (t : ↑(Set.Icc 0 T)) (r : ℕ) (hr : r ≤ 6) : EulerJetProductBounds.boundLevel period (baseMetricJet period hq D t) r ≤ S.B

The actual canonical base jet inherits the given derivative budget.

noncomputable def EulerCorrectionEnergyData.MetricBudget.growth0 (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} (K : MetricBudget period T hT D) (B0 : ℝ) : ℝ

The fixed constant part of the actual metric-growth majorant.

Equations

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

noncomputable def EulerCorrectionEnergyData.MetricBudget.growth1 (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} (K : MetricBudget period T hT D) : ℝ

The fixed linear part of the actual metric-growth majorant.

Equations

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

noncomputable def EulerCorrectionEnergyData.MetricBudget.multiplier (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} (K : MetricBudget period T hT D) : ℝ

The fixed coefficient multiplying the actual forcing norm.

Equations

• EulerCorrectionEnergyData.MetricBudget.multiplier period K = K.bound / K.c

theorem EulerCorrectionEnergyData.MetricBudget.constants_nonneg (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} (K : MetricBudget period T hT D) (B0 : ℝ) (hB0 : 0 ≤ B0) : 0 ≤ growth0 period K B0 ∧ 0 ≤ growth1 period K ∧ 0 ≤ multiplier period K

All fixed metric-growth and forcing coefficients are nonnegative.