Documentation

LeanPool.CaffarelliKohnNirenberg.Core.Step4.PressureGradientOriginBSlotInstancesCollar

The collar slice bound for the whole-carrier pressure gradient #

On a collar Q(z, ρ) inside the unit data cylinder of thm:A, every weak slice derivative of the pressure on the half ball B(z₁, ρ/2) is, by eq:pressure-gradient-decomposition, the sum of three completed Riesz terms built from the localized source, one smooth remainder gradient, and three completed Riesz terms built from the localized force. This file turns that identification into a slice inequality between L^{6/5} norms in which the localized source and the localized force have been replaced by majorants that no longer depend on the component index.

No velocity or gradient Morrey datum enters any estimate in this file.

The localized force slice is dominated in L^{6/5} by the force slice on the collar ball, uniformly in the component index.

theorem CKN.Core.Step4.collar_slice_gradient_eLpNorm_le {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q C : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) (hrem : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) x i‖ₑ ≤ fixedRemainderSliceMajorant C ρ z.1 u f p s) (D : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hD : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => D (y, s) i) (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => D (y, s) i) :

The collar slice bound of eq:pressure-gradient-decomposition. On the half ball of a collar inside the domain, every weak slice derivative of the pressure has L^{6/5} norm at most three times the Calderón–Zygmund constant applied to the centred source majorant, plus the smooth remainder majorant weighted by the half-ball volume, plus three times the same constant applied to the force slice norm on the collar ball.

theorem CKN.Core.Step4.time_mass_of_three_slice_bounds {J : Set ℝ} {N G M H : ℝ → ENNReal} {K W EG EM EH : ENNReal} (hG : AEMeasurable G (MeasureTheory.volume.restrict J)) (hM : AEMeasurable M (MeasureTheory.volume.restrict J)) (hH : AEMeasurable H (MeasureTheory.volume.restrict J)) (hK : K ≠ ⊤) (hW : W ≠ ⊤) (hN : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, N s ≤ K * G s + M s * W ^ (5 / 6) + K * H s) (hEG : ∫⁻ (s : ℝ) in J, G s ^ (6 / 5) ≤ EG) (hEM : ∫⁻ (s : ℝ) in J, M s ^ (6 / 5) ≤ EM) (hEH : ∫⁻ (s : ℝ) in J, H s ^ (6 / 5) ≤ EH) :
∫⁻ (s : ℝ) in J, N s ^ (6 / 5) ≤ 4 * (K ^ (6 / 5) * EG + W * EM + K ^ (6 / 5) * EH)

A slice bound of the shape produced by eq:pressure-gradient-decomposition turns three separate time masses into one, with the numerical factor of the three-term power split.

noncomputable def CKN.Core.Step4.bslotCollarConstant (C ρ : ℝ) :

The explicit absolute coefficient of the collar time mass of prop:bootstrap. Every factor is a fixed function of the collar radius and of the harmonic remainder constant; none depends on the force exponent, on the Morrey exponent, on the radii of the carrier, on the data size, or on the solution.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem CKN.Core.Step4.collar_gradient_time_mass_le (C ε : ℝ) (hε : 0 ≤ ε) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hsmall : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : 2 * ρ ≤ 1) (hW : MeasureTheory.volume (Foundation.Parabolic.vec3Ball 0 ρ) ≤ 1) (hQ : Foundation.Parabolic.parabolicCylinder z.1 z.2 (2 * ρ) ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1) (hrem : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) x i‖ₑ ≤ fixedRemainderSliceMajorant C ρ z.1 u f p s) (D : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hD : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => D (y, s) i) (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => D (y, s) i) (i : Fin 3) :

    The collar time mass of the weak pressure gradient. On a collar whose doubled cylinder stays inside the unit data cylinder of thm:A, the 6/5 time mass of any weak slice derivative of the pressure on the collar half ball is at most an explicit absolute multiple of ε + 1.