The order-one Hardy--Littlewood--Sobolev estimate in dimension three

The exponent used by the pressure decomposition is m = 5/2, s = 15. The proof is Hedberg's pointwise estimate followed by the strong maximal estimate. The a.e. maximal-data hypothesis is exposed so that zero data and finite truncations can be handled by the consuming pressure lemma.

noncomputable def CKN.Foundation.Euclidean.hlsRieszConstant : ENNReal

The constant in the three-dimensional order-one HLS estimate.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Foundation.Euclidean.rieszPotentialOne_hls_of_good {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : ∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2) < ⊤) (hI0 : ∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2) ≠ 0) (hgood : ∀ᵐ (z : Parabolic.Vec3), maximalMajorant f z ≠ 0 ∧ maximalMajorant f z ≠ ⊤) : (∫⁻ (z : Parabolic.Vec3), rieszPotentialOne f z ^ 15) ^ (1 / 15) ≤ hlsRieszConstant * (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (2 / 5)

theorem CKN.Foundation.Euclidean.maximalMajorant_ne_zero_of_integral_ne_zero {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hI0 : ∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2) ≠ 0) (z : Parabolic.Vec3) : maximalMajorant f z ≠ 0

theorem CKN.Foundation.Euclidean.rieszPotentialOne_hls {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : ∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2) < ⊤) (hI0 : ∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2) ≠ 0) : (∫⁻ (z : Parabolic.Vec3), rieszPotentialOne f z ^ 15) ^ (1 / 15) ≤ hlsRieszConstant * (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (2 / 5)

theorem CKN.Foundation.Euclidean.rieszPotentialOne_hls_of_zero_or_good {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : ∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2) < ⊤) : (∫⁻ (z : Parabolic.Vec3), rieszPotentialOne f z ^ 15) ^ (1 / 15) ≤ hlsRieszConstant * (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (2 / 5)