Fixed-base pointwise and metric-loss control by actual finite Gevrey norms.

theorem EulerGevreyLowNorms.weightedNorm_mono (period : ℝ) [Fact (0 < period)] {s p q : ℕ} (hpq : p ≤ q) (N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerSobolevGevreyOperators.weightedNorm period p N ρ u ≤ EulerSobolevGevreyOperators.weightedNorm period q N ρ u

Monotonicity in the fixed base Sobolev index.

theorem EulerGevreyLowNorms.restrict_norm_le_weighted (period : ℝ) [Fact (0 < period)] {s q : ℕ} (N : ℕ) (hq : q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ‖(EulerCylinderSobolevSpace.restrictOperator period hq) u‖ ≤ EulerSobolevGevreyOperators.weightedNorm period q N ρ u

The actual base Sobolev norm is contained in every nonempty truncated weighted sum.

theorem EulerGevreyLowNorms.value_ae_weighted (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hs : 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period u) x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 6 * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u

The actual pointwise bound has a constant depending only on the fixed base order six, never on the external cutoff.

theorem EulerGevreyLowNorms.metricLoss_eq (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedMetricLoss ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) K (EulerGevreyMetricComparison.energyValues period q N hN u) = ∑ n : Fin (N + 1), ↑↑n * EulerPacketWeights.weight ρ ↑n * ∑ w : Fin ↑n → Fin 4, EulerBaseWordMetric.baseWordMetricNorm period K (EulerH6Pressure.SpatialJet.derivativeJet (EulerCylinderSobolevSpace.toJet period u) w ⋯)

The exact metric radius-loss sum in fixed-base word notation.

theorem EulerGevreyLowNorms.weightedLoss_metric_lower (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ 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 q N ρ u ≤ √↑(Fintype.card (EulerBaseWordMetric.BaseWord q)) / c * EulerWeightedCylinderEnergy.weightedMetricLoss ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) K (EulerGevreyMetricComparison.energyValues period q N hN u)

The actual derivative-loss Sobolev sum is controlled by metric roots with only the fixed base-order constant.