Actual Fourier Sobolev estimates on Euclidean spaces. The Sobolev norm below is the L² norm of (1 + |ξ|²)^(s/2) 𝓕f(ξ), so its relation to the represented function is explicit. All estimates are proved from inversion and Hölder.

noncomputable def EulerSobolev.weightedFourier {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d : ℕ) (s : ℝ) (f : SchwartzMap (Domain d) F) : SchwartzMap (Domain d) F

The Fourier transform multiplied by the Sobolev weight.

Equations

• EulerSobolev.weightedFourier d s f = (SchwartzMap.smulLeftCLM F (EulerSobolev.besselWeight d s)) (EulerSobolev.schwartzFourier f)

theorem EulerSobolev.weightedFourier_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d : ℕ) (s : ℝ) (f : SchwartzMap (Domain d) F) (ξ : Domain d) : (weightedFourier d s f) ξ = besselWeight d s ξ • (schwartzFourier f) ξ

noncomputable def EulerSobolev.sobolevNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d : ℕ) (s : ℝ) (f : SchwartzMap (Domain d) F) : ℝ

The inhomogeneous Fourier Hˢ norm of a Schwartz function.

Equations

• EulerSobolev.sobolevNorm d s f = ‖(EulerSobolev.weightedFourier d s f).toLp 2 MeasureTheory.volume‖

theorem EulerSobolev.norm_apply_le_fourier_L1 {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (d : ℕ) (f : SchwartzMap (Domain d) F) (x : Domain d) : ‖f x‖ ≤ ‖(schwartzFourier f).toLp 1 MeasureTheory.volume‖

Fourier inversion bounds a Schwartz function pointwise by the L¹ norm of its transform.

theorem EulerSobolev.fourier_L1_le_sobolevNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d : ℕ) (s : ℝ) (hs : ↑d < 2 * s) (f : SchwartzMap (Domain d) F) : ‖(schwartzFourier f).toLp 1 MeasureTheory.volume‖ ≤ embeddingConstant d s hs * sobolevNorm d s f

Hölder with the reciprocal weight converts the Fourier L¹ norm into the Hˢ norm.

theorem EulerSobolev.norm_apply_le_sobolevNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (d : ℕ) (s : ℝ) (hs : ↑d < 2 * s) (f : SchwartzMap (Domain d) F) (x : Domain d) : ‖f x‖ ≤ embeddingConstant d s hs * sobolevNorm d s f

A genuine pointwise Sobolev embedding for every s > d/2.

theorem EulerSobolev.fourier_lineDeriv_norm_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d : ℕ) (f : SchwartzMap (Domain d) F) (m ξ : Domain d) : ‖(schwartzFourier (schwartzDerivative m f)) ξ‖ ≤ 2 * Real.pi * ‖ξ‖ * ‖m‖ * ‖(schwartzFourier f) ξ‖

The actual Fourier multiplier formula bounds each directional derivative.

theorem EulerSobolev.weightedFourier_lineDeriv_norm_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d : ℕ) (s : ℝ) (f : SchwartzMap (Domain d) F) (m ξ : Domain d) : ‖(weightedFourier d s (schwartzDerivative m f)) ξ‖ ≤ 2 * Real.pi * ‖m‖ * ‖(weightedFourier d (s + 1) f) ξ‖

theorem EulerSobolev.sobolevNorm_lineDeriv_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d : ℕ) (s : ℝ) (f : SchwartzMap (Domain d) F) (m : Domain d) : sobolevNorm d s (schwartzDerivative m f) ≤ 2 * Real.pi * ‖m‖ * sobolevNorm d (s + 1) f

A directional derivative maps H^(s+1) to H^s with its explicit Fourier factor.

theorem EulerSobolev.sobolevNorm_iteratedLineDeriv_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (d k : ℕ) (s : ℝ) (f : SchwartzMap (Domain d) F) (m : Fin k → Domain d) : sobolevNorm d s (schwartzIteratedDerivative m f) ≤ ((2 * Real.pi) ^ k * ∏ i : Fin k, ‖m i‖) * sobolevNorm d (s + ↑k) f

Iterating the Fourier multiplier estimate loses exactly one Sobolev order per derivative.

