Integer Sobolev spaces H^m(U) on open subsets of ℝ³

The local Sobolev space H^m(U) = W^{m,2}(U) used in lem:local-heat-gain and lem:local-div-curl of the Escauriaza–Seregin–Šverák manuscript, and lem:vorticity-products of that manuscript. It consists of the functions in L²(U) whose weak partial derivatives through order m lie in L²(U).

A derivative of order k is indexed by an ordered word α = [j₁, …, j_k] of coordinate directions, and denotes ∂_{j_k} ⋯ ∂_{j₁}: the first letter is applied first. A Sobolev family of f through order m on U is a map D from words to functions such that D [] is f, every D α with α.length ≤ m is square integrable on U, and D (α ++ [j]) is the weak j-th partial derivative of D α on U. The squared norm is the sum of ∫_U (D α)² over all words of length at most m, each ordered word counted once. Since Σ_{|α| = k} |ξ^α|² = |ξ|^{2k} over ordered words, this is the integer Sobolev norm Σ_{k ≤ m} ‖∇^k f‖²_{L²(U)}.

For a fixed f, weak derivatives on an open set are unique almost everywhere, so the norm does not depend on the family. The intrinsic norm hNormOn is the infimum over families, with value ⊤ when f ∉ H^m(U), for a finite family of components indexed by a finite type (scalar, vector or tensor fields).

A time-dependent field in L²(I; H^m(U)) is represented by a jointly square integrable family of its spatial distributional derivatives on U × I.

def CKN.sobolevWords (m : ℕ) : Finset (List (Fin 3))

The ordered derivative words of length at most m.

Equations

• CKN.sobolevWords m = (Finset.range (m + 1)).biUnion fun (k : ℕ) => Finset.image List.ofFn Finset.univ

theorem CKN.mem_sobolevWords {m : ℕ} {α : List (Fin 3)} : α ∈ sobolevWords m ↔ α.length ≤ m

A word lies in sobolevWords m exactly when its length is at most m.

