Pointwise truncation bounds

The Marcinkiewicz interpolation argument used for the Caffarelli–Kohn–Nirenberg program (CKN 1982) controls the two pieces of a function f cut at a level l > 0 by the single power |f| ^ p, for 1 < p < 2. This file records the two elementary pointwise inequalities that make that reduction work, stated for the ℝ≥0∞-valued modulus absE f x = ENNReal.ofReal |f x|.

Above the level the first inequality bounds the modulus itself by l ^ (1 - p) * |f| ^ p; below the level the second bounds its square by l ^ (2 - p) * |f| ^ p. Both are pointwise in x and depend only on the scalar comparison of |f x| with l; the exponents l ^ (1 - p) and l ^ (2 - p) are real powers.

theorem CKN.Foundation.Euclidean.absE_le_of_lt_absE {f : Parabolic.Vec3 → ℝ} {p l : ℝ} (hp1 : 1 < p) (hl : 0 < l) {x : Parabolic.Vec3} (hx : ENNReal.ofReal l < absE f x) : absE f x ≤ ENNReal.ofReal (l ^ (1 - p)) * absE f x ^ p

Above the level l, the modulus is dominated by the p-th power with the weight l ^ (1 - p): from l < |f x| the monotonicity of real powers gives |f x| ≤ l ^ (1 - p) * |f x| ^ p whenever 1 < p.

theorem CKN.Foundation.Euclidean.absE_sq_le_of_absE_le {f : Parabolic.Vec3 → ℝ} {p l : ℝ} (hp0 : 0 < p) (hp2 : p < 2) (hl : 0 < l) {x : Parabolic.Vec3} (hx : absE f x ≤ ENNReal.ofReal l) : absE f x ^ 2 ≤ ENNReal.ofReal (l ^ (2 - p)) * absE f x ^ p

Below the level l, the square is dominated by the p-th power with the weight l ^ (2 - p): from |f x| ≤ l the monotonicity of real powers gives |f x| ^ 2 ≤ l ^ (2 - p) * |f x| ^ p whenever 0 < p < 2.