Riesz Second

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

def CKN.Foundation.Euclidean.rieszSecondCubeStar (Q : DyadicIndex) : Set Parabolic.Vec3

The Euclidean 2√3 enlargement of a dyadic cube, with the cube's sup-radius dyadicScale Q.scale / 2.

Equations

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

theorem CKN.Foundation.Euclidean.rieszSecondCubeStar_volume (Q : DyadicIndex) : MeasureTheory.volume (rieszSecondCubeStar Q) ≤ ENNReal.ofReal (32 * Real.pi * √3) * MeasureTheory.volume (dyadicCubeSet Q)

The enlarged cube has the explicit volume comparison needed in the bad region estimate.

theorem CKN.Foundation.Euclidean.rieszSecondCubeStar_volume_sum {F : Parabolic.Vec3 → ℝ} {height : ℝ} (D : CZDecomposition F height) : ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), MeasureTheory.volume (rieszSecondCubeStar ↑Q) ≤ ENNReal.ofReal (32 * Real.pi * √3) * (dyadicL1Norm F / ENNReal.ofReal height)

theorem CKN.Foundation.Euclidean.rieszSecond_bad_output_measure {F : Parabolic.Vec3 → ℝ} {height level : ℝ} (D : CZDecomposition F height) (hlevel : 0 < level) {B : Parabolic.Vec3 → ℝ} (hB : MeasureTheory.Integrable B MeasureTheory.volume) {C_H : ENNReal} (hBoutside : ∫⁻ (x : Parabolic.Vec3) in (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |B x| ≤ C_H * (2 * dyadicL1Norm F)) : MeasureTheory.volume {x : Parabolic.Vec3 | level < |B x|} ≤ ENNReal.ofReal (32 * Real.pi * √3) * (dyadicL1Norm F / ENNReal.ofReal height) + C_H * (2 * dyadicL1Norm F) / ENNReal.ofReal level

theorem CKN.Foundation.Euclidean.rieszSecond_bad_cube_bridge {K b : Parabolic.Vec3 → ℝ} {Q : DyadicIndex} {C_H : ENNReal} (hC_H : C_H ≠ ⊤) (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) => K (x - y) * b y) (dyadicCubeSet Q) MeasureTheory.volume) (hjoint : AEMeasurable (fun (z : Parabolic.Vec3 × Parabolic.Vec3) => ENNReal.ofReal |(K (z.1 - z.2) - K (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 |(K (z.2 - z.1) - K (z.2 - dyadicCubeCenter Q.scale Q.corner)) * b z.1|) ((MeasureTheory.volume.restrict (dyadicCubeSet Q)).prod (MeasureTheory.volume.restrict (rieszSecondCubeStar Q)ᶜ))) (hExt : ∀ y ∈ dyadicCubeSet Q, ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar Q)ᶜ, ENNReal.ofReal |K (x - y) - K (x - dyadicCubeCenter Q.scale Q.corner)| ≤ C_H) : ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar Q)ᶜ, ENNReal.ofReal |∫ (y : Parabolic.Vec3) in dyadicCubeSet Q, K (x - y) * b y| ≤ C_H * ∫⁻ (y : Parabolic.Vec3) in dyadicCubeSet Q, ENNReal.ofReal |b y|

