Compactness Gradient Coordinates #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.weak_gradient_coordinate_integrals
{μ : MeasureTheory.Measure (Foundation.Parabolic.Vec3 × ℝ)}
(Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3)
(D : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 μ))
(hmem :
∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du k z)) 2 μ)
(hweak :
∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 μ)),
Filter.Tendsto
(fun (k : ℕ) =>
inner ℝ
(MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du k z)) ⋯)
w)
Filter.atTop (nhds (inner ℝ D w)))
(i j : Fin 3)
(w : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hw : MeasureTheory.MemLp w 2 μ)
:
Filter.Tendsto (fun (k : ℕ) => ∫ (z : Foundation.Parabolic.Vec3 × ℝ), Du k z i j * w z ∂μ) Filter.atTop
(nhds (∫ (z : Foundation.Parabolic.Vec3 × ℝ), (gradientCoordinateCLM i j) (↑↑D z) * w z ∂μ))
A weak L² limit of the matrix gradient gives weak convergence of
each scalar gradient coordinate against all L² tests.
theorem
CKN.Leray.weak_gradient_coordinate_integrals_on_subrectangle
{K Ω : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hΩ : IsOpen Ω)
(hΩK : Ω ⊆ K)
(hJ : MeasurableSet J)
(Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3)
(D :
↥(MeasureTheory.Lp CompactnessGradientFiber 2
((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))))
(hmem :
∀ (k : ℕ),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du k z)) 2
((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)))
(hweak :
∀
(v :
↥(MeasureTheory.Lp CompactnessGradientFiber 2
((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)))),
Filter.Tendsto
(fun (k : ℕ) =>
inner ℝ
(MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du k z)) ⋯)
v)
Filter.atTop (nhds (inner ℝ D v)))
(i j : Fin 3)
(w : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hw : MeasureTheory.MemLp w 2 ((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)))
:
Filter.Tendsto
(fun (k : ℕ) =>
∫ (z : Foundation.Parabolic.Vec3 × ℝ), Du k z i j * w z ∂(MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J))
Filter.atTop
(nhds
(∫ (z : Foundation.Parabolic.Vec3 × ℝ), (gradientCoordinateCLM i j) (↑↑D z) * w z ∂(MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)))
The coordinate pairings restrict from a compact rectangle to an open spatial subrectangle by extending each test by zero.