Riesz Second Operator

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

@[reducible, inline]

noncomputable abbrev CKN.Foundation.Euclidean.rieszSecondL2 : AddSubgroup (Parabolic.Vec3 →ₘ[MeasureTheory.volume] ℝ)

Real L² space on three-dimensional Euclidean volume.

Equations

• CKN.Foundation.Euclidean.rieszSecondL2 = MeasureTheory.Lp ℝ 2 MeasureTheory.volume

noncomputable def CKN.Foundation.Euclidean.rieszSecondSchwartzEmbedding : SchwartzMap Parabolic.Vec3 ℝ →L[ℝ] ↥rieszSecondL2

Continuous inclusion of Schwartz functions into the L² source space.

Equations

• CKN.Foundation.Euclidean.rieszSecondSchwartzEmbedding = SchwartzMap.toLpCLM ℝ ℝ 2 MeasureTheory.volume

structure CKN.Foundation.Euclidean.RieszSecondL2Input (i j : Fin 3) : Type

Schwartz-space construction and norm bound used to extend the second Riesz transform to L².

• smoothMap : SchwartzMap Parabolic.Vec3 ℝ →L[ℝ] ↥rieszSecondL2

  Second-Riesz operator on the dense Schwartz source space.

• smooth_bound (φ : SchwartzMap Parabolic.Vec3 ℝ) : ‖self.smoothMap φ‖ ≤ ‖rieszSecondSchwartzEmbedding φ‖
• smooth_hessian (F : Parabolic.Vec3 → ℝ) (_hF : ContDiff ℝ (↑⊤) F) (_hFc : HasCompactSupport F) : ∃ (hmem : MeasureTheory.MemLp (mixedSecond (pressureNewtonianPotential F) i j) 2 MeasureTheory.volume), self.smoothMap (_hFc.toSchwartzMap _hF) = MeasureTheory.MemLp.toLp (mixedSecond (pressureNewtonianPotential F) i j) hmem

noncomputable def CKN.Foundation.Euclidean.rieszSecondL2Extension {i j : Fin 3} (hL2 : RieszSecondL2Input i j) : ↥rieszSecondL2 →L[ℝ] ↥rieszSecondL2

Continuous L² extension of the Schwartz second-Riesz operator.

Equations

• CKN.Foundation.Euclidean.rieszSecondL2Extension hL2 = (↑((↑hL2.smoothMap).extendOfNorm ↑CKN.Foundation.Euclidean.rieszSecondSchwartzEmbedding)).mkContinuous 1 ⋯