theorem EulerSobolev.iteratedFDeriv_norm_le_sobolevNorm {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (d k : ℕ) (s : ℝ) (hs : ↑d < 2 * s) (f : SchwartzMap (Domain d) F) (x : Domain d) : ‖iteratedFDeriv ℝ k (⇑f) x‖ ≤ embeddingConstant d s hs * (2 * Real.pi) ^ k * sobolevNorm d (s + ↑k) f

Sobolev embedding controls the operator norm of every actual Fréchet derivative.

noncomputable def EulerSobolev.complexify (q : ℕ) : Domain q →ₗᵢ[ℝ] EuclideanSpace ℂ (Fin q)

Coordinatewise complexification is an actual linear isometry of Euclidean spaces.

Equations

• EulerSobolev.complexify q = { toFun := fun (x : EulerSobolev.Domain q) => WithLp.toLp 2 fun (i : Fin q) => ↑(x.ofLp i), map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

noncomputable def EulerSobolev.complexifySchwartz (d q : ℕ) (f : SchwartzMap (Domain d) (Domain q)) : SchwartzMap (Domain d) (EuclideanSpace ℂ (Fin q))

Coordinatewise isometric complexification of a real Schwartz vector field.

Equations

• EulerSobolev.complexifySchwartz d q f = (SchwartzMap.postcompCLM (EulerSobolev.complexify q).toContinuousLinearMap) f

noncomputable def EulerSobolev.realSobolevNorm (d q : ℕ) (s : ℝ) (f : SchwartzMap (Domain d) (Domain q)) : ℝ

The usual Fourier Hˢ norm of a real vector field, via isometric complexification.

Equations

• EulerSobolev.realSobolevNorm d q s f = EulerSobolev.sobolevNorm d s (EulerSobolev.complexifySchwartz d q f)

theorem EulerSobolev.complexifySchwartz_iteratedFDeriv_norm (d q k : ℕ) (f : SchwartzMap (Domain d) (Domain q)) (x : Domain d) : ‖iteratedFDeriv ℝ k (⇑(complexifySchwartz d q f)) x‖ = ‖iteratedFDeriv ℝ k (⇑f) x‖

theorem EulerSobolev.real_iteratedFDeriv_norm_le_sobolevNorm (d q k : ℕ) (s : ℝ) (hs : ↑d < 2 * s) (f : SchwartzMap (Domain d) (Domain q)) (x : Domain d) : ‖iteratedFDeriv ℝ k (⇑f) x‖ ≤ embeddingConstant d s hs * (2 * Real.pi) ^ k * realSobolevNorm d q (s + ↑k) f

Sobolev embedding for genuine real Euclidean vector fields and all derivative orders.

theorem EulerSobolev.real_three_dimensional_sobolev (q k : ℕ) (f : SchwartzMap (Domain 3) (Domain q)) (x : Domain 3) : ‖iteratedFDeriv ℝ k (⇑f) x‖ ≤ embeddingConstant 3 2 real_three_dimensional_sobolev._proof_1 * (2 * Real.pi) ^ k * realSobolevNorm 3 q (2 + ↑k) f

On ℝ³, H^(k+2) controls every derivative of order k. In particular, H³ → C¹.

theorem EulerSobolev.real_four_dimensional_sobolev (q k : ℕ) (f : SchwartzMap (Domain 4) (Domain q)) (x : Domain 4) : ‖iteratedFDeriv ℝ k (⇑f) x‖ ≤ embeddingConstant 4 3 real_four_dimensional_sobolev._proof_1 * (2 * Real.pi) ^ k * realSobolevNorm 4 q (3 + ↑k) f

On ℝ⁴, H^(k+3) controls every derivative of order k.

noncomputable def EulerSobolev.compactSobolevNorm (d q : ℕ) (s : ℝ) (f : Domain d → Domain q) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : ℝ

The same concrete Fourier norm, now for an unbundled smooth compactly supported field.

Equations

• EulerSobolev.compactSobolevNorm d q s f hf hc = EulerSobolev.realSobolevNorm d q s (hc.toSchwartzMap hf)

theorem EulerSobolev.compact_iteratedFDeriv_norm_le (q k : ℕ) (f : Domain 3 → Domain q) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) (x : Domain 3) : ‖iteratedFDeriv ℝ k f x‖ ≤ embeddingConstant 3 2 real_three_dimensional_sobolev._proof_1 * (2 * Real.pi) ^ k * compactSobolevNorm 3 q (2 + ↑k) f hf hc

theorem EulerSobolev.smooth_compact_solenoidal_limit_of_sobolev (f : ℕ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hc : ∀ (n : ℕ), HasCompactSupport (f n)) (hSob : ∀ (k : ℕ), Summable fun (n : ℕ) => compactSobolevNorm 3 3 (2 + ↑k) (f n) ⋯ ⋯) (K : Set EulerSmoothLimit.Space) (hK : IsCompact K) (hsupp : ∀ (n : ℕ), Function.support (f n) ⊆ K) (hdiv : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (f n) x = 0) : ∃ (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space), (∀ (x : EulerSmoothLimit.Space), HasSum (fun (n : ℕ) => f n x) (u x)) ∧ TendstoUniformly (fun (N : ℕ) (x : EulerSmoothLimit.Space) => ∑ n ∈ Finset.range N, f n x) u Filter.atTop ∧ ContDiff ℝ (↑⊤) u ∧ tsupport u ⊆ K ∧ HasCompactSupport u ∧ MeasureTheory.MemLp u 2 MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => ‖u x‖ ^ 2) MeasureTheory.volume ∧ (∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence u x = 0) ∧ ∀ (k : ℕ) (x : EulerSmoothLimit.Space), iteratedFDeriv ℝ k u x = ∑' (n : ℕ), iteratedFDeriv ℝ k (f n) x

The all-order Sobolev estimates construct the actual smooth, compactly supported, finite-energy solenoidal limit. Uniform derivative bounds are derived by Fourier analysis inside the proof, rather than supplied as an additional hypothesis.