The order-one Euclidean Riesz potential

This file supplies the geometric part of Hedberg's proof in the native three-dimensional model Vec3. The maximal majorant is the uncentred maximal function from Maximal.HardyLittlewood.

def CKN.Foundation.Euclidean.IsMaximalMajorant (f : Parabolic.Vec3 → ℝ) (M : Parabolic.Vec3 → ENNReal) : Prop

A maximal majorant for the absolute value of a real function.

Equations

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

noncomputable def CKN.Foundation.Euclidean.maximalMajorant (f : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ENNReal

The maximal majorant associated with the Euclidean maximal function.

Equations

• CKN.Foundation.Euclidean.maximalMajorant f = CKN.Foundation.Euclidean.maximalFunction fun (z : CKN.Foundation.Parabolic.Vec3) => ENNReal.ofReal |f z|

theorem CKN.Foundation.Euclidean.isMaximalMajorant_maximalMajorant (f : Parabolic.Vec3 → ℝ) : IsMaximalMajorant f (maximalMajorant f)

noncomputable def CKN.Foundation.Euclidean.rieszKernelOne (z w : Parabolic.Vec3) : ENNReal

The order-one Riesz kernel and its nonnegative potential.

Equations

• CKN.Foundation.Euclidean.rieszKernelOne z w = ENNReal.ofReal (dist z w) ^ (-2)

noncomputable def CKN.Foundation.Euclidean.rieszPotentialOne (f : Parabolic.Vec3 → ℝ) (z : Parabolic.Vec3) : ENNReal

Order-one Riesz potential of the absolute value of a scalar source.

Equations

• CKN.Foundation.Euclidean.rieszPotentialOne f z = ∫⁻ (w : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Euclidean.rieszKernelOne z w * ENNReal.ofReal |f w|

def CKN.Foundation.Euclidean.nearShell (R : ℝ) (n : ℕ) (z : Parabolic.Vec3) : Set Parabolic.Vec3

Dyadic shell inside the reference radius for the near-field potential estimate.

Equations

• CKN.Foundation.Euclidean.nearShell R n z = {w : CKN.Foundation.Parabolic.Vec3 | 2 ^ ↑(Int.negSucc n) * R ≤ dist z w ∧ dist z w < 2 ^ (↑(Int.negSucc n) + 1) * R}

def CKN.Foundation.Euclidean.farShell (R : ℝ) (n : ℕ) (z : Parabolic.Vec3) : Set Parabolic.Vec3

Dyadic shell outside the reference radius for the far-field potential estimate.

Equations

• CKN.Foundation.Euclidean.farShell R n z = {w : CKN.Foundation.Parabolic.Vec3 | 2 ^ ↑n * R ≤ dist z w ∧ dist z w < 2 ^ (↑n + 1) * R}

noncomputable def CKN.Foundation.Euclidean.nearTerm (n : ℕ) : ENNReal

Geometric-series term controlling the near-field order-one potential.

Equations

• CKN.Foundation.Euclidean.nearTerm n = ENNReal.ofReal (2 ^ ↑(Int.negSucc n)) ^ (-2) * ENNReal.ofReal ((4 * 2 ^ ↑(Int.negSucc n)) ^ 3)

noncomputable def CKN.Foundation.Euclidean.hedbergNearConstant : ENNReal

The geometric constant in the near-field estimate.

Equations

• CKN.Foundation.Euclidean.hedbergNearConstant = ∑' (n : ℕ), CKN.Foundation.Euclidean.nearTerm n

theorem CKN.Foundation.Euclidean.rieszPotentialOne_near_le {R : ℝ} (hR : 0 < R) {f : Parabolic.Vec3 → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : Parabolic.Vec3 → ENNReal} (hM : IsMaximalMajorant f M) (z : Parabolic.Vec3) : ∫⁻ (w : Parabolic.Vec3) in {w : Parabolic.Vec3 | dist z w < R}, rieszKernelOne z w * ENNReal.ofReal |f w| ≤ hedbergNearConstant * ENNReal.ofReal R * M z

noncomputable def CKN.Foundation.Euclidean.farTerm (n : ℕ) : ENNReal

Geometric-series term controlling the far-field order-one potential.

Equations

• CKN.Foundation.Euclidean.farTerm n = (ENNReal.ofReal (2 ^ ↑n) ^ (-(10 / 3)) * ENNReal.ofReal ((4 * 2 ^ ↑n) ^ 3)) ^ (3 / 5)

noncomputable def CKN.Foundation.Euclidean.hedbergFarConstant : ENNReal

Summed coefficient in the far-field Hedberg estimate.

Equations

• CKN.Foundation.Euclidean.hedbergFarConstant = ∑' (n : ℕ), CKN.Foundation.Euclidean.farTerm n

theorem CKN.Foundation.Euclidean.rieszPotentialOne_far_le {R : ℝ} (hR : 0 < R) {f : Parabolic.Vec3 → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (z : Parabolic.Vec3) : ∫⁻ (w : Parabolic.Vec3) in {w : Parabolic.Vec3 | R ≤ dist z w}, rieszKernelOne z w * ENNReal.ofReal |f w| ≤ hedbergFarConstant * ENNReal.ofReal R ^ (-(1 / 5)) * (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (2 / 5)

theorem CKN.Foundation.Euclidean.rieszPotentialOne_scale_le {R : ℝ} (hR : 0 < R) {f : Parabolic.Vec3 → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : Parabolic.Vec3 → ENNReal} (hM : IsMaximalMajorant f M) (z : Parabolic.Vec3) : rieszPotentialOne f z ≤ hedbergNearConstant * ENNReal.ofReal R * M z + hedbergFarConstant * ENNReal.ofReal R ^ (-(1 / 5)) * (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (2 / 5)

theorem CKN.Foundation.Euclidean.rieszPotentialOne_hedberg {f : Parabolic.Vec3 → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : Parabolic.Vec3 → ENNReal} (hM : IsMaximalMajorant f M) (z : Parabolic.Vec3) (hM0 : M z ≠ 0) (hMtop : M z ≠ ⊤) (hB0 : (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (2 / 5) ≠ 0) (hBtop : (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (2 / 5) ≠ ⊤) : rieszPotentialOne f z ≤ (hedbergNearConstant + hedbergFarConstant) * M z ^ (1 / 6) * (∫⁻ (w : Parabolic.Vec3), ENNReal.ofReal |f w| ^ (5 / 2)) ^ (1 / 3)