L² bookkeeping for the vorticity bootstrap

Conversions between L² seminorms and integrals of squares, convergence of integrals of squares, Fubini in the time-outer order on space-time boxes, integrability of smooth functions on bounded sets, the linearity of the coordinate derivatives on smooth functions, and the geometry of the backward kernel balls used in thm:vorticity-regularity of the Escauriaza–Seregin–Šverák manuscript.

theorem CKN.vorticity_eLpNorm_two_eq_sqrt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) : MeasureTheory.eLpNorm f 2 μ = ENNReal.ofReal √(∫ (x : α), f x ^ 2 ∂μ)

The L² seminorm of a square-integrable function is the square root of the integral of its square.

theorem CKN.vorticity_integral_sq_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) : ∫ (x : α), f x ^ 2 ∂μ = (MeasureTheory.eLpNorm f 2 μ).toReal ^ 2

The integral of the square of a square-integrable function is the square of its norm.

theorem CKN.vorticity_tendsto_eLpNorm_of_integral_sq {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {f : ι → α → ℝ} (hf : ∀ (i : ι), MeasureTheory.MemLp (f i) 2 μ) (h : Filter.Tendsto (fun (i : ι) => ∫ (x : α), f i x ^ 2 ∂μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (f i) 2 μ) l (nhds 0)

Integrals of squares tending to zero give L² convergence to zero.

theorem CKN.vorticity_integral_sq_tendsto_zero {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {f : ι → α → ℝ} (hf : ∀ (i : ι), MeasureTheory.MemLp (f i) 2 μ) (h : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (f i) 2 μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ (x : α), f i x ^ 2 ∂μ) l (nhds 0)

L² convergence to zero gives integrals of squares tending to zero.

theorem CKN.vorticity_tendsto_integral_sq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {g : α → ℝ} (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (h : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), f n x ^ 2 ∂μ) Filter.atTop (nhds (∫ (x : α), g x ^ 2 ∂μ))

Integrals of squares are continuous along L² convergence.

theorem CKN.vorticity_integral_sq_sub_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g h : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (hh : MeasureTheory.MemLp h 2 μ) : ∫ (x : α), (f x - g x) ^ 2 ∂μ ≤ 2 * ∫ (x : α), (f x - h x) ^ 2 ∂μ + 2 * ∫ (x : α), (g x - h x) ^ 2 ∂μ

The integral of the square of a difference is controlled by two nearby approximations.

theorem CKN.vorticity_integrableOn_of_continuous_bounded {S : Set (Foundation.Parabolic.Vec3 × ℝ)} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : Continuous g) (hS : Bornology.IsBounded S) : MeasureTheory.IntegrableOn g S MeasureTheory.volume

A continuous function is integrable on a bounded measurable set.

theorem CKN.vorticity_memLp_two_of_continuous_bounded {S : Set (Foundation.Parabolic.Vec3 × ℝ)} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : Continuous g) (hS : Bornology.IsBounded S) : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict S)

A continuous function is square integrable on a bounded set.

theorem CKN.vorticity_setIntegral_prod_time {B : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (B ×ˢ I) MeasureTheory.volume) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ I, f z = ∫ (t : ℝ) in I, ∫ (x : Foundation.Parabolic.Vec3) in B, f (x, t)

On a space-time box, the set integral is the iterated integral with time outside.

theorem CKN.vorticity_spatialPartial_sub {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial (fun (y : Foundation.Parabolic.Vec3 × ℝ) => f y - g y) j z = spatialPartial f j z - spatialPartial g j z

A spatial coordinate derivative of a difference of smooth functions.

theorem CKN.vorticity_timePartial_sub {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial (fun (y : Foundation.Parabolic.Vec3 × ℝ) => f y - g y) z = timePartial f z - timePartial g z

The time derivative of a difference of smooth functions.

theorem CKN.vorticity_spatialSecondPartial_sub {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (j k : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialSecondPartial (fun (y : Foundation.Parabolic.Vec3 × ℝ) => f y - g y) j k z = spatialSecondPartial f j k z - spatialSecondPartial g j k z

A second spatial coordinate derivative of a difference of smooth functions.

theorem CKN.vorticityBackBall_subset {x₀ : Foundation.Parabolic.Vec3} {ρ R a b κ ε : ℝ} (hε : 0 < ε) (hεR : 2 * ε ≤ R - ρ) (hεκ : 6 * ε ≤ κ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ Foundation.Parabolic.vec3Ball x₀ ρ ×ˢ Set.Ioc (a + κ) b) : Metric.closedBall (z - vorticityBackShift ε) ε ⊆ Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b

The backward kernel ball of a point of a slightly smaller box lies in the box.

theorem CKN.vorticityBackMollify_tendsto_restrict {W S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hW : MeasurableSet W) (hS : MeasurableSet S) (hSW : S ⊆ W) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hεpos : ∀ (n : ℕ), 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (vorticityBackMollify W f (ε n) ⋯ - f) 2 (MeasureTheory.volume.restrict S)) Filter.atTop (nhds 0)

Backward mollifications converge in L² on every subset of the domain.