Leray Assembly Momentum #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.lerayAssembly_momentum_four_terms
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
(A B C P : ℕ → α → ℝ)
(a b c p : α → ℝ)
(hA : ∀ (n : ℕ), MeasureTheory.Integrable (A n) μ)
(hB : ∀ (n : ℕ), MeasureTheory.Integrable (B n) μ)
(hC : ∀ (n : ℕ), MeasureTheory.Integrable (C n) μ)
(hP : ∀ (n : ℕ), MeasureTheory.Integrable (P n) μ)
(ha : MeasureTheory.Integrable a μ)
(hb : MeasureTheory.Integrable b μ)
(hc : MeasureTheory.Integrable c μ)
(hp : MeasureTheory.Integrable p μ)
(hAc : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), A n x ∂μ) Filter.atTop (nhds (∫ (x : α), a x ∂μ)))
(hBc : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), B n x ∂μ) Filter.atTop (nhds (∫ (x : α), b x ∂μ)))
(hCc : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), C n x ∂μ) Filter.atTop (nhds (∫ (x : α), c x ∂μ)))
(hPc : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), P n x ∂μ) Filter.atTop (nhds (∫ (x : α), p x ∂μ)))
(hreg : ∀ (n : ℕ), ∫ (x : α), -A n x - B n x + C n x - P n x ∂μ = 0)
:
The four terms of the regularized momentum identity pass to their limits separately.