Slice-selected pressure gradients: classical, additive, quantitative forms

Display (3.5) of the pressure-gradient section selects, on a half ball, the coordinate weak derivative of the pressure obtained by splitting it into a particular potential and a smooth harmonic representative. The ingredients recorded here are exactly the ones that selection step consumes: a C¹ function has its classical coordinate gradient as a weak partial derivative, weak partial derivatives add along an a.e. decomposition of the carrier, and a coordinate field obeying a pointwise gradient display is controlled in L^(6/5) on the half ball.

theorem CKN.Core.Step4.hasWeakPartialDerivOn_classicalGradient {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {h : Foundation.Parabolic.Vec3 → ℝ} (k : Fin 3) (hh : ContDiffOn ℝ (↑1) h B) : HasWeakPartialDerivOn B k h fun (x : Vec 3) => classicalGradient h x k

classical gradient of a C¹ function is its weak partial derivative

theorem CKN.Core.Step4.locallyIntegrableOn_classicalGradient {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {h : Foundation.Parabolic.Vec3 → ℝ} (k : Fin 3) (hh : ContDiffOn ℝ (↑1) h B) : MeasureTheory.LocallyIntegrableOn (fun (x : Vec 3) => classicalGradient h x k) B MeasureTheory.volume

The classical coordinate gradient of a C¹ function is locally integrable, as required by display (3.5).

theorem CKN.Core.Step4.hasWeakPartialDerivOn_add {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {k : Fin 3} {h w gh gw : Foundation.Parabolic.Vec3 → ℝ} (hh : HasWeakPartialDerivOn B k h gh) (hw : HasWeakPartialDerivOn B k w gw) (hhloc : MeasureTheory.LocallyIntegrableOn h B MeasureTheory.volume) (hwloc : MeasureTheory.LocallyIntegrableOn w B MeasureTheory.volume) (hghloc : MeasureTheory.LocallyIntegrableOn gh B MeasureTheory.volume) (hgwloc : MeasureTheory.LocallyIntegrableOn gw B MeasureTheory.volume) : HasWeakPartialDerivOn B k (fun (x : Vec 3) => h x + w x) fun (x : Vec 3) => gh x + gw x

Display (3.5) decomposes the selected pressure into a particular and a harmonic part; the weak partial derivatives of the two parts add.

theorem CKN.Core.Step4.eLpNorm_classicalGradient_component_le_of_sup {h : Foundation.Parabolic.Vec3 → ℝ} {x₀ : Foundation.Parabolic.Vec3} {ρ M : ℝ} (hρ : 0 < ρ) (hM : 0 ≤ M) (k : Fin 3) (hmeas : MeasureTheory.AEStronglyMeasurable (fun (x : Vec 3) => classicalGradient h x k) (MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2)))) (hsup : ∀ x ∈ euclideanBall x₀ (ρ / 2), Foundation.Parabolic.vec3EuclideanNorm (classicalGradient h x) ≤ M) : MeasureTheory.eLpNorm (fun (x : Vec 3) => classicalGradient h x k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))) ≤ ENNReal.ofReal M * MeasureTheory.volume (euclideanBall x₀ (ρ / 2)) ^ (5 / 6)

the L^(6/5) bound on the half ball produced by a pointwise gradient display