Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.PressureLimitLeray

Pressure convergence in the Leray limit #

The regularized transport tensor converges in L^(3/2) when both velocity factors converge strongly in L³, and the space-time Riesz pressure preserves that convergence on every finite slab (prop:leray-pressure-limit).

source
def CKN.Leray.lerayPressureLimitSlab (T : ℝ) :
Set (Foundation.Parabolic.Vec3 × ℝ)

The product-coordinate space-time region corresponding to the interval (0,T) in the Leray pressure limit (prop:leray-pressure-limit).

Equations
Instances For
    source
    noncomputable def CKN.Leray.lerayProductPressureOnSlab (T : ℝ) (v w : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hv : MeasureTheory.MemLp v 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hw : MeasureTheory.MemLp w 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) :
    Foundation.Parabolic.Vec3 × ℝ → ℝ

    The canonical space-time Riesz pressure on a finite slab, formed from the product of two L³ velocity fields.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CKN.Leray.lerayPressureLimit_Lthree (T : ℝ) (Jseq useq : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hJseq : ∀ (n : ℕ), MeasureTheory.MemLp (Jseq n) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (huseq : ∀ (n : ℕ), MeasureTheory.MemLp (useq n) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hu : MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hJconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Jseq n - u) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) Filter.atTop (nhds 0)) (huconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (useq n - u) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) Filter.atTop (nhds 0)) :
      Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (lerayProductPressureOnSlab T (Jseq n) (useq n) ⋯ ⋯ - lerayProductPressureOnSlab T u u hu hu) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) Filter.atTop (nhds 0)

      The regularized Leray pressures converge strongly in L^(3/2) on each finite time slab under the exact strong L³ velocity convergences in prop:leray-limit.