Compactness Ball Pairing

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.inner_toLp_vec3_eq_integral_dot (f g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, (f x).ofLp i * (g x).ofLp i

The real Hilbert pairing of vector-valued L² functions is the integral of their coordinatewise dot product.

theorem CKN.Leray.inner_cutoff_vec3_eq_integral_dot (u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (χ : Foundation.Parabolic.Vec3 → ℝ) (ψ : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3) (hf : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u x)) 2 MeasureTheory.volume) (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) : inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u x)) hf) (MeasureTheory.MemLp.toLp ψ hψ) = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u x i * (χ x • ψ x).ofLp i

Moving a scalar cutoff between the field and test leaves the spatial Hilbert pairing unchanged.

theorem CKN.Leray.inner_indicator_basis_eq_integral_component {B : Set Foundation.Parabolic.Vec3} (hB : MeasurableSet B) (hBfinite : MeasureTheory.volume B < ⊤) (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (i : Fin 3) : inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.indicatorConstLp 2 hB ⋯ (WithLp.toLp 2 (Pi.single i 1))) = ∫ (x : Foundation.Parabolic.Vec3) in B, (f x).ofLp i

The indicator of a finite-measure set paired with a vector L² field recovers the integral of one coordinate on that set.

theorem CKN.Leray.average_component_eq_scaled_inner {B : Set Foundation.Parabolic.Vec3} (hB : MeasurableSet B) (hBfinite : MeasureTheory.volume B < ⊤) (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (i : Fin 3) : ⨍ (x : Foundation.Parabolic.Vec3) in B, (f x).ofLp i = (MeasureTheory.volume B).toReal⁻¹ * inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.indicatorConstLp 2 hB ⋯ (WithLp.toLp 2 (Pi.single i 1)))

A ball coordinate average is a fixed Hilbert pairing multiplied by the inverse volume.

theorem CKN.Leray.average_vec3_component_eq_cutoff_pairing {B : Set Foundation.Parabolic.Vec3} (hB : MeasurableSet B) (hBfinite : MeasureTheory.volume B < ⊤) (u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ x ∈ B, χ x = 1) (hf : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u x)) 2 MeasureTheory.volume) (i : Fin 3) : ⨍ (x : Foundation.Parabolic.Vec3) in B, u x i = (MeasureTheory.volume B).toReal⁻¹ * inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u x)) hf) (MeasureTheory.indicatorConstLp 2 hB ⋯ (WithLp.toLp 2 (Pi.single i 1)))

If a cutoff is one on a finite-measure set, the original field's coordinate average is a Hilbert pairing with the cutoff field.

theorem CKN.Leray.eventually_uniform_vec3_of_uniform_pairings {T : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : ℕ → T → E) (v : T → E) (ψ : Fin 3 → E) (c : ℝ) (hc : 0 ≤ c) (hpair : ∀ (i : Fin 3) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : T), dist (inner ℝ (u n t) (ψ i)) (inner ℝ (v t) (ψ i)) < ε) (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : T), Foundation.Parabolic.vec3EuclideanNorm ((fun (i : Fin 3) => c * inner ℝ (u n t) (ψ i)) - fun (i : Fin 3) => c * inner ℝ (v t) (ψ i)) ≤ ε

Uniform convergence of three Hilbert pairings gives uniform convergence of the associated vector of coefficients.

theorem CKN.Leray.vec3_norm_pairings_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (ψ : Fin 3 → E) (c C : ℝ) (hc : 0 ≤ c) (hC : ‖v‖ ≤ C) : (Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => c * inner ℝ v (ψ i)) ≤ c * C * ∑ i : Fin 3, ‖ψ i‖

A bound on a Hilbert vector bounds any three fixed scalar pairings assembled into a vector.

theorem CKN.Leray.eventually_uniform_vec3_ball_averages {I J : Set ℝ} (hJI : J ⊆ I) {B : Set Foundation.Parabolic.Vec3} (hB : MeasurableSet B) (hBfinite : MeasureTheory.volume B < ⊤) (u : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ x ∈ B, χ x = 1) (hmem : ∀ (n : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u n (x, ↑t))) 2 MeasureTheory.volume) (V : ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (huniform : ∀ (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : ℝ) (ht : t ∈ J), dist (inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, t))) ⋯) x) (inner ℝ (V ⟨t, ⋯⟩) x) < ε) (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : ℝ) (ht : t ∈ J), Foundation.Parabolic.vec3EuclideanNorm ((fun (i : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in B, u n (y, t) i) - fun (i : Fin 3) => (MeasureTheory.volume B).toReal⁻¹ * inner ℝ (V ⟨t, ⋯⟩) (MeasureTheory.indicatorConstLp 2 hB ⋯ (WithLp.toLp 2 (Pi.single i 1)))) ≤ ε

Uniform weak convergence of cutoff slices gives uniform convergence of the three coordinate averages on a set where the cutoff equals one.