Compactness Finite Rank #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.lintegral_vec3_ball_average_error_le_of_field_energy
{U : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
(hr : 0 < r)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(huMeas : Measurable u)
(hDuMeas : Measurable Du)
(huenergy :
∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in U, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 2 < ⊤)
(hweak :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u (x, t) i) fun (x : Vec 3) => Du (x, t) i)
(henergy : ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in U, ENNReal.ofReal (spatialGradientSq u Du (x, t)) < ⊤)
(hball : euclideanBall x₀ r ⊆ U)
:
∫⁻ (t : ℝ) in J, ∫⁻ (x : Vec 3) in euclideanBall x₀ r, ENNReal.ofReal
(Foundation.Parabolic.vec3EuclideanNorm
(u (x, t) - fun (i : Fin 3) => ⨍ (y : Vec 3) in euclideanBall x₀ r, u (y, t) i) ^ 2) ≤ 3 * (sobolevPoincareL6Constant * MeasureTheory.volume (euclideanBall x₀ r) ^ (1 / 3)) ^ 2 * ∫⁻ (t : ℝ) in J, ∫⁻ (x : Vec 3) in euclideanBall x₀ r, ENNReal.ofReal (spatialGradientSq u Du (x, t))
The field-level scalar Poincaré estimates control the vector error from a ball average by the space-time gradient energy on that ball.
theorem
CKN.Leray.lintegral_vec3_finite_rank_average_error_le_of_field_energy
{ι : Type u_1}
[Fintype ι]
{U : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{K : Set Foundation.Parabolic.Vec3}
{x : ι → Foundation.Parabolic.Vec3}
{r : ℝ}
(hr : 0 < r)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(huMeas : Measurable u)
(hDuMeas : Measurable Du)
(huenergy :
∫⁻ (t : ℝ) in J, ∫⁻ (y : Foundation.Parabolic.Vec3) in U, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (y, t))) ^ 2 < ⊤)
(hweak :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn U (fun (y : Vec 3) => u (y, t) i) fun (y : Vec 3) => Du (y, t) i)
(henergy : ∫⁻ (t : ℝ) in J, ∫⁻ (y : Foundation.Parabolic.Vec3) in U, ENNReal.ofReal (spatialGradientSq u Du (y, t)) < ⊤)
(hK : MeasurableSet K)
(hJ : MeasurableSet J)
(φ : ι → Foundation.Parabolic.Vec3 → ℝ)
(hφ : ∀ (i : ι), Measurable (φ i))
(hweight : ∀ (i : ι) (y : Foundation.Parabolic.Vec3), 0 ≤ φ i y ∧ φ i y ≤ 1)
(hsum : ∀ y ∈ K, ∑ i : ι, φ i y = 1)
(hcover : ∀ (i : ι), euclideanBall (x i) r ⊆ U)
(hsupport : ∀ (i : ι) (y : Foundation.Parabolic.Vec3), φ i y ≠ 0 → y ∈ euclideanBall (x i) r)
:
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, ENNReal.ofReal
(Foundation.Parabolic.vec3EuclideanNorm
(u z - ∑ i : ι, φ i z.1 • fun (j : Fin 3) => ⨍ (y : Vec 3) in euclideanBall (x i) r, u (y, z.2) j) ^ 2) ≤ ∑ i : ι,
3 * (sobolevPoincareL6Constant * MeasureTheory.volume (euclideanBall (x i) r) ^ (1 / 3)) ^ 2 * ∫⁻ (t : ℝ) in J, ∫⁻ (y : Vec 3) in euclideanBall (x i) r, ENNReal.ofReal (spatialGradientSq u Du (y, t))
The finite-rank approximation error is bounded by the sum of the space-time gradient energies on the balls of the cover.
theorem
CKN.Leray.lintegral_vec3_finite_rank_average_error_le_of_colored_cover
{ι : Type u_1}
[Fintype ι]
{N : ℕ}
{U : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{K : Set Foundation.Parabolic.Vec3}
{r : ℝ}
(hr : 0 < r)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(huMeas : Measurable u)
(hDuMeas : Measurable Du)
(huenergy :
∫⁻ (t : ℝ) in J, ∫⁻ (y : Foundation.Parabolic.Vec3) in U, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (y, t))) ^ 2 < ⊤)
(hweak :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn U (fun (y : Vec 3) => u (y, t) i) fun (y : Vec 3) => Du (y, t) i)
(henergy : ∫⁻ (t : ℝ) in J, ∫⁻ (y : Foundation.Parabolic.Vec3) in U, ENNReal.ofReal (spatialGradientSq u Du (y, t)) < ⊤)
(hK : MeasurableSet K)
(hJ : MeasurableSet J)
(x : ι → Foundation.Parabolic.Vec3)
(color : ι → Fin N)
(φ : ι → Foundation.Parabolic.Vec3 → ℝ)
(hφ : ∀ (i : ι), Measurable (φ i))
(hweight : ∀ (i : ι) (y : Foundation.Parabolic.Vec3), 0 ≤ φ i y ∧ φ i y ≤ 1)
(hsum : ∀ y ∈ K, ∑ i : ι, φ i y = 1)
(hball : ∀ (i : ι), euclideanBall (x i) r ⊆ U)
(hsupport : ∀ (i : ι) (y : Foundation.Parabolic.Vec3), φ i y ≠ 0 → y ∈ euclideanBall (x i) r)
(hdisjoint : ∀ (i j : ι), i ≠ j → color i = color j → Disjoint (euclideanBall (x i) r) (euclideanBall (x j) r))
:
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, ENNReal.ofReal
(Foundation.Parabolic.vec3EuclideanNorm
(u z - ∑ i : ι, φ i z.1 • fun (j : Fin 3) => ⨍ (y : Vec 3) in euclideanBall (x i) r, u (y, z.2) j) ^ 2) ≤ 3 * (sobolevPoincareL6Constant * MeasureTheory.volume (euclideanBall 0 r) ^ (1 / 3)) ^ 2 * ∑ _j : Fin N,
∫⁻ (t : ℝ) in J, ∫⁻ (y : Foundation.Parabolic.Vec3) in U, ENNReal.ofReal (spatialGradientSq u Du (y, t))
Combining the ball Poincaré estimate with a bounded-overlap coloring gives a uniform error bound for the finite-rank average on the compact region.
theorem
CKN.Leray.lintegral_vec3_finite_rank_average_error_le_of_mixed_bounds
{ι : Type u_1}
[Fintype ι]
{N : ℕ}
{W Kc K : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{r : ℝ}
(hr : 0 < r)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(huMeas : Measurable u)
(hDuMeas : Measurable Du)
(hweak :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), HasWeakGradientOn W (fun (y : Vec 3) => u (y, t) i) fun (y : Vec 3) => Du (y, t) i)
(hJ : MeasurableSet J)
[MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)]
(M G : ENNReal)
(hM : M < ⊤)
(hG : G < ⊤)
(hWKc : W ⊆ Kc)
(huBound :
∀ t ∈ J,
∫⁻ (x : Foundation.Parabolic.Vec3) in Kc, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 2 ≤ M)
(hDuBound :
∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in Kc, ENNReal.ofReal (spatialGradientSq u Du (x, t)) ≤ G)
(hK : MeasurableSet K)
(x : ι → Foundation.Parabolic.Vec3)
(color : ι → Fin N)
(φ : ι → Foundation.Parabolic.Vec3 → ℝ)
(hφ : ∀ (i : ι), Measurable (φ i))
(hweight : ∀ (i : ι) (y : Foundation.Parabolic.Vec3), 0 ≤ φ i y ∧ φ i y ≤ 1)
(hsum : ∀ y ∈ K, ∑ i : ι, φ i y = 1)
(hball : ∀ (i : ι), euclideanBall (x i) r ⊆ W)
(hsupport : ∀ (i : ι) (y : Foundation.Parabolic.Vec3), φ i y ≠ 0 → y ∈ euclideanBall (x i) r)
(hdisjoint : ∀ (i j : ι), i ≠ j → color i = color j → Disjoint (euclideanBall (x i) r) (euclideanBall (x j) r))
:
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in K ×ˢ J, ENNReal.ofReal
(Foundation.Parabolic.vec3EuclideanNorm
(u z - ∑ i : ι, φ i z.1 • fun (j : Fin 3) => ⨍ (y : Vec 3) in euclideanBall (x i) r, u (y, z.2) j) ^ 2) ≤ 3 * (sobolevPoincareL6Constant * MeasureTheory.volume (euclideanBall 0 r) ^ (1 / 3)) ^ 2 * ∑ _j : Fin N,
∫⁻ (t : ℝ) in J, ∫⁻ (y : Foundation.Parabolic.Vec3) in W, ENNReal.ofReal (spatialGradientSq u Du (y, t))
The finite-rank estimate uses a uniform velocity slice bound and an integrated gradient bound, as in the local compactness hypothesis.