Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Euclidean.Interpolation

Marcinkiewicz interpolation between weak (1,1) and strong (2,2) #

For a sublinear operator T on functions Vec3 → ℝ that is of weak type (1,1) with constant A₁ and of strong type (2,2) with constant A₂, the interpolation theorem interpolation_weak11_strong22 gives the strong (p,p) bound with the explicit constant p · 2^p · (A₁/(p-1) + A₂²/(2-p)) for every 1 < p < 2. The exponents p = 3/2 and p = 6/5 are recorded as corollaries.

The analytic ingredients — the distribution-function estimate obtained by truncating at level t/2, and its layer-cake integral against the weight p t^{p-1} — are in InterpolationBasic.lean.

source
theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22 {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ p : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → ∀ (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 → ∫⁻ (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) :
∫⁻ (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. A sublinear operator T that is of weak type (1,1) with constant A₁ and of strong type (2,2) with constant A₂ satisfies the strong (p,p) bound for every 1 < p < 2, with the explicit constant p · 2^p · (A₁/(p-1) + A₂²/(2-p)). This is the distribution-function estimate at the level t, integrated against the layer-cake weight p t^{p-1}.

source
theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_threeHalves {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → ∀ (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 → ∫⁻ (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) :
∫⁻ (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 at the exponent p = 3/2: weak (1,1) and strong (2,2) estimates give the strong (3/2,3/2) estimate, with the constant of interpolation_weak11_strong22 specialized to p = 3/2.

source
theorem CKN.Foundation.Euclidean.interpolation_weak11_strong22_sixFifths {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {A₁ A₂ : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3), |T (f + g) x| ≤ |T f x| + |T g x|) (hTmeas : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → Measurable (T f)) (hweak : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → ∀ (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 → ∫⁻ (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) :
∫⁻ (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 at the exponent p = 6/5: weak (1,1) and strong (2,2) estimates give the strong (6/5,6/5) estimate, with the constant of interpolation_weak11_strong22 specialized to p = 6/5.