Weighted limits for the Carleman density argument

Finite sums of weak derivative components retain L² convergence, so the weighted quadratic terms in lem:carleman-sobolev of the Escauriaza–Seregin–Šverák manuscript converge on a fixed compact support neighborhood.

theorem carlemanLimitVolumeIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem carlemanLimitVolumeIsAddLeftInvariant : MeasureTheory.volume.IsAddLeftInvariant

theorem CKN.memLp_finset_sum {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {p : ENNReal} {f : ι → X → ℝ} (s : Finset ι) (h : ∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) : MeasureTheory.MemLp (fun (x : X) => ∑ i ∈ s, f i x) p μ

Finite sums of Lᵖ scalar fields remain in Lᵖ (lem:carleman-sobolev, ESS).

theorem CKN.spaceTimeMollify_add_of_memLp {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} (hδ : 0 < δ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : spaceTimeMollify (f + g) δ hδ = spaceTimeMollify f δ hδ + spaceTimeMollify g δ hδ

Space-time mollification is additive for globally L² fields (lem:carleman-sobolev, ESS).

theorem CKN.spaceTimeMollify_finset_sum {ι : Type u_1} {s : Finset ι} {f : ι → Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} (hδ : 0 < δ) (hf : ∀ i ∈ s, MeasureTheory.MemLp (f i) 2 MeasureTheory.volume) : spaceTimeMollify (fun (x : Foundation.Parabolic.Vec3 × ℝ) => ∑ i ∈ s, f i x) δ hδ = fun (x : Foundation.Parabolic.Vec3 × ℝ) => ∑ i ∈ s, spaceTimeMollify (f i) δ hδ x

Space-time mollification commutes with finite sums of globally L² fields (lem:carleman-sobolev, ESS).

theorem CKN.weightedPiSq_integrable {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Fintype ι] {ρ : X → ℝ} {C : ℝ} (hρ : MeasureTheory.AEStronglyMeasurable ρ μ) (hρbound : ∀ᵐ (x : X) ∂μ, ‖ρ x‖ ≤ C) {f : X → ι → ℝ} (hf : ∀ (i : ι), MeasureTheory.MemLp (fun (x : X) => f x i) 2 μ) : MeasureTheory.Integrable (fun (x : X) => ρ x * ∑ i : ι, f x i ^ 2) μ

A bounded measurable coefficient makes a finite weighted sum of L² squares integrable (lem:carleman-sobolev, ESS).

theorem CKN.setIntegral_eq_of_zero_off {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) (hBA : B ⊆ A) {f : X → ℝ} (hzero : ∀ᵐ (x : X) ∂μ, x ∈ A → x ∉ B → f x = 0) : ∫ (x : X) in A, f x ∂μ = ∫ (x : X) in B, f x ∂μ

If an integrand vanishes almost everywhere off a compact subset, its integral reduces to that subset (lem:carleman-sobolev, ESS).

theorem CKN.spaceTimeMollify_memLp_of_memLp {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} (hδ : 0 < δ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (spaceTimeMollify f δ hδ) 2 MeasureTheory.volume

Space-time mollification preserves global L² membership (lem:carleman-sobolev, ESS).

theorem CKN.tendsto_mollify_l2_restrict {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hεpos : ∀ (n : ℕ), 0 < ε n) (S : Set (Foundation.Parabolic.Vec3 × ℝ)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3 × ℝ) => spaceTimeMollify f (ε n) ⋯ x - f x) 2 (MeasureTheory.volume.restrict S)) Filter.atTop (nhds 0)

Global L² convergence of mollifications restricts to every measurable subset (lem:carleman-sobolev, ESS).

theorem CKN.vec3EuclideanNorm_sq (v : Foundation.Parabolic.Vec3) : Foundation.Parabolic.vec3EuclideanNorm v ^ 2 = ∑ i : Fin 3, v i ^ 2

The squared Euclidean norm on Vec3 is the sum of coordinate squares (lem:carleman-sobolev, ESS).

theorem CKN.value_eq_zero_of_tsupport_subset {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hfsupport : tsupport f ⊆ S) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ S) : f z = 0

A scalar field vanishes off any set containing its topological support (lem:carleman-sobolev, ESS).

theorem CKN.fin3_double_sum_eq_product (f : Fin 3 → Fin 3 → ℝ) : ∑ i : Fin 3, ∑ j : Fin 3, f i j = ∑ ij : Fin 3 × Fin 3, f ij.1 ij.2

Two coordinate sums identify with a sum over ordered coordinate pairs (lem:carleman-sobolev, ESS).

theorem CKN.weightedPiSq_tendsto {X : Type u_1} {ι : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Fintype ι] {ρ : X → ℝ} {C : ℝ} (hC : 0 ≤ C) (hρ : MeasureTheory.AEStronglyMeasurable ρ μ) (hρbound : ∀ᵐ (x : X) ∂μ, ‖ρ x‖ ≤ C) {f : X → ι → ℝ} {fseq : ℕ → X → ι → ℝ} (hf : ∀ (i : ι), MeasureTheory.MemLp (fun (x : X) => f x i) 2 μ) (hfseq : ∀ (n : ℕ) (i : ι), MeasureTheory.MemLp (fun (x : X) => fseq n x i) 2 μ) (hconv : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : X) => fseq n x i - f x i) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : X), ρ x * ∑ i : ι, fseq n x i ^ 2 ∂μ) Filter.atTop (nhds (∫ (x : X), ρ x * ∑ i : ι, f x i ^ 2 ∂μ))

Bounded weights preserve convergence of finite sums of componentwise quadratic integrals. This is the mass, gradient, and parabolic residual limit used by lem:carleman-sobolev (ESS).