noncomputable def SobolevDuality.sobolevWeight (n : ℕ) (s : ℝ) (ξ : EuclideanSpace ℝ (Fin n)) : ℝ

The Sobolev weight ⟨ξ⟩^s = (1 + |ξ|²)^(s/2) on the dual variable ξ, used to define the Sobolev space H^s via the Fourier transform.

theorem SobolevDuality.sobolevWeight_pos (n : ℕ) (s : ℝ) (ξ : EuclideanSpace ℝ (Fin n)) : 0 < sobolevWeight n s ξ

The Sobolev weight is strictly positive everywhere.

def SobolevDuality.MemHs (n : ℕ) (s : ℝ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Prop

Membership in the Sobolev space H^s of order s: a tempered distribution u belongs to H^s if its Fourier transform 𝓕 u is represented (against Schwartz test functions) by an L² function divided by the Sobolev weight ⟨ξ⟩^s.

def SobolevDuality.Hs (n : ℕ) (s : ℝ) : Type

The Sobolev space H^s as the subtype of tempered distributions satisfying MemHs.

noncomputable def SobolevDuality.dualIdentification (n : ℕ) (s : ℝ) : SobolevSpace.Hs n (-s) ≃ₗᵢ⋆[ℂ] SobolevSpace.Hs n s →L[ℂ] ℂ

Proposition 9.8 (Sobolev duality): the antilinear isometric isomorphism H^{-s} ≃ (H^s)* identifying the Sobolev space of order -s with the continuous dual of H^s.