structure SchwartzWeightedSobolev.WeightedSobolevSpace (n k : ℕ) : Type

The k-th weighted Sobolev space on ℝⁿ: a structure recording an underlying Sobolev representative, used to model functions f such that ⟨x⟩^k · f ∈ H^k.

• witness : SobolevEmbedding.SobolevSpace n k

noncomputable def SchwartzWeightedSobolev.WeightedSobolevSpace.toFun {n k : ℕ} (u : WeightedSobolevSpace n k) (x : EuclideanSpace ℝ (Fin n)) : ℂ

The underlying function of a WeightedSobolevSpace n k element: divide the Sobolev witness by ⟨x⟩^k so that the witness's Hᵏ regularity translates into pointwise ⟨x⟩^k-decay of the original function.

@[implicit_reducible]

noncomputable instance SchwartzWeightedSobolev.instCoeFunWeightedSobolevSpaceForallEuclideanSpaceRealFinComplex {n k : ℕ} : CoeFun (WeightedSobolevSpace n k) fun (x : WeightedSobolevSpace n k) => EuclideanSpace ℝ (Fin n) → ℂ

Coercion that lets an element of WeightedSobolevSpace n k be applied as a function EuclideanSpace ℝ (Fin n) → ℂ.

structure SchwartzWeightedSobolev.MemAllWeightedSobolev (n : ℕ) : Type

Bundle of a function lying in every weighted Sobolev space, with a consistent family of weighted Sobolev witnesses.

• toFun : EuclideanSpace ℝ (Fin n) → ℂ
• mem_weighted (k : ℕ) : WeightedSobolevSpace n k
• consistent (k : ℕ) (x : EuclideanSpace ℝ (Fin n)) : self.toFun x = (self.mem_weighted k).toFun x

@[implicit_reducible]

instance SchwartzWeightedSobolev.instCoeFunMemAllWeightedSobolevForallEuclideanSpaceRealFinComplex {n : ℕ} : CoeFun (MemAllWeightedSobolev n) fun (x : MemAllWeightedSobolev n) => EuclideanSpace ℝ (Fin n) → ℂ

Coercion that lets an element of MemAllWeightedSobolev n be applied as a function EuclideanSpace ℝ (Fin n) → ℂ.

theorem SchwartzWeightedSobolev.schwartz_ck_iteratedFDeriv_memLp {n : ℕ} (u : TestFunctions.SchwartzTestFunctionSpace n) (k j : ℕ) (hj : j ≤ k) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j (fun (x : EuclideanSpace ℝ (Fin n)) => ⋯.choose.witnessV.toZeroAtInftyContinuousMap x) x) 2 MeasureTheory.volume

The iterated Fréchet derivatives (up to order k) of the Cᵏ witness of a Schwartz test function lie in L² with respect to Lebesgue measure.

noncomputable def SchwartzWeightedSobolev.schwartzToSobolev {n : ℕ} (u : TestFunctions.SchwartzTestFunctionSpace n) (k : ℕ) : { s : SobolevEmbedding.SobolevSpace n k // s.toFun = fun (x : EuclideanSpace ℝ (Fin n)) => ⋯.choose.witnessV.toZeroAtInftyContinuousMap x }

From a Schwartz test function u, extract a Hᵏ Sobolev representative (for every k) by taking the weighted Cᵏ-witness's underlying function.

noncomputable def SchwartzWeightedSobolev.schwartzToAllWeightedSobolev {n : ℕ} (u : TestFunctions.SchwartzTestFunctionSpace n) : { w : MemAllWeightedSobolev n // w.toFun = u.toFun }

A Schwartz test function lies in every weighted Sobolev space, with underlying function equal to the original Schwartz function.

noncomputable def SchwartzWeightedSobolev.schwartzToAllWeightedSobolev' {n : ℕ} (u : TestFunctions.SchwartzTestFunctionSpace n) : MemAllWeightedSobolev n

Plain version of schwartzToAllWeightedSobolev discarding the proof of the pointwise consistency identity.

def SchwartzWeightedSobolev.allWeightedSobolevToSchwartz {n : ℕ} (w : MemAllWeightedSobolev n) : { u : TestFunctions.SchwartzTestFunctionSpace n // u.toFun = w.toFun }

Converse direction: a function lying in every weighted Sobolev space is a Schwartz test function (and has the same underlying function).

def SchwartzWeightedSobolev.allWeightedSobolevToSchwartz' {n : ℕ} (w : MemAllWeightedSobolev n) : TestFunctions.SchwartzTestFunctionSpace n

Plain version of allWeightedSobolevToSchwartz discarding the proof of the pointwise identity.

def SchwartzWeightedSobolev.IsSchwartz (n : ℕ) (f : EuclideanSpace ℝ (Fin n) → ℂ) : Prop

A function f : ℝⁿ → ℂ is Schwartz if it arises as the underlying function of some element of SchwartzTestFunctionSpace n.

def SchwartzWeightedSobolev.IsInAllWeightedSobolev (n : ℕ) (f : EuclideanSpace ℝ (Fin n) → ℂ) : Prop

A function f : ℝⁿ → ℂ lies in every weighted Sobolev space if it arises as the underlying function of some MemAllWeightedSobolev n.