def CKN.wordDeriv : List (Fin 3) → (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ

The classical derivative along a word, wordDeriv [j₁, …, j_k] f = ∂_{j_k} ⋯ ∂_{j₁} f.

Equations

• CKN.wordDeriv [] x✝ = x✝
• CKN.wordDeriv (j :: α) x✝ = CKN.wordDeriv α (CKN.spatialDeriv x✝ j)

structure CKN.IsSobolevFamilyOn (m : ℕ) (U : Set Foundation.Parabolic.Vec3) (f : Foundation.Parabolic.Vec3 → ℝ) (D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ) : Prop

D is a Sobolev family of f through order m on U: D [] is f almost everywhere on U, each D α with α.length ≤ m is in L²(U), and D (α ++ [j]) is the weak j-th partial derivative of D α on U.

• zero : D [] =ᵐ[MeasureTheory.volume.restrict U] f
• memL2 (α : List (Fin 3)) : α.length ≤ m → MeasureTheory.MemLp (D α) 2 (MeasureTheory.volume.restrict U)
• weak (α : List (Fin 3)) (j : Fin 3) : α.length < m → HasWeakPartialDerivOn U j (D α) (D (α ++ [j]))

noncomputable def CKN.sobolevNormSqOn (m : ℕ) (U : Set Foundation.Parabolic.Vec3) (D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ) : ℝ

The squared H^m(U) norm of a Sobolev family: the sum of the squared L²(U) norms of all ordered derivatives through order m.

Equations

• CKN.sobolevNormSqOn m U D = ∑ α ∈ CKN.sobolevWords m, ∫ (x : CKN.Foundation.Parabolic.Vec3) in U, D α x ^ 2

def CKN.MemSobolevOn (m : ℕ) (U : Set Foundation.Parabolic.Vec3) (f : Foundation.Parabolic.Vec3 → ℝ) : Prop

Membership in H^m(U).

Equations

• CKN.MemSobolevOn m U f = ∃ (D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.IsSobolevFamilyOn m U f D

noncomputable def CKN.hNormOn {ι : Type u_1} [Fintype ι] (m : ℕ) (U : Set Foundation.Parabolic.Vec3) (f : ι → Foundation.Parabolic.Vec3 → ℝ) : ENNReal

The H^m(U) norm of a field with finitely many components, indexed by ι: the infimum of (Σ_i ‖D_i‖²_{H^m(U)})^{1/2} over Sobolev families D_i of the components, and ⊤ if some component is not in H^m(U).

Equations

• One or more equations did not get rendered due to their size.

def CKN.vecComponents (v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Fin 3 → Foundation.Parabolic.Vec3 → ℝ

The components of a vector field, as the argument of hNormOn.

Equations

• CKN.vecComponents v i x = v x i

def CKN.tensorSquareComponents (v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Fin 3 × Fin 3 → Foundation.Parabolic.Vec3 → ℝ

The components of the tensor product v ⊗ v, as the argument of hNormOn.

Equations

• CKN.tensorSquareComponents v ij x = v x ij.1 * v x ij.2

structure CKN.IsL2SobolevFamilyOn (m : ℕ) (U : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (z : Foundation.Parabolic.Vec3 × ℝ → ℝ) (D : List (Fin 3) → Foundation.Parabolic.Vec3 × ℝ → ℝ) : Prop

z ∈ L²(I; H^m(U)), with derivative family D: each D α with α.length ≤ m is square integrable on U × I, D [] is z almost everywhere on U × I, and D (α ++ [j]) is the distributional j-th spatial derivative of D α on U × I. A field in L²(U × I) whose spatial distributional derivatives through order m are in L²(U × I) is exactly an element of L²(I; H^m(U)).

• memL2 (α : List (Fin 3)) : α.length ≤ m → MeasureTheory.MemLp (D α) 2 (MeasureTheory.volume.restrict (U ×ˢ I))
• zero : D [] =ᵐ[MeasureTheory.volume.restrict (U ×ˢ I)] z
• weak (α : List (Fin 3)) (j : Fin 3) : α.length < m → ∀ (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U ×ˢ I → ∫ (p : Foundation.Parabolic.Vec3 × ℝ) in U ×ˢ I, D α p * spatialPartial φ j p = -∫ (p : Foundation.Parabolic.Vec3 × ℝ) in U ×ˢ I, D (α ++ [j]) p * φ p

noncomputable def CKN.l2SobolevNormSqOn (m : ℕ) (U : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (D : List (Fin 3) → Foundation.Parabolic.Vec3 × ℝ → ℝ) : ℝ

The squared L²(I; H^m(U)) norm of a space-time derivative family.

Equations

• CKN.l2SobolevNormSqOn m U I D = ∑ α ∈ CKN.sobolevWords m, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in U ×ˢ I, D α p ^ 2

def CKN.IsHeatSolutionOn (U : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (z G : Foundation.Parabolic.Vec3 × ℝ → ℝ) : Prop

z solves ∂ₜ z - Δ z = G in distributions on U × I.

Equations

• One or more equations did not get rendered due to their size.

def CKN.IsWeakDivCurlOn (U : Set Foundation.Parabolic.Vec3) (v ζ : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Prop

div v = 0 and curl v = ζ in distributions on U, where (curl v)_k = ∂_{k+1} v_{k+2} - ∂_{k+2} v_{k+1} with indices mod 3.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.isHeatSolutionOn_zero (U : Set Foundation.Parabolic.Vec3) (I : Set ℝ) : IsHeatSolutionOn U I (fun (x : Foundation.Parabolic.Vec3 × ℝ) => 0) fun (x : Foundation.Parabolic.Vec3 × ℝ) => 0

The zero field solves the homogeneous heat equation.

theorem CKN.isWeakDivCurlOn_zero (U : Set Foundation.Parabolic.Vec3) : IsWeakDivCurlOn U (fun (x : Foundation.Parabolic.Vec3) => 0) fun (x : Foundation.Parabolic.Vec3) => 0

The zero field is divergence free with zero curl.

theorem CKN.memSobolevOn_zero (m : ℕ) (U : Set Foundation.Parabolic.Vec3) : MemSobolevOn m U fun (x : Foundation.Parabolic.Vec3) => 0

The zero function lies in every H^m(U).