Radius reduction for actual finite weighted Sobolev norms.

theorem EulerGevreyRadiusReduction.weight_mono_radius {r R : ℝ} (hr : 0 ≤ r) (hR : r ≤ R) (n : ℕ) : EulerPacketWeights.weight r n ≤ EulerPacketWeights.weight R n

theorem EulerGevreyRadiusReduction.weightedNorm_mono_radius (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) {r R : ℝ} (hr : 0 ≤ r) (hR : r ≤ R) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerSobolevGevreyOperators.weightedNorm period q N r u ≤ EulerSobolevGevreyOperators.weightedNorm period q N R u

theorem EulerGevreyRadiusReduction.weightedCoefficient_mono_radius (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (q N : ℕ) {r R : ℝ} (hr : 0 ≤ r) (hR : r ≤ R) : EulerSobolevGevreyOperators.weightedCoefficient period K q N r ≤ EulerSobolevGevreyOperators.weightedCoefficient period K q N R

theorem EulerGevreyRadiusReduction.weightedNorm_mono_cutoff (period : ℝ) [Fact (0 < period)] {s : ℕ} (q : ℕ) {N M : ℕ} (hNM : N ≤ M) (r : ℝ) (hr : 0 < r) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerSobolevGevreyOperators.weightedNorm period q N r u ≤ EulerSobolevGevreyOperators.weightedNorm period q M r u

theorem EulerGevreyRadiusReduction.weightedCoefficient_mono_cutoff (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (q : ℕ) {N M : ℕ} (hNM : N ≤ M) (r : ℝ) (hr : 0 < r) : EulerSobolevGevreyOperators.weightedCoefficient period K q N r ≤ EulerSobolevGevreyOperators.weightedCoefficient period K q M r

theorem EulerGevreyRadiusReduction.weightedNorm_unique (period : ℝ) [Fact (0 < period)] {s t : ℕ} (q N : ℕ) (r : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period t)) (huv : EulerCylinderSobolevSpace.value period u = EulerCylinderSobolevSpace.value period v) (hs : N + q ≤ s) (ht : N + q ≤ t) : EulerSobolevGevreyOperators.weightedNorm period q N r u = EulerSobolevGevreyOperators.weightedNorm period q N r v

A retained weighted norm depends only on the genuine underlying field.

theorem EulerGevreyRadiusReduction.derivative_block_sum (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (hn : n + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : ∑ i : Fin 4, EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period ((EulerCylinderSobolevSpace.derivativeOperator period s i) u)) q n = EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) q (n + 1)

The four actual coordinate derivatives form exactly the next external block.

theorem EulerGevreyRadiusReduction.successor_square_le_four_two_pow (n : ℕ) : ↑(n + 1) ^ 2 ≤ 4 * 2 ^ n

A fixed exponential absorbs the square introduced by one factorial shift.

theorem EulerGevreyRadiusReduction.weight_half_le_shift (R : ℝ) (hR : 0 < R) (n : ℕ) : EulerPacketWeights.weight (R / 2) n ≤ 4 / R * EulerPacketWeights.weight R (n + 1)

theorem EulerGevreyRadiusReduction.weightedNorm_derivative_half (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (R : ℝ) (hR : 0 < R) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period q N (R / 2) ((EulerCylinderSobolevSpace.derivativeOperator period s i) u) ≤ 4 / R * EulerSobolevGevreyOperators.weightedNorm period q (N + 1) R u

Halving the positive radius pays for one full spatial/angular derivative, with no dependence on the external cutoff.