Riesz Second Weak Certificate

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

theorem CKN.Foundation.Euclidean.rieszSecond_concrete_bad_bridge {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (hL2 : RieszSecondL2Input i j) (D : CZDecomposition F level) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (Q : { Q : DyadicIndex // Q ∈ D.cubes }) : ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x| ≤ ENNReal.ofReal (64 * Real.pi * rieszSecondKernelC₂) * ∫⁻ (y : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) y|

theorem CKN.Foundation.Euclidean.rieszSecond_concrete_bad_additivity {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (hL2 : RieszSecondL2Input i j) (D : CZDecomposition F level) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) : (∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp F hF₂) x - rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicGoodPart F D.cubes) ⋯) x = ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x) ∧ ∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, Summable fun (Q : { Q : DyadicIndex // Q ∈ D.cubes }) => |rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x|

noncomputable def CKN.Foundation.Euclidean.rieszSecondL2CzCertificate {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (hL2 : RieszSecondL2Input i j) (_hFmeas : Measurable F) (hFint : MeasureTheory.Integrable F MeasureTheory.volume) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hlevel : 0 < level) : RieszSecondL2CZCertificate hL2 F hF₂ level

Concrete Calderón–Zygmund certificate for the second-Riesz L² operator.

Equations

• CKN.Foundation.Euclidean.rieszSecondL2CzCertificate hL2 _hFmeas hFint hF₂ hlevel = CKN.Foundation.Euclidean.rieszSecondL2CzCertificateOfInterfaces hL2 hFint hF₂ hlevel ⋯

theorem CKN.Foundation.Euclidean.rieszSecondL2_weak_type (i j : Fin 3) (f : Parabolic.Vec3 → ℝ) : Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator (rieszSecondL2Input i j) f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l

theorem CKN.Foundation.Euclidean.rieszSecondL2_interpolation_threeHalves {i j : Fin 3} {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫⁻ (x : Parabolic.Vec3), absE (rieszSecondL2RawOperator (rieszSecondL2Input i j) f) x ^ (3 / 2) ≤ ENNReal.ofReal (rieszSecondInterpolationConstant rieszSecondWeakTypeConstant 1 (3 / 2)) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ (3 / 2)

theorem CKN.Foundation.Euclidean.rieszSecondL2_interpolation_sixFifths {i j : Fin 3} {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫⁻ (x : Parabolic.Vec3), absE (rieszSecondL2RawOperator (rieszSecondL2Input i j) f) x ^ (6 / 5) ≤ ENNReal.ofReal (rieszSecondInterpolationConstant rieszSecondWeakTypeConstant 1 (6 / 5)) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ (6 / 5)