Newtonian Derivative Local Lp

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.Foundation.Euclidean.scalarConvolution (f g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : ℝ

The scalar convolution convention used for the Newtonian derivative.

Equations

• CKN.Foundation.Euclidean.scalarConvolution f g x = ∫ (y : CKN.Foundation.Parabolic.Vec3), f y * g (x - y)

noncomputable def CKN.Foundation.Euclidean.convolutionMajorant (f g : Parabolic.Vec3 → ENNReal) (x : Parabolic.Vec3) : ENNReal

Extended nonnegative convolution used to majorize ordinary convolution integrals.

Equations

• CKN.Foundation.Euclidean.convolutionMajorant f g x = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), f y * g (x - y)

theorem CKN.Foundation.Euclidean.eLpNorm_scalarConvolution_six_fifths_three_halves {f g : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hg : Measurable g) : MeasureTheory.eLpNorm (scalarConvolution f g) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ MeasureTheory.eLpNorm f (ENNReal.ofReal (6 / 5)) MeasureTheory.volume * MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

Young's estimate for the exponents used by the truncated Newtonian derivative. The proof uses Hölder twice and Tonelli on the nonnegative majorant.

The next declarations specialize the preceding Young estimate to the three-dimensional Newtonian derivative.

noncomputable def CKN.Foundation.Euclidean.truncatedNewtonianDerivative (R : ℝ) (i : Fin 3) : Parabolic.Vec3 → ℝ

The Newtonian derivative kernel truncated to a ball about the origin.

Equations

• CKN.Foundation.Euclidean.truncatedNewtonianDerivative R i z = if ‖z‖ < R then CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel i z else 0

theorem CKN.Foundation.Euclidean.measurable_truncatedNewtonianDerivative (R : ℝ) (i : Fin 3) : Measurable (truncatedNewtonianDerivative R i)

The truncated Newtonian derivative kernel is measurable.

The complementary kernel is kept separate so that the local estimate can be assembled from a Young bound and a pointwise tail bound.

noncomputable def CKN.Foundation.Euclidean.farNewtonianDerivative (R : ℝ) (i : Fin 3) : Parabolic.Vec3 → ℝ

The Newtonian derivative kernel restricted to the complement of a ball.

Equations

• CKN.Foundation.Euclidean.farNewtonianDerivative R i z = if R ≤ ‖z‖ then CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel i z else 0

theorem CKN.Foundation.Euclidean.measurable_farNewtonianDerivative (R : ℝ) (i : Fin 3) : Measurable (farNewtonianDerivative R i)

The complementary Newtonian derivative kernel is measurable.

theorem CKN.Foundation.Euclidean.truncatedNewtonianDerivative_memLp {R : ℝ} : 0 < R → ∀ (i : Fin 3), MeasureTheory.MemLp (truncatedNewtonianDerivative R i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The truncated Newtonian derivative belongs to L^(6/5).

noncomputable def CKN.Foundation.Euclidean.newtonianDerivativePotential (i : Fin 3) (G : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : ℝ

The first Newtonian derivative potential, with the derivative in the kernel slot.

Equations

• CKN.Foundation.Euclidean.newtonianDerivativePotential i G x = ∫ (y : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel i (x - y) * G y

theorem CKN.Foundation.Euclidean.newtonianDerivative_far_kernel_bound {R' : ℝ} {z : Parabolic.Vec3} (hR' : 0 < R') (hz : R' ≤ ‖z‖) (i : Fin 3) : |spatialDeriv Heat.newtonianKernel i z| ≤ (4 * Real.pi)⁻¹ * (R' ^ 2)⁻¹

The derivative kernel has the expected inverse-square bound away from the origin.

theorem CKN.Foundation.Euclidean.norm_farNewtonianDerivative_le {R : ℝ} (hR : 0 < R) (i : Fin 3) (z : Parabolic.Vec3) : ‖farNewtonianDerivative R i z‖ ≤ (4 * Real.pi)⁻¹ * (R ^ 2)⁻¹

The far kernel is bounded by its inverse-square value at the cutoff.

theorem CKN.Foundation.Euclidean.newtonianDerivative_far_integral_enorm_le {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R' : ℝ} (hR' : 0 < R') (x : Parabolic.Vec3) (hfar : ∀ (y : Parabolic.Vec3), G y ≠ 0 → R' ≤ ‖x - y‖) : ‖newtonianDerivativePotential i G x‖ₑ ≤ ENNReal.ofReal ((4 * Real.pi)⁻¹ * (R' ^ 2)⁻¹) * ∫⁻ (y : Parabolic.Vec3), ‖G y‖ₑ

At points whose support is outside the near ball, the far potential is bounded by the inverse-square kernel constant times the L¹ size of the data.

theorem CKN.Foundation.Euclidean.scalarConvolution_far_enorm_le {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R : ℝ} (hR : 0 < R) (x : Parabolic.Vec3) : ‖scalarConvolution G (farNewtonianDerivative R i) x‖ₑ ≤ ENNReal.ofReal ((4 * Real.pi)⁻¹ * (R ^ 2)⁻¹) * ∫⁻ (y : Parabolic.Vec3), ‖G y‖ₑ

The convolution with the far kernel has the same pointwise tail bound.

theorem CKN.Foundation.Euclidean.eLpNorm_one_le_of_memLp_six_fifths_of_support {G : Parabolic.Vec3 → ℝ} {R : ℝ} : 0 < R → ∀ (hGmeas : Measurable G), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → ∀ (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0), MeasureTheory.eLpNorm G 1 MeasureTheory.volume ≤ MeasureTheory.volume (Metric.closedBall 0 R) ^ (1 / 6) * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

Compact support converts the L^(6/5) size into the L¹ size needed by the far part.

theorem CKN.Foundation.Euclidean.newtonianDerivativePotential_eLpNorm_three_halves_restrict_ball_le_split {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R ρ R' : ℝ} (hR : 0 < R) (hρ : 0 < ρ) (hR' : 0 < R') (hGmeas : Measurable G) (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : MeasureTheory.eLpNorm (newtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Metric.ball 0 ρ)) ≤ MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume * MeasureTheory.eLpNorm (truncatedNewtonianDerivative R' i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal ((4 * Real.pi)⁻¹ * (R' ^ 2)⁻¹) * MeasureTheory.volume (Metric.ball 0 ρ) ^ (2 / 3) * MeasureTheory.volume (Metric.closedBall 0 R) ^ (1 / 6) * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The local Newtonian derivative estimate obtained by adding the near Young estimate to the bounded far tail.

theorem CKN.Foundation.Euclidean.newtonianDerivativePotential_eLpNorm_three_halves_restrict_ball_le {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R ρ : ℝ} (hR : 0 < R) (hρ : 0 < ρ) (hGmeas : Measurable G) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → ∀ (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0), MeasureTheory.eLpNorm (newtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Metric.ball 0 ρ)) ≤ MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume * MeasureTheory.eLpNorm (truncatedNewtonianDerivative (R + ρ) i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

On a ball, compact support lets the potential use the truncated kernel.