The Fourier H³ norm is controlled by genuine third directional derivatives in L².

theorem EulerSobolevDerivativeNorm.norm_le_sum_coordinates (d : ℕ) (ξ : EulerSobolev.Domain d) : ‖ξ‖ ≤ ∑ i : Fin d, ‖ξ.ofLp i‖

theorem EulerSobolevDerivativeNorm.multilinear_norm_le_coordinate_sum {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (d n : ℕ) (T : EulerSobolev.Domain d [×n]→L[ℝ] F) : ‖T‖ ≤ ∑ w : Fin n → Fin d, ‖T fun (j : Fin n) => EuclideanSpace.single (w j) 1‖

The operator norm of a derivative tensor is bounded by the sum of its coordinate entries.

theorem EulerSobolevDerivativeNorm.besselWeight_one_le_coordinate_sum (d : ℕ) (ξ : EulerSobolev.Domain d) : EulerSobolev.besselWeight d 1 ξ ≤ 1 + ∑ i : Fin d, ‖ξ.ofLp i‖

theorem EulerSobolevDerivativeNorm.besselWeight_three_le_pure_three (d : ℕ) (ξ : EulerSobolev.Domain d) : EulerSobolev.besselWeight d 3 ξ ≤ (↑d + 1) ^ 2 * (1 + ∑ i : Fin d, ‖ξ.ofLp i‖ ^ 3)

theorem EulerSobolevDerivativeNorm.sobolevNorm_three_le_pure_derivatives (d : ℕ) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : EulerSobolev.sobolevNorm d 3 f ≤ (↑d + 1) ^ 2 * (‖f.toLp 2 MeasureTheory.volume‖ + (2 * Real.pi) ^ (-3) * ∑ i : Fin d, ‖(EulerSobolevProducts.directional d 3 (EuclideanSpace.single i 1) f).toLp 2 MeasureTheory.volume‖)

theorem EulerSobolevDerivativeNorm.pointwise_le_L2_third_derivatives (f : SchwartzMap (EulerSobolev.Domain 4) ℂ) (x : EulerSobolev.Domain 4) : ‖f x‖ ≤ EulerSobolev.embeddingConstant 4 3 pointwise_le_L2_third_derivatives._proof_1 * 25 * (‖f.toLp 2 MeasureTheory.volume‖ + (2 * Real.pi) ^ (-3) * ∑ i : Fin 4, ‖(EulerSobolevProducts.directional 4 3 (EuclideanSpace.single i 1) f).toLp 2 MeasureTheory.volume‖)

Four-dimensional Sobolev embedding stated solely with actual L² derivative norms.