Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RieszPressurePackageSlices

Slice agreement for pressure extensions #

The spatial extensions are independent of exponent on every tensor that is integrable at two exponents. The proof reads them as time slices of extensions of a tensor supported on a finite time interval.

source
noncomputable def CKN.Leray.rieszPressurePackageTimeTensor (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
ℝ

The space-time tensor component restricted to the time interval (0,1) and extended by zero elsewhere.

Equations
Instances For
    source
    theorem CKN.Leray.rieszPressureSlice_ae_eq_of_memLp_common (r : ℝ) (hr : 1 < r) (s : ℝ) (hs : 1 < s) (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hFr : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume) (hFs : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal s) MeasureTheory.volume) :
    ↑↑(rieszPressureSlice r hr fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (F i j) ⋯) =ᵐ[MeasureTheory.volume] ↑↑(rieszPressureSlice s hs fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (F i j) ⋯)
    source
    theorem CKN.Leray.rieszPressureSpaceTime_slice_exponent_agreement (r : ℝ) (hr : 1 < r) (s : ℝ) (hs : 1 < s) (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hFr : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume) (hFs : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal s) MeasureTheory.volume) :
    ∀ᵐ (t : ℝ), ∃ (hFrt : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) (ENNReal.ofReal r) MeasureTheory.volume) (hFst : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) (ENNReal.ofReal s) MeasureTheory.volume), ↑↑(rieszPressureSlice r hr fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) ⋯) =ᵐ[MeasureTheory.volume] ↑↑(rieszPressureSlice s hs fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) ⋯)