Actual coefficient and pressure operators on finite weighted Sobolev sums.

noncomputable def EulerSobolevGevreyOperators.weightedNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (ρ : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ℝ

The truncated Gevrey sum of genuine fixed-order Sobolev blocks.

Equations

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

noncomputable def EulerSobolevGevreyOperators.weightedCoefficient (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (q N : ℕ) (ρ : ℝ) : ℝ

Weighted coefficient derivative bounds in the same fixed base norm.

Equations

• EulerSobolevGevreyOperators.weightedCoefficient period K q N ρ = ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.coefficientBlock period K q n

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

theorem EulerSobolevGevreyOperators.weightedCoefficient_nonneg (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (q N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) : 0 ≤ weightedCoefficient period K q N ρ

theorem EulerSobolevGevreyOperators.blockNorm_unique (period : ℝ) [Fact (0 < period)] {s t q n : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) (K : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection t g) (hfg : f = g) (hs : n + q ≤ s) (ht : n + q ≤ t) : EulerH6Pressure.blockNorm period J q n = EulerH6Pressure.blockNorm period K q n

A genuine fixed-order block is independent of the chosen derivative-jet construction.

theorem EulerSobolevGevreyOperators.weightedNorm_add_le (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedNorm period q N ρ (u + v) ≤ weightedNorm period q N ρ u + weightedNorm period q N ρ v

The actual complete Sobolev weighted norm satisfies the triangle inequality at every valid cutoff.

theorem EulerSobolevGevreyOperators.weightedNorm_zero (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) : weightedNorm period q N ρ 0 = 0

The zero Sobolev field has zero weighted energy.

theorem EulerSobolevGevreyOperators.weightedNorm_sum_le (period : ℝ) [Fact (0 < period)] {s : ℕ} {ι : Type u_1} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (S : Finset ι) (u : ι → ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedNorm period q N ρ (∑ i ∈ S, u i) ≤ ∑ i ∈ S, weightedNorm period q N ρ (u i)

The actual finite weighted Sobolev norm is subadditive on finite sums.

theorem EulerSobolevGevreyOperators.weightedNorm_coefficient (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedNorm period q N ρ ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) u) ≤ weightedCoefficient period K q N ρ * weightedNorm period q N ρ u

Actual coefficient multiplication has a cutoff-independent weighted Sobolev bound.

theorem EulerSobolevGevreyOperators.weightedNorm_pressure (period : ℝ) [Fact (0 < period)] {s q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (N : ℕ) (hN : N + q ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (EulerH6Pressure.CoefficientJet.restrict K q ⋯).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K q l ≤ Rc ^ l * ↑l.factorial ^ 2) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedNorm period q N ρ ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) u) ≤ 2 * M * weightedNorm period q N ρ u

The actual coercive pressure operator obeys the unshifted finite Gevrey estimate on complete Sobolev inputs.

theorem EulerSobolevGevreyOperators.weightedNorm_product (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedNorm period 6 N ρ (EulerSobolevL2Product.productHq period hs L hL u v) ≤ EulerH6Nonlinear.productConstant period 3 * weightedNorm period 6 N ρ u * weightedNorm period 6 N ρ v

Actual scalar-component multiplication in finite Gevrey sums.