theorem CKN.Foundation.Euclidean.rieszSecondL2Extension_agrees {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (φ : SchwartzMap Parabolic.Vec3 ℝ) : (rieszSecondL2Extension hL2) (rieszSecondSchwartzEmbedding φ) = hL2.smoothMap φ

theorem CKN.Foundation.Euclidean.rieszSecondL2Extension_smooth_hessian {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {F : Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) : ∃ (hmem : MeasureTheory.MemLp (mixedSecond (pressureNewtonianPotential F) i j) 2 MeasureTheory.volume), (rieszSecondL2Extension hL2) (MeasureTheory.MemLp.toLp F ⋯) = MeasureTheory.MemLp.toLp (mixedSecond (pressureNewtonianPotential F) i j) hmem

theorem CKN.Foundation.Euclidean.rieszSecondL2Extension_norm_le {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (f : ↥rieszSecondL2) : ‖(rieszSecondL2Extension hL2) f‖ ≤ ‖f‖

noncomputable def CKN.Foundation.Euclidean.rieszSecondLpMeasurableRepresentative (u : ↥rieszSecondL2) : Parabolic.Vec3 → ℝ

A chosen measurable representative of an L² equivalence class.

Equations

• CKN.Foundation.Euclidean.rieszSecondLpMeasurableRepresentative u = AEMeasurable.mk ↑↑u ⋯

theorem CKN.Foundation.Euclidean.rieszSecondLpMeasurableRepresentative_measurable (u : ↥rieszSecondL2) : Measurable (rieszSecondLpMeasurableRepresentative u)

theorem CKN.Foundation.Euclidean.rieszSecondLpMeasurableRepresentative_ae_eq (u : ↥rieszSecondL2) : ↑↑u =ᵐ[MeasureTheory.volume] rieszSecondLpMeasurableRepresentative u

noncomputable def CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (u : ↥rieszSecondL2) : Parabolic.Vec3 → ℝ

Measurable representative of the second-Riesz L² output.

Equations

• CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator hL2 u = CKN.Foundation.Euclidean.rieszSecondLpMeasurableRepresentative ((CKN.Foundation.Euclidean.rieszSecondL2Extension hL2) u)

theorem CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator_measurable {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (u : ↥rieszSecondL2) : Measurable (rieszSecondL2MeasurableOperator hL2 u)

theorem CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator_ae_eq_extension {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (u : ↥rieszSecondL2) : rieszSecondL2MeasurableOperator hL2 u =ᵐ[MeasureTheory.volume] ↑↑((rieszSecondL2Extension hL2) u)

theorem CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator_add_ae {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (u v : ↥rieszSecondL2) : rieszSecondL2MeasurableOperator hL2 (u + v) =ᵐ[MeasureTheory.volume] rieszSecondL2MeasurableOperator hL2 u + rieszSecondL2MeasurableOperator hL2 v

theorem CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator_smul_ae {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (c : ℝ) (u : ↥rieszSecondL2) : rieszSecondL2MeasurableOperator hL2 (c • u) =ᵐ[MeasureTheory.volume] c • rieszSecondL2MeasurableOperator hL2 u

theorem CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator_eLpNorm_le {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (u : ↥rieszSecondL2) : MeasureTheory.eLpNorm (rieszSecondL2MeasurableOperator hL2 u) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (↑↑u) 2 MeasureTheory.volume

theorem CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator_l2_bound {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (u : ↥rieszSecondL2) : ∫⁻ (x : Parabolic.Vec3), absE (rieszSecondL2MeasurableOperator hL2 u) x ^ 2 ≤ ∫⁻ (x : Parabolic.Vec3), absE (↑↑u) x ^ 2

theorem CKN.Foundation.Euclidean.rieszSecondL2MeasurableOperator_smooth_global_bound {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {F : Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) : ∫⁻ (x : Parabolic.Vec3), absE (rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp F ⋯)) x ^ 2 ≤ ∫⁻ (x : Parabolic.Vec3), absE F x ^ 2

theorem CKN.Foundation.Euclidean.rieszSecondL2_weak_type_of_cz_certificate {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level C₂ A : ℝ} {C_H : ENNReal} (hL2 : RieszSecondL2Input i j) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hlevel : 0 < level) (hA : 0 ≤ A) (hAeq : dyadicL1Norm F = ENNReal.ofReal A) {G B : CZDecomposition F level → Parabolic.Vec3 → ℝ} (hdecomp : ∀ (D : CZDecomposition F level) (x : Parabolic.Vec3), rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp F hF₂) x = G D x + B D x) (henergy : ∀ (D : CZDecomposition F level), ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2 ≤ 8 * level * A) (hgoodL2 : ∀ (D : CZDecomposition F level), MeasureTheory.Integrable (fun (x : Parabolic.Vec3) => G D x ^ 2) MeasureTheory.volume ∧ ∫ (x : Parabolic.Vec3), G D x ^ 2 ≤ C₂ ^ 2 * ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2) (hbad : ∀ (D : CZDecomposition F level), ∃ (Tbad : { Q : DyadicIndex // Q ∈ D.cubes } → Parabolic.Vec3 → ℝ), MeasureTheory.Integrable (B D) MeasureTheory.volume ∧ (∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |B D x| ≤ ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ENNReal.ofReal |Tbad Q x|) ∧ (∀ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), AEMeasurable (fun (x : Parabolic.Vec3) => ENNReal.ofReal |Tbad Q x|) (MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ)) ∧ ∀ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |Tbad Q x| ≤ C_H * ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x|) : MeasureTheory.volume {x : Parabolic.Vec3 | level < |rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp F hF₂) x|} ≤ ENNReal.ofReal (8 * C₂ ^ 2 * level / (level / 2) ^ 2) * ENNReal.ofReal A + ENNReal.ofReal (32 * Real.pi * √3) * (ENNReal.ofReal A / ENNReal.ofReal level) + C_H * (2 * ENNReal.ofReal A) / ENNReal.ofReal (level / 2)

structure CKN.Foundation.Euclidean.RieszSecondL2CZCertificate {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (F : Parabolic.Vec3 → ℝ) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (level : ℝ) : Type

Good and bad output decomposition with quantitative data for the weak-(1,1) estimate.

• A : ℝ

  Finite real value of the source L¹ mass in the Calderón–Zygmund certificate.

• hA : 0 ≤ self.A
• hAeq : dyadicL1Norm F = ENNReal.ofReal self.A
• G : CZDecomposition F level → Parabolic.Vec3 → ℝ

  Good contribution to the operator output in the Calderón–Zygmund certificate.

• B : CZDecomposition F level → Parabolic.Vec3 → ℝ

  Bad contribution to the operator output in the Calderón–Zygmund certificate.

• hdecomp (D : CZDecomposition F level) (x : Parabolic.Vec3) : rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp F hF₂) x = self.G D x + self.B D x
• henergy (D : CZDecomposition F level) : ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2 ≤ 8 * level * self.A
• hgoodL2 (D : CZDecomposition F level) : MeasureTheory.Integrable (fun (x : Parabolic.Vec3) => self.G D x ^ 2) MeasureTheory.volume ∧ ∫ (x : Parabolic.Vec3), self.G D x ^ 2 ≤ 1 ^ 2 * ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2
• hbad (D : CZDecomposition F level) : ∃ (Tbad : { Q : DyadicIndex // Q ∈ D.cubes } → Parabolic.Vec3 → ℝ), MeasureTheory.Integrable (self.B D) MeasureTheory.volume ∧ (∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |self.B D x| ≤ ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ENNReal.ofReal |Tbad Q x|) ∧ (∀ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), AEMeasurable (fun (x : Parabolic.Vec3) => ENNReal.ofReal |Tbad Q x|) (MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ)) ∧ ∀ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |Tbad Q x| ≤ ENNReal.ofReal (64 * Real.pi * rieszSecondKernelC₂) * ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x|

noncomputable def CKN.Foundation.Euclidean.rieszSecondWeakTypeConstant : ℝ

Explicit weak-(1,1) coefficient assembled from the decomposition and kernel bounds.

Equations

• CKN.Foundation.Euclidean.rieszSecondWeakTypeConstant = 32 + 32 * Real.pi * √3 + 256 * Real.pi * CKN.Foundation.Euclidean.rieszSecondKernelC₂

theorem CKN.Foundation.Euclidean.rieszSecondKernelC_H : ENNReal.ofReal (64 * Real.pi * rieszSecondKernelC₂) = ENNReal.ofReal 1152

noncomputable def CKN.Foundation.Euclidean.rieszSecondL2RawOperator {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (f : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ℝ

Measurable second-Riesz operator on L² inputs, extended by zero outside L².

Equations

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

theorem CKN.Foundation.Euclidean.rieszSecondL2RawOperator_measurable {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : Measurable (rieszSecondL2RawOperator hL2 f)

theorem CKN.Foundation.Euclidean.rieszSecondL2RawOperator_ae_eq {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : rieszSecondL2RawOperator hL2 f =ᵐ[MeasureTheory.volume] rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp f hf)

theorem CKN.Foundation.Euclidean.rieszSecondL2_restricted_weak_type {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hcertificate : {F : Parabolic.Vec3 → ℝ} → {level : ℝ} → Measurable F → MeasureTheory.Integrable F MeasureTheory.volume → (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) → 0 < level → RieszSecondL2CZCertificate hL2 F hF₂ level) (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 hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l