Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.LerayHopfLimitMomentum

Passage of the regularized transport term to the limit #

This is the nonlinear term passage in the solenoidal weak equation of prop:leray-hopf-limit.

source
theorem CKN.Leray.lerayHopfLimit_momentumIdentity_of_termLimits {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (Aseq : ℕ → α → ℝ) (A : α → ℝ) (Bseq : ℕ → α → ℝ) (B : α → ℝ) (Cseq : ℕ → α → ℝ) (C : α → ℝ) (hAseq : ∀ (n : ℕ), MeasureTheory.Integrable (Aseq n) μ) (hA : MeasureTheory.Integrable A μ) (hBseq : ∀ (n : ℕ), MeasureTheory.Integrable (Bseq n) μ) (hB : MeasureTheory.Integrable B μ) (hCseq : ∀ (n : ℕ), MeasureTheory.Integrable (Cseq n) μ) (hC : MeasureTheory.Integrable C μ) (hAconv : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), Aseq n x ∂μ) Filter.atTop (nhds (∫ (x : α), A x ∂μ))) (hBconv : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), Bseq n x ∂μ) Filter.atTop (nhds (∫ (x : α), B x ∂μ))) (hCconv : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), Cseq n x ∂μ) Filter.atTop (nhds (∫ (x : α), C x ∂μ))) (hreg : ∀ (n : ℕ), ∫ (x : α), -Aseq n x - Bseq n x + Cseq n x ∂μ = 0) :
∫ (x : α), -A x - B x + C x ∂μ = 0

Separate convergence of the linear, transport, and viscous terms passes a regularized solenoidal momentum identity to the limit.

source
theorem CKN.Leray.lerayHopfLimit_linearTerm_tendsto {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (U : ℕ → α → Fin 3 → ℝ) (u : α → Fin 3 → ℝ) (hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 μ) Filter.atTop (nhds 0)) (φ : Fin 3 → α → ℝ) (hφ : ∀ (i : Fin 3), MeasureTheory.MemLp (φ i) ⊤ μ) :
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), ∑ i : Fin 3, U n x i * φ i x ∂μ) Filter.atTop (nhds (∫ (x : α), ∑ i : Fin 3, u x i * φ i x ∂μ))

Strong local L³ convergence passes the linear weak-momentum term to the limit against a bounded test derivative.

source
theorem CKN.Leray.lerayHopfLimit_weakGradientTerm_tendsto {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (D : ℕ → α → Fin 3 → Fin 3 → ℝ) (d : α → Fin 3 → Fin 3 → ℝ) (hD : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (x : α) => D n x i j) 2 μ) (hd : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : α) => d x i j) 2 μ) (hweak : ∀ (i j : Fin 3) (w : α → ℝ), MeasureTheory.MemLp w 2 μ → Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), D n x i j * w x ∂μ) Filter.atTop (nhds (∫ (x : α), d x i j * w x ∂μ))) (φ : Fin 3 → Fin 3 → α → ℝ) (hφ : ∀ (i j : Fin 3), MeasureTheory.MemLp (φ i j) 2 μ) :
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), ∑ i : Fin 3, ∑ j : Fin 3, D n x i j * φ i j x ∂μ) Filter.atTop (nhds (∫ (x : α), ∑ i : Fin 3, ∑ j : Fin 3, d x i j * φ i j x ∂μ))

Weak local L² convergence of the velocity gradients passes their pairing with a test gradient to the limit.

source
theorem CKN.Leray.lerayHopfLimit_advectiveTerm_tendsto {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (U J : ℕ → α → Fin 3 → ℝ) (u : α → Fin 3 → ℝ) (hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) (hJ : ∀ (n : ℕ), MeasureTheory.MemLp (J n) 3 μ) (hu : MeasureTheory.MemLp u 3 μ) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 μ) Filter.atTop (nhds 0)) (hJconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n - u) 3 μ) Filter.atTop (nhds 0)) (φ : Fin 3 → Fin 3 → α → ℝ) (hφ : ∀ (i j : Fin 3), MeasureTheory.MemLp (φ i j) ⊤ μ) :
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), ∑ i : Fin 3, ∑ j : Fin 3, U n x i * J n x j * φ i j x ∂μ) Filter.atTop (nhds (∫ (x : α), ∑ i : Fin 3, ∑ j : Fin 3, u x i * u x j * φ i j x ∂μ))

Strong local L³ convergence of the solution and its mollified transport field passes the transport term to the quadratic limit.

source
theorem CKN.Leray.lerayHopfLimit_weakEquation_of_regularized {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (U J : ℕ → α → Fin 3 → ℝ) (u : α → Fin 3 → ℝ) (D : ℕ → α → Fin 3 → Fin 3 → ℝ) (d : α → Fin 3 → Fin 3 → ℝ) (hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) (hJ : ∀ (n : ℕ), MeasureTheory.MemLp (J n) 3 μ) (hu : MeasureTheory.MemLp u 3 μ) (hUconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 3 μ) Filter.atTop (nhds 0)) (hJconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n - u) 3 μ) Filter.atTop (nhds 0)) (hD : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (x : α) => D n x i j) 2 μ) (hd : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : α) => d x i j) 2 μ) (hweakD : ∀ (i j : Fin 3) (w : α → ℝ), MeasureTheory.MemLp w 2 μ → Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), D n x i j * w x ∂μ) Filter.atTop (nhds (∫ (x : α), d x i j * w x ∂μ))) (dt : Fin 3 → α → ℝ) (hdt : ∀ (i : Fin 3), MeasureTheory.MemLp (dt i) ⊤ μ) (φ : Fin 3 → Fin 3 → α → ℝ) (hφtop : ∀ (i j : Fin 3), MeasureTheory.MemLp (φ i j) ⊤ μ) (hφ2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (φ i j) 2 μ) (hAseq : ∀ (n : ℕ), MeasureTheory.Integrable (fun (x : α) => ∑ i : Fin 3, U n x i * dt i x) μ) (hA : MeasureTheory.Integrable (fun (x : α) => ∑ i : Fin 3, u x i * dt i x) μ) (hBseq : ∀ (n : ℕ), MeasureTheory.Integrable (fun (x : α) => ∑ i : Fin 3, ∑ j : Fin 3, U n x i * J n x j * φ i j x) μ) (hB : MeasureTheory.Integrable (fun (x : α) => ∑ i : Fin 3, ∑ j : Fin 3, u x i * u x j * φ i j x) μ) (hCseq : ∀ (n : ℕ), MeasureTheory.Integrable (fun (x : α) => ∑ i : Fin 3, ∑ j : Fin 3, D n x i j * φ i j x) μ) (hC : MeasureTheory.Integrable (fun (x : α) => ∑ i : Fin 3, ∑ j : Fin 3, d x i j * φ i j x) μ) (hreg : ∀ (n : ℕ), ∫ (x : α), -∑ i : Fin 3, U n x i * dt i x - ∑ i : Fin 3, ∑ j : Fin 3, U n x i * J n x j * φ i j x + ∑ i : Fin 3, ∑ j : Fin 3, D n x i j * φ i j x ∂μ = 0) :
∫ (x : α), -∑ i : Fin 3, u x i * dt i x - ∑ i : Fin 3, ∑ j : Fin 3, u x i * u x j * φ i j x + ∑ i : Fin 3, ∑ j : Fin 3, d x i j * φ i j x ∂μ = 0

The regularized solenoidal momentum identities pass to the limit under the strong velocity and weak gradient convergences in prop:leray-limit.