Kernel Power #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Weighted and Riesz power-mean bounds for the Poincare kernel integrand #
First: a Hölder-type weighted power-mean inequality used to convert the
interval integral into an L^p bound.
Second: the final convex-domain Riesz-kernel bounds used by the Poincare
estimates.
theorem
CKN.weighted_power_mean_setIntegral
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
{p : ℝ}
(hp : 1 < p)
{f w : α → ℝ}
(hf : ∀ (x : α), 0 ≤ f x)
(hw : ∀ (x : α), 0 ≤ w x)
(hf_meas : AEMeasurable f (μ.restrict s))
(hwi : MeasureTheory.IntegrableOn w s μ)
(hfpwi : MeasureTheory.IntegrableOn (fun (x : α) => f x ^ p * w x) s μ)
:
Cache Nontrivial (Vec d) once per section.
theorem
CKN.integral_mul_rieszKernel_rpow_le_of_isSobolevRegularDomain
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
(hU : IsSobolevRegularDomain U)
{p : ℝ}
(hp : 1 < p)
{g : Vec d → ℝ}
(hg_nonneg : ∀ (y : Vec d), 0 ≤ g y)
(hg_meas : AEMeasurable g (MeasureTheory.volume.restrict U))
{x : Vec d}
(hx : x ∈ U)
(hgpK_int : MeasureTheory.IntegrableOn (fun (y : Vec d) => g y ^ p * rieszKernel x y) U MeasureTheory.volume)
:
theorem
CKN.integral_mul_rieszKernel_rpow_le_bound_of_isSobolevRegularDomain
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
(hU : IsSobolevRegularDomain U)
{p : ℝ}
(hp : 1 < p)
{g : Vec d → ℝ}
(hg_nonneg : ∀ (y : Vec d), 0 ≤ g y)
(hg_meas : AEMeasurable g (MeasureTheory.volume.restrict U))
{x : Vec d}
(hx : x ∈ U)
(hgpK_int : MeasureTheory.IntegrableOn (fun (y : Vec d) => g y ^ p * rieszKernel x y) U MeasureTheory.volume)
:
(∫ (y : Vec d) in U, g y * rieszKernel x y) ^ p ≤ (↑d * (MeasureTheory.volume (Metric.ball 0 1)).toReal * (4 * Classical.choose ⋯)) ^ (p - 1) * ∫ (y : Vec d) in U, g y ^ p * rieszKernel x y
theorem
CKN.integrable_rpow_integral_mul_rieszKernel_of_isSobolevRegularDomain
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
(hU : IsSobolevRegularDomain U)
{p : ℝ}
(hp : 1 < p)
{g : Vec d → ℝ}
(hg_nonneg : ∀ (y : Vec d), 0 ≤ g y)
(hg_meas : AEMeasurable g (MeasureTheory.volume.restrict U))
(hgK_prod_int :
MeasureTheory.IntegrableOn (fun (z : Vec d × Vec d) => g z.2 * rieszKernel z.1 z.2) (U ×ˢ U)
(MeasureTheory.volume.prod MeasureTheory.volume))
(hgpK_prod_int :
MeasureTheory.IntegrableOn (fun (z : Vec d × Vec d) => g z.2 ^ p * rieszKernel z.1 z.2) (U ×ˢ U)
(MeasureTheory.volume.prod MeasureTheory.volume))
:
MeasureTheory.Integrable (fun (x : Vec d) => (∫ (y : Vec d) in U, g y * rieszKernel x y) ^ p)
(MeasureTheory.volume.restrict U)
theorem
CKN.integral_rpow_integral_mul_rieszKernel_le_bound_of_isSobolevRegularDomain
{d : ℕ}
[NeZero d]
{U : Set (Vec d)}
(hU : IsSobolevRegularDomain U)
{p : ℝ}
(hp : 1 < p)
{g : Vec d → ℝ}
(hg_nonneg : ∀ (y : Vec d), 0 ≤ g y)
(hg_meas : AEMeasurable g (MeasureTheory.volume.restrict U))
(hgK_prod_int :
MeasureTheory.IntegrableOn (fun (z : Vec d × Vec d) => g z.2 * rieszKernel z.1 z.2) (U ×ˢ U)
(MeasureTheory.volume.prod MeasureTheory.volume))
(hgp_int : MeasureTheory.IntegrableOn (fun (y : Vec d) => g y ^ p) U MeasureTheory.volume)
(hgpK_prod_int :
MeasureTheory.IntegrableOn (fun (z : Vec d × Vec d) => g z.2 ^ p * rieszKernel z.1 z.2) (U ×ˢ U)
(MeasureTheory.volume.prod MeasureTheory.volume))
: