The selected weak pressure gradient of a suitable weak solution slice #

For a suitable weak solution and almost every time s of the one-sided interval J_ρ = (t₀ - ρ², t₀], the local pressure decomposition of the pressure-gradient section writes the slice as p₁ + p_har + (p₇ + p₈) on the inner ball B_{13ρ/20}(x₀). Differentiating the three summands separately — the first by the Calderón–Zygmund selection applied to the divergence-form source, the second classically on B_{ρ/2}(x₀), the third by its own potential identities — produces the slice field of display (3.5).

The harmonic term is taken from the interior gradient display, whose ρ^{-3} weight becomes the ρ^{-1/2} weight of display (3.5) once it is integrated over the half ball.

source

theorem CKN.Core.Step4.locallyIntegrableOn_of_memLp_three_halves {g : Foundation.Parabolic.Vec3 → ℝ} {x₀ : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ r))) :

MeasureTheory.LocallyIntegrableOn g (euclideanBall x₀ r) MeasureTheory.volume

A slice which lies in L^{3/2} of a ball of finite measure is locally integrable there. This is the regularity of the force potentials which display (3.5) uses before their weak derivatives are taken.

source

∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (k : Fin 3), MeasureTheory.eLpNorm (fun (x : Vec 3) => classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p s) x k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal (C₁₇ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + F s) * ρ ^ (-1 / 2))

The coordinate L^{6/5} bound of the harmonic part of the pressure slice on the half ball, in the ρ^{-1/2} normalization of display (3.5). The input is the interior gradient display of the harmonic remainder.

source

∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), (∀ (k : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k) (euclideanBall z.1 (ρ / 2)) MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ∧ (∀ (k : Fin 3), HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => D x k) ∧ ∀ (k : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => D x k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal C_CZ * ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => V (x, s) i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (C₁₇ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + F s) * ρ ^ (-1 / 2)) + ENNReal.ofReal (Sw s)

Display (3.5) of the pressure-gradient section, on one time slice of a suitable weak solution.

For almost every time of the one-sided interval J_ρ the pressure slice has a Vec3-valued weak spatial gradient on the half ball B_{ρ/2}(x₀): its coordinates are locally integrable there, it lies in L^{6/5} there, it is the coordinate weak gradient of the slice, and its coordinate norms are bounded by the Calderón–Zygmund norm of the divergence-form source together with the ρ^{-1/2}-weighted L^{3/2} norm of the pressure and the force-potential term.

source

theorem CKN.Core.Step4.exists_scalar_slice_gradient_of_vector_slice {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {K : ℝ → ENNReal} (k : Fin 3) (hD : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), (∀ (j : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x j) B MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ∧ (∀ (j : Fin 3), HasWeakPartialDerivOn B j (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => D x j) ∧ ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => D x j) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ K s) :

∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ K s

The vector-valued slice field of display (3.5) supplies the scalar per-coordinate interface consumed by the space-time measurable selection of the pressure gradient.

Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Step4.SliceSelectedGradient

The selected weak pressure gradient of a suitable weak solution slice #