Potential Decay Growth Sum

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

Growth bookkeeping for local L^{3/2} norms of pressure potentials

This file collects the elementary measure-theoretic bookkeeping used to compare the local L^{3/2} norms of the pressure potentials on the round balls euclideanBall 0 ρ: a global MemLp bound restricts to any ball, the local norm is controlled by the global norm times the linear growth factor 1 + ρ, and the operation of adding, subtracting, or summing finitely many potentials preserves an affine growth bound of the shape C * (1 + ρ). The statements are purely about MeasureTheory.lpNorm; no analysis enters.

theorem CKN.memLp_euclideanBall_of_memLp_volume {h : Foundation.Parabolic.Vec3 → ℝ} (hh : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (ρ : ℝ) : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))

A function that is L^{3/2} with respect to Lebesgue measure remains L^{3/2} after restricting Lebesgue measure to any round ball about the origin.

theorem CKN.lpNorm_euclideanBall_le_of_memLp_volume {h : Foundation.Parabolic.Vec3 → ℝ} (hh : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ρ : ℝ} (hρ : 0 < ρ) : MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) MeasureTheory.volume * (1 + ρ)

The local L^{3/2} norm of a global L^{3/2} function over the ball of radius ρ > 0 is at most the global norm multiplied by 1 + ρ.

theorem CKN.memLp_volume_of_memLp_restrict_of_support {h : Foundation.Parabolic.Vec3 → ℝ} {s : Set Foundation.Parabolic.Vec3} (hmeas : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) (hsupp : Function.support h ⊆ s) (hh : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict s)) : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

A function whose support is contained in s and which is L^{3/2} on s is L^{3/2} with respect to the ambient Lebesgue measure, provided it is almost everywhere strongly measurable there.

theorem CKN.lpNorm_euclideanBall_growth_add {f g : Foundation.Parabolic.Vec3 → ℝ} {C D : ℝ} (hfmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hf : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ)) (hg : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ D * (1 + ρ)) {ρ : ℝ} (hρ : 0 < ρ) : MeasureTheory.lpNorm (f + g) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (C + D) * (1 + ρ)

If f and g obey local L^{3/2} growth bounds with constants C and D, then f + g obeys the local growth bound with constant C + D.

theorem CKN.lpNorm_euclideanBall_growth_sub {f g : Foundation.Parabolic.Vec3 → ℝ} {C D : ℝ} (hfmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hf : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ)) (hg : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ D * (1 + ρ)) {ρ : ℝ} (hρ : 0 < ρ) : MeasureTheory.lpNorm (f - g) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (C + D) * (1 + ρ)

If f and g obey local L^{3/2} growth bounds with constants C and D, then f - g obeys the local growth bound with constant C + D.

theorem CKN.lpNorm_euclideanBall_growth_sum {ι : Type u_1} {s : Finset ι} {f : ι → Foundation.Parabolic.Vec3 → ℝ} {C : ι → ℝ} (hmem : ∀ i ∈ s, ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (f i) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hb : ∀ i ∈ s, ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (f i) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C i * (1 + ρ)) {ρ : ℝ} (hρ : 0 < ρ) : MeasureTheory.lpNorm (∑ i ∈ s, f i) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (∑ i ∈ s, C i) * (1 + ρ)

A finite sum of L^{3/2} potentials obeying local growth bounds with constants C i obeys the local growth bound with constant ∑ i ∈ s, C i.