Genuine L∞ control of finite-order cylinder Sobolev fields, obtained by smooth density.

noncomputable def EulerCylinderSobolevSpace.sobolevEmbeddingConstant (period : ℝ) [Fact (0 < period)] (q : ℕ) : ℝ

A fixed-order embedding constant for the complete finite-array Sobolev norm.

Equations

• EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q = 3 * EulerCylinderSobolev.cylinderEmbeddingConstant period * ↑(Fintype.card (EulerCylinderSobolevSpace.SobolevWord q))

theorem EulerCylinderSobolevSpace.sobolevEmbeddingConstant_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) : 0 ≤ sobolevEmbeddingConstant period q

theorem EulerCylinderSobolevSpace.mollifier_pointwise_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (n : ℕ) (u : ↥(SobolevSpace period q)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerMollifierRepresentative.smoothMollifier period n (value period u) x‖ ≤ sobolevEmbeddingConstant period q * ‖u‖

Every actual smooth mollification has the same uniform pointwise Sobolev bound.

theorem EulerCylinderSobolevSpace.value_ae_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (u : ↥(SobolevSpace period q)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(value period u) x‖ ≤ sobolevEmbeddingConstant period q * ‖u‖

Every actual Hq field, q≥3, has an almost-everywhere bounded L² representative.