Growth of the indexed pressure-extension residual

The global pressure operator used here is the indexed L^(3/2) extension. The ordinary kernel formula is not used. The first theorem is the residual bookkeeping in a form independent of the construction of the operator; the second supplies its local hypotheses from the global MemLp statement of the indexed extension. The last two declarations expose the pressure-decomposition shape consumed by the CZ identification argument.

theorem CKN.pressure_residual_local_linear_growth_of_bounds {p₁ T : Foundation.Parabolic.Vec3 → ℝ} {C₁ C₂ p : ℝ} (hp : 1 ≤ p) (hP1mem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp p₁ (ENNReal.ofReal p) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hTmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp T (ENNReal.ofReal p) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hP1bound : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm p₁ (ENNReal.ofReal p) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C₁ * (1 + ρ)) (hTbound : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm T (ENNReal.ofReal p) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C₂ * (1 + ρ)) (ρ : ℝ) : 0 < ρ → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p₁ x - T x) (ENNReal.ofReal p) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ∧ MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p₁ x - T x) (ENNReal.ofReal p) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (C₁ + C₂) * (1 + ρ)

theorem CKN.pressureSecondExtension_residual_growth_of_decomposition {p₁ T P H J : Foundation.Parabolic.Vec3 → ℝ} {C₀ C_H C_J C_T : ℝ} (hdecomp : p₁ = P - (H + J)) (hPmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp P (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hPbound : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm P (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C₀ * (1 + ρ)) (hHmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hHbound : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C_H * (1 + ρ)) (hJmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp J (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hJbound : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm J (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C_J * (1 + ρ)) (hTmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp T (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hTbound : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm T (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C_T * (1 + ρ)) (ρ : ℝ) : 0 < ρ → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p₁ x - T x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ∧ MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p₁ x - T x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (C₀ + C_H + C_J + C_T) * (1 + ρ)