Marcinkiewicz interpolation for operators defined on a restricted class

interpolation_weak11_strong22 (Interpolation.lean) assumes sublinearity, the weak (1,1) bound and the strong (2,2) bound for every measurable function. A Calderón--Zygmund operator obtained as the L^2-extension of a singular integral does not satisfy such hypotheses: outside L^2 it is only defined by a convention, so the endpoint estimates hold only on the classes on which the operator is genuinely defined.

This file proves the same conclusion, with the same constant p · 2^p · (A₁/(p-1) + A₂²/(2-p)) for 1 < p < 2, from hypotheses restricted to the classes actually visited by the truncation argument. Two variants are provided:

• interpolation_weak11_strong22_of_classes, whose endpoint hypotheses are assumed for integrable functions (weak (1,1)) and for L^2 functions (strong (2,2)), with sublinearity only for an (integrable, L^2) pair;
• interpolation_weak11_strong22_of_l2_classes, whose hypotheses are in addition confined to L^2 inputs throughout, which is the form available for an operator constructed as an L^2-extension and only later extended to L^p by density.

Splitting f at the level t/2 produces the two pieces f·1_{|f| > t/2} and f·1_{|f| ≤ t/2}. For f ∈ L^p with 1 < p < 2 the first is integrable and the second lies in L^2; these two facts, proved here from the pointwise bounds of InterpolationTruncBounds.lean, are what lets the restricted hypotheses be applied. Everything else is the argument of Interpolation.lean.

The two truncations of an L^p function

theorem CKN.Foundation.Euclidean.integrable_indicator_gt_of_memLp {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) {p : ℝ} (hp1 : 1 < p) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) {l : ℝ} (hl : 0 < l) : MeasureTheory.Integrable ((absE f ⁻¹' Set.Ioi (ENNReal.ofReal l)).indicator f) MeasureTheory.volume

The part of an L^p function above a positive level is integrable: on {|f| > l} the modulus is bounded by l^{1-p} |f|^p.

theorem CKN.Foundation.Euclidean.memLp_two_indicator_le_of_memLp {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) {p : ℝ} (hp0 : 0 < p) (hp2 : p < 2) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) {l : ℝ} (hl : 0 < l) : MeasureTheory.MemLp ((absE f ⁻¹' Set.Iic (ENNReal.ofReal l)).indicator f) 2 MeasureTheory.volume

The part of an L^p function below a positive level lies in L^2: on {|f| ≤ l} the square of the modulus is bounded by l^{2-p} |f|^p.

The distribution-function bound from the two pieces

The layer-cake integration

theorem CKN.Foundation.Euclidean.interpolation_of_tail_bound {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ p : ℝ} (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hTf : Measurable (T f)) (htail : ∀ (t : ℝ), 0 < t → MeasureTheory.volume {x : Parabolic.Vec3 | t < |T f x|} ≤ ENNReal.ofReal (2 * A₁ / t) * highTail (absE f) t + ENNReal.ofReal (4 * A₂ ^ 2 / t ^ 2) * lowTail (absE f) t) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ p ≤ ENNReal.ofReal (p * (2 ^ p * (A₁ / (p - 1) + A₂ ^ 2 / (2 - p)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ p

The layer-cake half of the interpolation theorem: the distribution-function bound at every level, integrated against the weight p t^{p-1}. This is the proof of interpolation_weak11_strong22 with the tail estimate taken as a hypothesis.

Interpolation with hypotheses restricted to the endpoint classes

theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_of_classes {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ p : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume ∨ MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) (hTf : Measurable (T f)) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ p ≤ ENNReal.ofReal (p * (2 ^ p * (A₁ / (p - 1) + A₂ ^ 2 / (2 - p)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ p

Marcinkiewicz interpolation for an operator defined on L^1 + L^2. The weak (1,1) bound is assumed only for integrable functions, the strong (2,2) bound only for L^2 functions, and sublinearity only for a pair consisting of an integrable function and an L^2 function. For f ∈ L^p with 1 < p < 2 the conclusion and the constant are those of interpolation_weak11_strong22.

Because f ∈ L^p is in general neither integrable nor square integrable, the measurability of T f for the input f itself is not a consequence of hTmeas and is taken as the explicit hypothesis hTf.

theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_of_l2_classes {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ p : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ p ≤ ENNReal.ofReal (p * (2 ^ p * (A₁ / (p - 1) + A₂ ^ 2 / (2 - p)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ p

Marcinkiewicz interpolation for an operator defined on L^2. Every hypothesis is confined to square-integrable inputs: this is the form available for an operator constructed as the L^2-extension of a singular integral, before it has been extended to L^p by density. For f ∈ L^p ∩ L^2 with 1 < p < 2 the conclusion and the constant are those of interpolation_weak11_strong22.

The two truncations of such an f at a level l > 0 lie in L^1 ∩ L^2 and in L^2 respectively, so all four hypotheses apply to them; and T f is measurable by hTmeas applied to f itself, so no extra measurability hypothesis is needed.

The exponents used by the pressure estimates

theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_of_classes_threeHalves {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume ∨ MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hTf : Measurable (T f)) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ (3 / 2) ≤ ENNReal.ofReal (3 / 2 * (2 ^ (3 / 2) * (A₁ / (3 / 2 - 1) + A₂ ^ 2 / (2 - 3 / 2)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ (3 / 2)

interpolation_weak11_strong22_of_classes at the exponent p = 3/2.

theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_of_classes_sixFifths {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume ∨ MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hTf : Measurable (T f)) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ (6 / 5) ≤ ENNReal.ofReal (6 / 5 * (2 ^ (6 / 5) * (A₁ / (6 / 5 - 1) + A₂ ^ 2 / (2 - 6 / 5)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ (6 / 5)

interpolation_weak11_strong22_of_classes at the exponent p = 6/5.

theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_of_l2_classes_threeHalves {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ (3 / 2) ≤ ENNReal.ofReal (3 / 2 * (2 ^ (3 / 2) * (A₁ / (3 / 2 - 1) + A₂ ^ 2 / (2 - 3 / 2)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ (3 / 2)

interpolation_weak11_strong22_of_l2_classes at the exponent p = 3/2.

theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_of_l2_classes_sixFifths {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |T f x|} ≤ (ENNReal.ofReal A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hstrong : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ 2 ≤ ENNReal.ofReal (A₂ ^ 2) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2) (hA₁ : 0 ≤ A₁) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫⁻ (x : Parabolic.Vec3), absE (T f) x ^ (6 / 5) ≤ ENNReal.ofReal (6 / 5 * (2 ^ (6 / 5) * (A₁ / (6 / 5 - 1) + A₂ ^ 2 / (2 - 6 / 5)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ (6 / 5)

interpolation_weak11_strong22_of_l2_classes at the exponent p = 6/5.