Pressure Gradient One Sided #

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The slice interface used by the one-sided pressure estimate. The outer ball is the region on which the slice weak derivative is supplied; the norm bound is recorded on the inner half-ball exactly as in display (3.5).

source

def CKN.Core.Step4.pressureGradientOneScaleAt (C_CZ R₀ : ℝ) (V : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (t : ℝ) :

Prop

One-time-slice weak pressure gradient and its local Calderón–Zygmund estimate.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CKN.Core.Step4.pressureGradientOneScaleBound {J : Set ℝ} (C_CZ R₀ : ℝ) (V : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) :

Prop

Almost-everywhere-in-time version of the one-scale pressure-gradient estimate.

Equations

CKN.Core.Step4.pressureGradientOneScaleBound C_CZ R₀ V p = ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, CKN.Core.Step4.pressureGradientOneScaleAt C_CZ R₀ V p t

Instances For

A slice bound gives product integrability once its time majorant is integrable. The spatial finite-measure factor is retained explicitly; this is the factor supplied by the bounded inner ball in the application.

source

theorem CKN.Core.Step4.pressure_gradient_integrable_on_of_slice_bound {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {f : Foundation.Parabolic.ParabolicPoint → ℝ} {K : ℝ → ENNReal} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict B)] (hfmeas : MeasureTheory.AEStronglyMeasurable f ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))) (hslice : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ K t) (hKtop : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, K t ≠ ⊤) (hKint : MeasureTheory.Integrable (fun (t : ℝ) => (K t).toReal) (MeasureTheory.volume.restrict J)) :

MeasureTheory.Integrable f ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))

source

theorem CKN.Core.Step4.pressure_gradient_integrable_on_of_selected_bounds {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {K : Fin 3 → ℝ → ENNReal} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict B)] (hDpmeas : ∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))) (hbound : ∀ (i : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Dp (x, t) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ K i t) (hKtop : ∀ (i : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, K i t ≠ ⊤) (hKint : ∀ (i : Fin 3), MeasureTheory.Integrable (fun (t : ℝ) => (K i t).toReal) (MeasureTheory.volume.restrict J)) (i : Fin 3) :

MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J))

The pressure factor needed by the selector is locally integrable on every compact solution box. The spatial set may be any subset of the box, which is the form used after the fixed-radius cutoff is intersected with a local box.

source

MeasureTheory.IntegrableOn p (B ×ˢ J) MeasureTheory.volume

The quantitative target is recorded with constants before the fields. The local-integrability conjunct is the interface used by localized equation representations on arbitrary sub-boxes.

source

noncomputable def CKN.Core.Step4.oneSidedPressureGradientKP (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) :

ENNReal

Quantitative Morrey bound assembled from velocity, gradient, forcing and harmonic remainders.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CKN.Core.Step4.oneSidedPressureGradientKP_lt_top (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) :

25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → ∀ (hKU : KU < ⊤) (hKD : KD < ⊤), oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD < ⊤

source

def CKN.Core.Step4.oneSidedPressureGradientQuantitative :

Prop

Uniform quantitative pressure-gradient conclusion on the prescribed range of Morrey exponents.

Equations

One or more equations did not get rendered due to their size.

Instances For

This wrapper exposes the numerical call used by Theorem A. It retains the pressure field on the returned support and normalizes only the Morrey exponent arithmetic.

source

theorem CKN.Core.Step4.initial_pressure_gradient_of_quantitative (hGA : oneSidedPressureGradientQuantitative) (q C_CZ ε₀ : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) (hC : 0 ≤ C_CZ) (hε₀ : 0 ≤ ε₀) (hKU : KU < ⊤) (hKD : KD < ⊤) :

Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Step4.PressureGradientOneSided

Pressure Gradient One Sided #