Sobolev weights and directional derivatives

The physical domain, embedding constant, and Schwartz derivatives used by the cylinder estimates are independent of Fourier inversion.

@[reducible, inline]

abbrev EulerSobolev.Domain (d : ℕ) : Type

The real Euclidean domain of dimension d.

Equations

• EulerSobolev.Domain d = EuclideanSpace ℝ (Fin d)

noncomputable def EulerSobolev.besselWeight (d : ℕ) (s : ℝ) (ξ : Domain d) : ℝ

The Fourier weight defining the inhomogeneous Sobolev order s.

Equations

• EulerSobolev.besselWeight d s ξ = (1 + ‖ξ‖ ^ 2) ^ (s / 2)

theorem EulerSobolev.besselWeight_temperate (d : ℕ) (s : ℝ) : Function.HasTemperateGrowth (besselWeight d s)

theorem EulerSobolev.besselWeight_pos (d : ℕ) (s : ℝ) (ξ : Domain d) : 0 < besselWeight d s ξ

theorem EulerSobolev.besselWeight_neg_mul (d : ℕ) (s : ℝ) (ξ : Domain d) : besselWeight d (-s) ξ * besselWeight d s ξ = 1

theorem EulerSobolev.besselWeight_add (d : ℕ) (s t : ℝ) (ξ : Domain d) : besselWeight d (s + t) ξ = besselWeight d s ξ * besselWeight d t ξ

theorem EulerSobolev.besselWeight_mul_norm_le (d : ℕ) (s : ℝ) (ξ : Domain d) : besselWeight d s ξ * ‖ξ‖ ≤ besselWeight d (s + 1) ξ

One derivative factor is absorbed by one Sobolev order.

theorem EulerSobolev.reciprocal_weight_memLp (d : ℕ) (s : ℝ) (hs : ↑d < 2 * s) : MeasureTheory.MemLp (besselWeight d (-s)) 2 MeasureTheory.volume

The reciprocal Bessel weight is in L² exactly in the range needed here.

noncomputable def EulerSobolev.reciprocalWeightLp (d : ℕ) (s : ℝ) (hs : ↑d < 2 * s) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The reciprocal Fourier weight represented as a genuine L² element.

Equations

• EulerSobolev.reciprocalWeightLp d s hs = MeasureTheory.MemLp.toLp (EulerSobolev.besselWeight d (-s)) ⋯

noncomputable def EulerSobolev.embeddingConstant (d : ℕ) (s : ℝ) (hs : ↑d < 2 * s) : ℝ

A finite Sobolev embedding constant: the L² norm of the reciprocal weight.

Equations

• EulerSobolev.embeddingConstant d s hs = ‖EulerSobolev.reciprocalWeightLp d s hs‖

noncomputable def EulerSobolevProducts.directional (d n : ℕ) (v : EulerSobolev.Domain d) (f : SchwartzMap (EulerSobolev.Domain d) ℂ) : SchwartzMap (EulerSobolev.Domain d) ℂ

Repeated differentiation in one fixed direction, as a Schwartz function.

Equations

• EulerSobolevProducts.directional d n v f = EulerSobolev.schwartzIteratedDerivative (fun (x : Fin n) => v) f