Actual metric Gevrey energies, fixed norm conversion, and nonlinear scalar growth bounds.

noncomputable def EulerGevreyMetricEstimate.energyNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ℝ

The actual fixed-base metric Gevrey energy of one complete Sobolev field.

Equations

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

noncomputable def EulerGevreyMetricEstimate.energyLoss (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ℝ

The actual metric radius-loss quantity at the same cutoff.

Equations

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

noncomputable def EulerGevreyMetricEstimate.metricAmplification (c : ℝ) : ℝ

A fixed conversion factor, with no external derivative cutoff in its definition.

Equations

• EulerGevreyMetricEstimate.metricAmplification c = 1 + √5461 / c

theorem EulerGevreyMetricEstimate.energyNorm_nonneg (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : 0 ≤ energyNorm period N hN ρ K u

theorem EulerGevreyMetricEstimate.energyLoss_nonneg (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : 0 ≤ energyLoss period N hN ρ K u

theorem EulerGevreyMetricEstimate.metricAmplification_one_le {c : ℝ} (hc : 0 < c) : 1 ≤ metricAmplification c

theorem EulerGevreyMetricEstimate.weightedNorm_le_energy (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (c : ℝ) (hc : 0 < c) (hK : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (K v) v) : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u ≤ metricAmplification c * energyNorm period N hN ρ K u

Every actual retained Sobolev block is bounded by the metric energy with the fixed factor.

theorem EulerGevreyMetricEstimate.weightedLoss_le_energy (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (c : ℝ) (hc : 0 < c) (hK : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (K v) v) : EulerSobolevTransportCommutator.weightedLoss period 6 N ρ u ≤ metricAmplification c * energyLoss period N hN ρ K u

The actual radius-loss sum obeys the identical fixed metric conversion.

theorem EulerGevreyMetricEstimate.metric_polynomial_conversion (S0 S1 S2 D R B a E Y X Z H : ℝ) (hS1 : 0 ≤ S1) (hS2 : 0 ≤ S2) (hD : 0 ≤ D) (hB : 0 ≤ B) (ha : 1 ≤ a) (hE0 : 0 ≤ E) (hY0 : 0 ≤ Y) (hX0 : 0 ≤ X) (hE : E ≤ a * X) (hY : Y ≤ a * Z) (hH : H ≤ S0 * R + S1 * E + S2 * E ^ 2 + D * (B + E) * Y) : H ≤ S0 * R + S1 * a * X + S2 * a ^ 2 * X ^ 2 + D * a ^ 2 * (B + X) * Z

Exact scalar conversion of a Sobolev forcing polynomial to metric energy and metric radius loss.

noncomputable def EulerGevreyMetricEstimate.metricVelocityBound (period : ℝ) [Fact (0 < period)] (c B X : ℝ) : NNReal

A concrete pointwise velocity bound determined by the actual metric energy.

Equations

• EulerGevreyMetricEstimate.metricVelocityBound period c B X = (EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 6 * (B + EulerGevreyMetricEstimate.metricAmplification c * X)).toNNReal

theorem EulerGevreyMetricEstimate.velocity_ae_metric (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (z e : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (c B : ℝ) (hc : 0 < c) (hK : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (K v) v) (hz : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ z ≤ B) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period (z + e)) x‖ ≤ ↑(metricVelocityBound period c B (energyNorm period N hN ρ K e))

The actual background-plus-error velocity satisfies the fixed-order bound used by the metric PDE estimate.