The actual complete Sobolev product obeys the finite Gevrey H⁶ algebra bound, including nonsmooth inputs.

@[instance_reducible]

noncomputable def EulerSobolevGevreyProduct.gevreySobolevGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevGevreyProduct.gevreySobolevGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevGevreyProduct.gevreySobolevSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevGevreyProduct.gevreySobolevSpace period q = inferInstance

theorem EulerSobolevGevreyProduct.continuous_blockNorm (period : ℝ) [Fact (0 < period)] {s q n : ℕ} (h : n + q ≤ s) : Continuous fun (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) => EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) q n

The external Hq block is a continuous function of the actual finite Sobolev class.

theorem EulerSobolevGevreyProduct.continuous_weighted_blockNorm (period : ℝ) [Fact (0 < period)] {s q : ℕ} (N : ℕ) (h : N + q ≤ s) (ρ : ℝ) : Continuous fun (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) => ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) q n

Every truncated weighted block norm is continuous on its genuine Sobolev domain.

theorem EulerSobolevGevreyProduct.product_weighted_bound_smooth (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)) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period (EulerSobolevL2Product.productHq period hs L hL u v)) 6 n ≤ (EulerH6Nonlinear.productConstant period 3 * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) 6 n) * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period v) 6 n

On actual smooth H∞ representatives, the complete product has the cutoff-independent weighted H⁶ bound.

theorem EulerSobolevGevreyProduct.continuous_product (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) : Continuous fun (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s) × ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) => EulerSobolevL2Product.productHq period hs L hL p.1 p.2

Continuity of the actual product in both finite-Sobolev inputs.

theorem EulerSobolevGevreyProduct.product_weighted_bound (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)) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period (EulerSobolevL2Product.productHq period hs L hL u v)) 6 n ≤ (EulerH6Nonlinear.productConstant period 3 * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) 6 n) * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period v) 6 n

The cutoff-independent Gevrey product bound holds for actual finite Sobolev inputs, by genuine H∞ approximation and continuity.