Local Sobolev Calculus

Supporting estimates for the Navier–Stokes development.

theorem CKN.wordDeriv_append (α : List (Fin 3)) (j : Fin 3) (g : Foundation.Parabolic.Vec3 → ℝ) : wordDeriv (α ++ [j]) g = spatialDeriv (wordDeriv α g) j

Appending a final letter to a derivative word applies that derivative last.

theorem CKN.contDiff_wordDeriv {g : Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (α : List (Fin 3)) : ContDiff ℝ (↑⊤) (wordDeriv α g)

Every ordered derivative of a smooth function is smooth.

theorem CKN.isSobolevFamilyOn_wordDeriv {m : ℕ} {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hL2 : ∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (wordDeriv α g) 2 (MeasureTheory.volume.restrict U)) : IsSobolevFamilyOn m U g fun (α : List (Fin 3)) => wordDeriv α g

A smooth function with square-integrable derivatives gives its classical ordered derivatives as a Sobolev family.

theorem CKN.isSobolevFamilyOn_succ_iff {m : ℕ} {U : Set Foundation.Parabolic.Vec3} {f : Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} : IsSobolevFamilyOn (m + 1) U f D ↔ IsSobolevFamilyOn 0 U f D ∧ ∀ (j : Fin 3), HasWeakPartialDerivOn U j (D []) (D [j]) ∧ IsSobolevFamilyOn m U (D [j]) fun (α : List (Fin 3)) => D (j :: α)

A family through order m + 1 consists of its order-zero family, its first derivatives, and the shifted families through order m.

theorem CKN.IsSobolevFamilyOn.of_le {m m' : ℕ} {U : Set Foundation.Parabolic.Vec3} {f : Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : IsSobolevFamilyOn m U f D) (hm : m' ≤ m) : IsSobolevFamilyOn m' U f D

A Sobolev family restricts to every lower derivative order.

theorem CKN.IsSobolevFamilyOn.mono_set {m : ℕ} {U V : Set Foundation.Parabolic.Vec3} {f : Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : IsSobolevFamilyOn m U f D) (hV : IsOpen V) (hVU : V ⊆ U) : IsSobolevFamilyOn m V f D

A Sobolev family restricts to an open subset of its domain.

theorem CKN.IsSobolevFamilyOn.add {m : ℕ} {U : Set Foundation.Parabolic.Vec3} {f g : Foundation.Parabolic.Vec3 → ℝ} {D E : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (hf : IsSobolevFamilyOn m U f D) (hg : IsSobolevFamilyOn m U g E) : IsSobolevFamilyOn m U (fun (x : Foundation.Parabolic.Vec3) => f x + g x) fun (α : List (Fin 3)) (x : Foundation.Parabolic.Vec3) => D α x + E α x

Sums of Sobolev families are Sobolev families.

theorem CKN.IsSobolevFamilyOn.const_mul {m : ℕ} {U : Set Foundation.Parabolic.Vec3} {f : Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : IsSobolevFamilyOn m U f D) (c : ℝ) : IsSobolevFamilyOn m U (fun (x : Foundation.Parabolic.Vec3) => c * f x) fun (α : List (Fin 3)) (x : Foundation.Parabolic.Vec3) => c * D α x

Scalar multiples of Sobolev families are Sobolev families.

theorem CKN.IsSobolevFamilyOn.congr_ae {m : ℕ} {U : Set Foundation.Parabolic.Vec3} {f f' : Foundation.Parabolic.Vec3 → ℝ} {D D' : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : IsSobolevFamilyOn m U f D) (hf : f =ᵐ[MeasureTheory.volume.restrict U] f') (hD : ∀ (α : List (Fin 3)), α.length ≤ m → D α =ᵐ[MeasureTheory.volume.restrict U] D' α) : IsSobolevFamilyOn m U f' D'

Replacing a Sobolev family by almost-everywhere equal representatives preserves its properties.

theorem CKN.IsSobolevFamilyOn.ae_eq {m : ℕ} {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {f : Foundation.Parabolic.Vec3 → ℝ} {D D' : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : IsSobolevFamilyOn m U f D) (h' : IsSobolevFamilyOn m U f D') (α : List (Fin 3)) : α.length ≤ m → D α =ᵐ[MeasureTheory.volume.restrict U] D' α

Weak derivative families of one function agree almost everywhere on an open set.

theorem CKN.IsSobolevFamilyOn.of_tendsto {m : ℕ} {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {Dn : ℕ → List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (n : ℕ), IsSobolevFamilyOn m U (Dn n []) (Dn n)) (hD : ∀ (α : List (Fin 3)), α.length ≤ m → MeasureTheory.MemLp (D α) 2 (MeasureTheory.volume.restrict U)) (hconv : ∀ (α : List (Fin 3)), α.length ≤ m → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Dn n α - D α) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : IsSobolevFamilyOn m U (D []) D

Limits in L² of Sobolev families remain Sobolev families.

theorem CKN.hNormOn_le {ι : Type u_1} [Fintype ι] {m : ℕ} {U : Set Foundation.Parabolic.Vec3} {f : ι → Foundation.Parabolic.Vec3 → ℝ} {D : ι → List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (i : ι), IsSobolevFamilyOn m U (f i) (D i)) : hNormOn m U f ≤ ENNReal.ofReal √(∑ i : ι, sobolevNormSqOn m U (D i))

The intrinsic Sobolev norm is bounded by the value from any chosen Sobolev family.

theorem CKN.hNormOn_eq {ι : Type u_1} [Fintype ι] {m : ℕ} {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {f : ι → Foundation.Parabolic.Vec3 → ℝ} {D : ι → List (Fin 3) → Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (i : ι), IsSobolevFamilyOn m U (f i) (D i)) : hNormOn m U f = ENNReal.ofReal √(∑ i : ι, sobolevNormSqOn m U (D i))

The intrinsic Sobolev norm is computed by any representing family on an open set.

theorem CKN.hNormOn_lt_top_iff {ι : Type u_1} [Fintype ι] {m : ℕ} {U : Set Foundation.Parabolic.Vec3} {f : ι → Foundation.Parabolic.Vec3 → ℝ} : hNormOn m U f < ⊤ ↔ ∀ (i : ι), MemSobolevOn m U (f i)

A finite Sobolev norm is equivalent to componentwise membership in the Sobolev space.