Compactness Finite Rank Core

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.finite_lintegral_prod_of_uniform_slice_bound {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (f : Foundation.Parabolic.ParabolicPoint → ENNReal) (hf : Measurable f) (hJ : MeasurableSet J) [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)] (B : ENNReal) (hB : B < ⊤) (hslice : ∀ t ∈ J, ∫⁻ (x : Foundation.Parabolic.Vec3) in K, f (x, t) ≤ B) : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in K, f (x, t) < ⊤

A uniform finite spatial integral on each time slice gives a finite space-time integral on a finite time window.

theorem CKN.Leray.lintegral_parabolic_rectangle_eq_iterated {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (f : Foundation.Parabolic.ParabolicPoint → ENNReal) (hf : Measurable f) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, f z = ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in K, f (x, t)

Integrating on a spatial-time rectangle agrees with the iterated Lebesgue integral in time and then space.

theorem CKN.Leray.vec3_norm_sq_sub_finite_rank_average_le {ι : Type u_1} [Fintype ι] (K : Set Foundation.Parabolic.Vec3) (φ : ι → Foundation.Parabolic.Vec3 → ℝ) (a : ι → ℝ → Foundation.Parabolic.Vec3) (u x : Foundation.Parabolic.Vec3) (t : ℝ) (hweight : ∀ (i : ι) (y : Foundation.Parabolic.Vec3), 0 ≤ φ i y ∧ φ i y ≤ 1) (hsum : x ∈ K → ∑ i : ι, φ i x = 1) (hx : x ∈ K) : Foundation.Parabolic.vec3EuclideanNorm (u - ∑ i : ι, φ i x • a i t) ^ 2 ≤ ∑ i : ι, φ i x * Foundation.Parabolic.vec3EuclideanNorm (u - a i t) ^ 2

Pointwise error for a finite-rank spatial approximation assembled from local averages with a measurable partition of unity.

theorem CKN.Leray.lintegral_error_le_sum_of_supported_terms {α : Type u_1} {β : Type u_2} {ι : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype ι] {μ : MeasureTheory.Measure (α × β)} (K : Set α) (J : Set β) (B : ι → Set α) (e : α × β → ENNReal) (q : ι → α × β → ENNReal) (hK : MeasurableSet K) (hJ : MeasurableSet J) (hB : ∀ (i : ι), MeasurableSet (B i)) (hpoint : ∀ z ∈ K ×ˢ J, e z ≤ ∑ i : ι, q i z) (hsupport : ∀ (i : ι), ∀ z ∉ B i ×ˢ Set.univ, q i z = 0) (hq : ∀ (i : ι), Measurable (q i)) : ∫⁻ (z : α × β) in K ×ˢ J, e z ∂μ ≤ ∑ i : ι, ∫⁻ (z : α × β) in B i ×ˢ J, q i z ∂μ

A pointwise finite-rank error bound integrates to the sum of the local errors when each summand vanishes outside its assigned spatial set.

theorem CKN.Leray.lintegral_vec3_finite_rank_average_error_le {ι : Type u_1} [Fintype ι] {μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint} (J : Set ℝ) (K : Set Foundation.Parabolic.Vec3) (B : ι → Set Foundation.Parabolic.Vec3) (φ : ι → Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (a : ι → ℝ → Foundation.Parabolic.Vec3) (hJ : MeasurableSet J) (hK : MeasurableSet K) (hB : ∀ (i : ι), MeasurableSet (B i)) (hφ : ∀ (i : ι), Measurable (φ i)) (hu : Measurable u) (ha : ∀ (i : ι), Measurable (a i)) (hweight : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), 0 ≤ φ i x ∧ φ i x ≤ 1) (hsum : ∀ x ∈ K, ∑ i : ι, φ i x = 1) (hsupport : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), φ i x ≠ 0 → x ∈ B i) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z - ∑ i : ι, φ i z.1 • a i z.2) ^ 2) ∂μ ≤ ∑ i : ι, ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in B i ×ˢ J, ENNReal.ofReal (φ i z.1 * Foundation.Parabolic.vec3EuclideanNorm (u z - a i z.2) ^ 2) ∂μ

The measurable finite-rank average error is bounded by the sum of its local ball errors. The weights form a partition on the compact region and each weight is supported in its assigned ball.

theorem CKN.Leray.lintegral_vec3_finite_rank_average_error_le_unweighted {ι : Type u_1} [Fintype ι] {μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint} (J : Set ℝ) (K : Set Foundation.Parabolic.Vec3) (B : ι → Set Foundation.Parabolic.Vec3) (φ : ι → Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (a : ι → ℝ → Foundation.Parabolic.Vec3) (hJ : MeasurableSet J) (hK : MeasurableSet K) (hB : ∀ (i : ι), MeasurableSet (B i)) (hφ : ∀ (i : ι), Measurable (φ i)) (hu : Measurable u) (ha : ∀ (i : ι), Measurable (a i)) (hweight : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), 0 ≤ φ i x ∧ φ i x ≤ 1) (hsum : ∀ x ∈ K, ∑ i : ι, φ i x = 1) (hsupport : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), φ i x ≠ 0 → x ∈ B i) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z - ∑ i : ι, φ i z.1 • a i z.2) ^ 2) ∂μ ≤ ∑ i : ι, ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in B i ×ˢ J, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z - a i z.2) ^ 2) ∂μ

Replacing each weighted local error by its full ball error preserves the finite-rank space-time estimate.

theorem CKN.Leray.tendsto_vec3_ball_poincare_factor_zero : Filter.Tendsto (fun (n : ℕ) => (sobolevPoincareL6Constant * MeasureTheory.volume (euclideanBall 0 (1 / (↑n + 1))) ^ (1 / 3)) ^ 2) Filter.atTop (nhds 0)

The squared Poincare factor for equal-radius spatial balls vanishes with the radius.

theorem CKN.Leray.eventually_small_colored_ball_energy_factor {N : ℕ} (G : ENNReal) (hG : G < ⊤) (ε : ENNReal) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, 3 * (sobolevPoincareL6Constant * MeasureTheory.volume (euclideanBall 0 (1 / (↑n + 1))) ^ (1 / 3)) ^ 2 * ∑ _j : Fin N, G ≤ ε

The integrated finite-rank error coefficient is eventually smaller than any prescribed tolerance when the local gradient energy is uniformly bounded.

theorem CKN.Leray.sum_lintegral_ball_gradient_energy_le_of_coloring {ι : Type u_1} [Fintype ι] {N : ℕ} {U : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (B : ι → Set Foundation.Parabolic.Vec3) (color : ι → Fin N) (f : Foundation.Parabolic.ParabolicPoint → ENNReal) (hB : ∀ (i : ι), MeasurableSet (B i)) (hsubset : ∀ (i : ι), B i ⊆ U) (hdisjoint : ∀ (i j : ι), i ≠ j → color i = color j → Disjoint (B i) (B j)) (hf : Measurable f) : ∑ i : ι, ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in B i, f (x, t) ≤ ∑ _j : Fin N, ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in U, f (x, t)

A finite family of spatial balls split into finitely many disjoint colors has total local gradient energy bounded by the number of colors times the energy on its containing set.