theorem CKN.Foundation.Euclidean.rieszSecond_bad_cube_bridge_of_kernel {K b : Parabolic.Vec3 → ℝ} {Q : DyadicIndex} {C₂ : ℝ} (hC₂ : 0 ≤ C₂) (hKmeas : Measurable K) (hdiff : ∀ (x : Parabolic.Vec3), x ≠ 0 → DifferentiableAt ℝ K x) (hgrad : ∀ (x : Parabolic.Vec3), x ≠ 0 → ‖fderiv ℝ K x‖ ≤ C₂ * Parabolic.vec3EuclideanNorm x ^ (-4)) (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) => K (x - y) * b y) (dyadicCubeSet Q) MeasureTheory.volume) (hjoint : AEMeasurable (fun (z : Parabolic.Vec3 × Parabolic.Vec3) => ENNReal.ofReal |(K (z.1 - z.2) - K (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 |(K (z.2 - z.1) - K (z.2 - dyadicCubeCenter Q.scale Q.corner)) * b z.1|) ((MeasureTheory.volume.restrict (dyadicCubeSet Q)).prod (MeasureTheory.volume.restrict (rieszSecondCubeStar Q)ᶜ))) : ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar Q)ᶜ, ENNReal.ofReal |∫ (y : Parabolic.Vec3) in dyadicCubeSet Q, K (x - y) * b y| ≤ ENNReal.ofReal (64 * Real.pi * C₂) * ∫⁻ (y : Parabolic.Vec3) in dyadicCubeSet Q, ENNReal.ofReal |b y|

theorem CKN.Foundation.Euclidean.rieszSecond_good_part_chebyshev {F : Parabolic.Vec3 → ℝ} {height level C A : ℝ} (D : CZDecomposition F height) (hheight : 0 < height) (hlevel : 0 < level) (hA : 0 ≤ A) (henergy : ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2 ≤ 8 * height * A) {T : Parabolic.Vec3 → ℝ → ℝ} (hT : MeasureTheory.Integrable (fun (x : Parabolic.Vec3) => T x (dyadicGoodPart F D.cubes x) ^ 2) MeasureTheory.volume) (hL2 : ∫ (x : Parabolic.Vec3), T x (dyadicGoodPart F D.cubes x) ^ 2 ≤ C ^ 2 * ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2) : MeasureTheory.volume {x : Parabolic.Vec3 | level < |T x (dyadicGoodPart F D.cubes x)|} ≤ ENNReal.ofReal (8 * C ^ 2 * height / level ^ 2) * ENNReal.ofReal A

The good part estimate after the (L^2) operator bound and Chebyshev.

theorem CKN.Foundation.Euclidean.rieszSecond_hormander_kernel_condition {K : Parabolic.Vec3 → ℝ} {C₂ : ℝ} (hC₂ : 0 ≤ C₂) (hdiff : ∀ (x : Parabolic.Vec3), x ≠ 0 → DifferentiableAt ℝ K x) (hgrad : ∀ (x : Parabolic.Vec3), x ≠ 0 → ‖fderiv ℝ K x‖ ≤ C₂ * Parabolic.vec3EuclideanNorm x ^ (-4)) {y : Parabolic.Vec3} (hy : y ≠ 0) : ∫⁻ (x : Parabolic.Vec3) in {x : Parabolic.Vec3 | 2 * Parabolic.vec3EuclideanNorm y < Parabolic.vec3EuclideanNorm x}, ENNReal.ofReal |K (x - y) - K x| ≤ ENNReal.ofReal (64 * Real.pi * C₂)

The summed bad-part estimate supplied by the Hörmander integral bound.

theorem CKN.Foundation.Euclidean.rieszSecond_hormander_sum_bound {F : Parabolic.Vec3 → ℝ} {height : ℝ} (D : CZDecomposition F height) {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {C_H : ENNReal} (hH : ∀ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |T (dyadicBadPart F ↑Q) x| ≤ C_H * ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x|) : ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |T (dyadicBadPart F ↑Q) x| ≤ C_H * (2 * dyadicL1Norm F)

theorem CKN.Foundation.Euclidean.rieszSecond_hormander_sum_bound_of_kernel {F : Parabolic.Vec3 → ℝ} {height : ℝ} (D : CZDecomposition F height) {T : (Parabolic.Vec3 → ℝ) → Parabolic.Vec3 → ℝ} {K : Parabolic.Vec3 → ℝ} {C₂ : ℝ} (hC₂ : 0 ≤ C₂) (hdiff : ∀ (x : Parabolic.Vec3), x ≠ 0 → DifferentiableAt ℝ K x) (hgrad : ∀ (x : Parabolic.Vec3), x ≠ 0 → ‖fderiv ℝ K x‖ ≤ C₂ * Parabolic.vec3EuclideanNorm x ^ (-4)) (hH : ∀ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), (∀ (y : Parabolic.Vec3), y ≠ 0 → ∫⁻ (x : Parabolic.Vec3) in {x : Parabolic.Vec3 | 2 * Parabolic.vec3EuclideanNorm y < Parabolic.vec3EuclideanNorm x}, ENNReal.ofReal |K (x - y) - K x| ≤ ENNReal.ofReal (64 * Real.pi * C₂)) → ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |T (dyadicBadPart F ↑Q) x| ≤ ENNReal.ofReal (64 * Real.pi * C₂) * ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x|) : ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |T (dyadicBadPart F ↑Q) x| ≤ ENNReal.ofReal (64 * Real.pi * C₂) * (2 * dyadicL1Norm F)

theorem CKN.Foundation.Euclidean.rieszSecond_bad_part_exterior_bound {F : Parabolic.Vec3 → ℝ} {height : ℝ} (D : CZDecomposition F height) {B : Parabolic.Vec3 → ℝ} {Tbad : { Q : DyadicIndex // Q ∈ D.cubes } → Parabolic.Vec3 → ℝ} {C_H : ENNReal} (hpoint : ∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |B x| ≤ ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), ENNReal.ofReal |Tbad Q x|) (hmeas : ∀ (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)ᶜ)) (hbridge : ∀ (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|) : ∫⁻ (x : Parabolic.Vec3) in (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |B x| ≤ C_H * (2 * dyadicL1Norm F)

theorem CKN.Foundation.Euclidean.rieszSecond_weak_type_unconditional {F : Parabolic.Vec3 → ℝ} {level C₂ A : ℝ} {C_H : ENNReal} (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hlevel : 0 < level) (hA : 0 ≤ A) (hAeq : dyadicL1Norm F = ENNReal.ofReal A) {T : Parabolic.Vec3 → ℝ} {G B : CZDecomposition F level → Parabolic.Vec3 → ℝ} (hdecomp : ∀ (D : CZDecomposition F level) (x : Parabolic.Vec3), T x = G D x + B D x) (henergy : ∀ (D : CZDecomposition F level), ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2 ≤ 8 * level * A) (hL2 : ∀ (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 < |T 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)