Riesz Second Bad Part

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

noncomputable def CKN.Foundation.Euclidean.rieszSecondKernelC₂ : ℝ

Explicit coefficient controlling the second Riesz kernel's size estimates.

Equations

• CKN.Foundation.Euclidean.rieszSecondKernelC₂ = 72 / (4 * Real.pi)

noncomputable def CKN.Foundation.Euclidean.rieszSecondKernel (i j : Fin 3) (z : Parabolic.Vec3) : ℝ

Second spatial derivative of the Newtonian kernel in the chosen coordinates.

Equations

• CKN.Foundation.Euclidean.rieszSecondKernel i j z = CKN.spatialDeriv (CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel i) j z

noncomputable def CKN.Foundation.Euclidean.heatSecondFormula (i j : Fin 3) (z : Parabolic.Vec3) : ℝ

Algebraic Hessian formula for the inverse Euclidean radius, before Newtonian normalization.

Equations

• CKN.Foundation.Euclidean.heatSecondFormula i j z = 3 * z i * z j * CKN.Foundation.Heat.q z ^ (-5 / 2) - (if i = j then 1 else 0) * CKN.Foundation.Heat.q z ^ (-3 / 2)

noncomputable def CKN.Foundation.Euclidean.heatQDerivative (p : ℝ) (x : Parabolic.Vec3) : Parabolic.Vec3 →L[ℝ] ℝ

Continuous linear differential of the power of the squared Euclidean norm.

Equations

• CKN.Foundation.Euclidean.heatQDerivative p x = (p * CKN.Foundation.Heat.q x ^ (p - 1)) • ∑ k : Fin 3, (2 * x k) • ContinuousLinearMap.proj k

noncomputable def CKN.Foundation.Euclidean.heatSecondDerivative (i j : Fin 3) (x : Parabolic.Vec3) : Parabolic.Vec3 →L[ℝ] ℝ

Continuous linear differential of the algebraic Newtonian Hessian formula.

Equations

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

theorem CKN.Foundation.Euclidean.rieszSecondKernelC₂_nonneg : 0 ≤ rieszSecondKernelC₂

theorem CKN.Foundation.Euclidean.rieszSecondKernel_measurable (i j : Fin 3) : Measurable (rieszSecondKernel i j)

theorem CKN.Foundation.Euclidean.rieszSecondKernel_differentiableAt {x : Parabolic.Vec3} (hx : x ≠ 0) (i j : Fin 3) : DifferentiableAt ℝ (rieszSecondKernel i j) x

theorem CKN.Foundation.Euclidean.rieszSecondKernel_fderiv_bound {x : Parabolic.Vec3} (hx : x ≠ 0) (i j : Fin 3) : ‖fderiv ℝ (rieszSecondKernel i j) x‖ ≤ rieszSecondKernelC₂ * Parabolic.vec3EuclideanNorm x ^ (-4)

theorem CKN.Foundation.Euclidean.rieszSecond_cube_star_exterior_geometry {Q : DyadicIndex} {x y : Parabolic.Vec3} (hx : x ∈ (rieszSecondCubeStar Q)ᶜ) (hy : y ∈ dyadicCubeSet Q) : 2 * Parabolic.vec3EuclideanNorm (y - dyadicCubeCenter Q.scale Q.corner) < Parabolic.vec3EuclideanNorm (x - dyadicCubeCenter Q.scale Q.corner)

theorem CKN.Foundation.Euclidean.rieszSecond_bad_cube_mean_zero {Q : DyadicIndex} {b : Parabolic.Vec3 → ℝ} (i j : Fin 3) (hmean : ∫ (y : Parabolic.Vec3) in dyadicCubeSet Q, b y = 0) (hb : MeasureTheory.IntegrableOn b (dyadicCubeSet Q) MeasureTheory.volume) (hterm : ∀ x ∈ (rieszSecondCubeStar Q)ᶜ, MeasureTheory.IntegrableOn (fun (y : Parabolic.Vec3) => rieszSecondKernel i j (x - y) * b y) (dyadicCubeSet Q) MeasureTheory.volume) {x : Parabolic.Vec3} (hx : x ∈ (rieszSecondCubeStar Q)ᶜ) : ∫ (y : Parabolic.Vec3) in dyadicCubeSet Q, rieszSecondKernel i j (x - y) * b y = ∫ (y : Parabolic.Vec3) in dyadicCubeSet Q, (rieszSecondKernel i j (x - y) - rieszSecondKernel i j (x - dyadicCubeCenter Q.scale Q.corner)) * b y

theorem CKN.Foundation.Euclidean.rieszSecond_bad_cube_hormander {Q : DyadicIndex} {b : Parabolic.Vec3 → ℝ} (i j : Fin 3) (hmean : ∫ (y : Parabolic.Vec3) in dyadicCubeSet Q, b y = 0) (hb : MeasureTheory.IntegrableOn b (dyadicCubeSet Q) MeasureTheory.volume) (hterm : ∀ x ∈ (rieszSecondCubeStar Q)ᶜ, MeasureTheory.IntegrableOn (fun (y : Parabolic.Vec3) => rieszSecondKernel i j (x - y) * b y) (dyadicCubeSet Q) MeasureTheory.volume) (hjoint : AEMeasurable (fun (z : Parabolic.Vec3 × Parabolic.Vec3) => ENNReal.ofReal |(rieszSecondKernel i j (z.1 - z.2) - rieszSecondKernel i j (z.1 - dyadicCubeCenter Q.scale Q.corner)) * b z.2|) ((MeasureTheory.volume.restrict (rieszSecondCubeStar Q)ᶜ).prod (MeasureTheory.volume.restrict (dyadicCubeSet Q)))) (hjointSwap : AEMeasurable (fun (z : Parabolic.Vec3 × Parabolic.Vec3) => ENNReal.ofReal |(rieszSecondKernel i j (z.2 - z.1) - rieszSecondKernel i j (z.2 - dyadicCubeCenter Q.scale Q.corner)) * b z.1|) ((MeasureTheory.volume.restrict (dyadicCubeSet Q)).prod (MeasureTheory.volume.restrict (rieszSecondCubeStar Q)ᶜ))) : ∃ (Tbad : Parabolic.Vec3 → ℝ), AEMeasurable (fun (x : Parabolic.Vec3) => ENNReal.ofReal |Tbad x|) (MeasureTheory.volume.restrict (rieszSecondCubeStar Q)ᶜ) ∧ MeasureTheory.IntegrableOn Tbad (rieszSecondCubeStar Q)ᶜ MeasureTheory.volume ∧ ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar Q)ᶜ, ENNReal.ofReal |Tbad x| ≤ ENNReal.ofReal (64 * Real.pi * rieszSecondKernelC₂) * ∫⁻ (y : Parabolic.Vec3) in dyadicCubeSet Q, ENNReal.ofReal |b y|