Pressure Gradient One Sided Origin #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The origin carrier is the backward cylinder. The slice estimate used by the pressure construction is therefore consumed directly on that carrier; there is no symmetric time window in this interface.
Existence interface for a measurable weak pressure gradient with normalized-cylinder cell bounds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Core.Step4.oneSidedPressureGradientOriginScalarSlice_of_vector_slice
{R₀ : ℝ}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{K : ℝ → ENNReal}
(hD :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (-R₀ ^ 2) 0), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (j : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x j) (euclideanBall 0 (R₀ / 2))
MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall 0 (R₀ / 2))) ∧ (∀ (j : Fin 3),
HasWeakPartialDerivOn (euclideanBall 0 (R₀ / 2)) 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 (euclideanBall 0 (R₀ / 2))) ≤ K s)
(j : Fin 3)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (-R₀ ^ 2) 0), ∃ (g : Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.LocallyIntegrableOn g (euclideanBall 0 (R₀ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (euclideanBall 0 (R₀ / 2)) j (fun (x : Vec 3) => p (x, s)) g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall 0 (R₀ / 2))) ≤ K s
theorem
CKN.Core.Step4.oneSidedPressureGradientOriginCellOutput_of_past_slice_bounds
{R₁ κ : ℝ}
{A B : ENNReal}
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hR₁ : 0 < R₁)
(hR₁quarter : R₁ < 3 / 4)
(hκ : 6 / 5 ≤ κ)
(hsmall :
∀ (i : Fin 3),
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ),
0 < r →
r ≤ R₁ →
Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5)
(fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) z r ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ))))
(hglobal :
∀ (i : Fin 3),
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 R₁, ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ B)
:
oneSidedPressureGradientOriginCellOutput R₁ κ (Endgame.oneSidedMorreyBound (6 / 5) κ R₁ A B) Dp