Strong bounds supplied by the two endpoint estimates

This file records the assembly step for a second Newtonian derivative. The operator is left as the operator supplied by the endpoint development: the only inputs here are its sublinearity, measurability, weak (1,1) estimate, and global (2,2) estimate.

noncomputable def CKN.Foundation.Euclidean.rieszSecondInterpolationConstant (A₁ A₂ p : ℝ) : ℝ

The explicit integral constant furnished by weak-to-strong interpolation.

Equations

• CKN.Foundation.Euclidean.rieszSecondInterpolationConstant A₁ A₂ p = p * (2 ^ p * (A₁ / (p - 1) + A₂ ^ 2 / (2 - p)))

theorem CKN.Foundation.Euclidean.rieszSecond_sublinear_of_additive {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} (hTadd : ∀ (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3), T (f + g) x = T f x + T g x) (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : |T (f + g) x| ≤ |T f x| + |T g x|

Convert pointwise additivity into the exact sublinearity interface.

theorem CKN.Foundation.Euclidean.rieszSecond_measurable_of_convolution {K : Parabolic.Vec3 → ℝ} (hK : Measurable K) (f : Parabolic.Vec3 → ℝ) : Measurable f → Measurable (MeasureTheory.convolution f K (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

A measurable scalar convolution kernel gives a measurable convolution output.

theorem CKN.Foundation.Euclidean.rieszSecond_convolution_congr {K f g : Parabolic.Vec3 → ℝ} (hfg : f =ᵐ[MeasureTheory.volume] g) : MeasureTheory.convolution f K (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume = MeasureTheory.convolution g K (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Convolution respects almost-everywhere equality of its input.

theorem CKN.Foundation.Euclidean.rieszSecond_convolution_sublinear_of_integrable {K f g : Parabolic.Vec3 → ℝ} {x : Parabolic.Vec3} (hf : MeasureTheory.Integrable (fun (y : Parabolic.Vec3) => f y * K (x - y)) MeasureTheory.volume) (hg : MeasureTheory.Integrable (fun (y : Parabolic.Vec3) => g y * K (x - y)) MeasureTheory.volume) : |MeasureTheory.convolution (f + g) K (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x| ≤ |MeasureTheory.convolution f K (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x| + |MeasureTheory.convolution g K (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x|

The literal convolution is sublinear wherever the two input integrals exist.

theorem CKN.Foundation.Euclidean.rieszSecond_strong_type_of_inputs {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)) (hWeak11 : ∀ (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) (hL2 : ∀ (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) {g : Parabolic.Vec3 → ℝ} (hg : Measurable g) : ∫⁻ (x : Parabolic.Vec3), absE (T g) x ^ p ≤ ENNReal.ofReal (rieszSecondInterpolationConstant A₁ A₂ p) * ∫⁻ (x : Parabolic.Vec3), absE g x ^ p

The strong (p,p) integral estimate from the two endpoint estimates.

theorem CKN.Foundation.Euclidean.rieszSecond_eLpNorm_bound_of_inputs {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)) (hWeak11 : ∀ (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) (hL2 : ∀ (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) {g : Parabolic.Vec3 → ℝ} (hg : Measurable g) : MeasureTheory.eLpNorm (T g) (ENNReal.ofReal p) MeasureTheory.volume ≤ ENNReal.ofReal (rieszSecondInterpolationConstant A₁ A₂ p) ^ (1 / p) * MeasureTheory.eLpNorm g (ENNReal.ofReal p) MeasureTheory.volume

The strong Lp seminorm estimate assembled from the two endpoint inputs.

theorem CKN.Foundation.Euclidean.rieszSecond_strong_type_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)) (hWeak11 : ∀ (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) (hL2 : ∀ (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₁) {g : Parabolic.Vec3 → ℝ} (hg : Measurable g) : ∫⁻ (x : Parabolic.Vec3), absE (T g) x ^ (3 / 2) ≤ ENNReal.ofReal (rieszSecondInterpolationConstant A₁ A₂ (3 / 2)) * ∫⁻ (x : Parabolic.Vec3), absE g x ^ (3 / 2)

The integral estimate at exponent 3 / 2.

theorem CKN.Foundation.Euclidean.rieszSecond_strong_type_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)) (hWeak11 : ∀ (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) (hL2 : ∀ (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₁) {g : Parabolic.Vec3 → ℝ} (hg : Measurable g) : ∫⁻ (x : Parabolic.Vec3), absE (T g) x ^ (6 / 5) ≤ ENNReal.ofReal (rieszSecondInterpolationConstant A₁ A₂ (6 / 5)) * ∫⁻ (x : Parabolic.Vec3), absE g x ^ (6 / 5)

The integral estimate at exponent 6 / 5.