Riesz Second Weak Assembly

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

noncomputable def CKN.Foundation.Euclidean.czGood {level : ℝ} (F : Parabolic.Vec3 → ℝ) (D : CZDecomposition F level) : Parabolic.Vec3 → ℝ

Good function supplied by a chosen Calderón–Zygmund decomposition.

Equations

• CKN.Foundation.Euclidean.czGood F D = CKN.Foundation.Euclidean.dyadicGoodPart F D.cubes

noncomputable def CKN.Foundation.Euclidean.czBad {level : ℝ} (F : Parabolic.Vec3 → ℝ) (D : CZDecomposition F level) (Q : { Q : DyadicIndex // Q ∈ D.cubes }) : Parabolic.Vec3 → ℝ

Mean-zero bad piece associated with one cube of a Calderón–Zygmund decomposition.

Equations

• CKN.Foundation.Euclidean.czBad F D Q = CKN.Foundation.Euclidean.dyadicBadPart F ↑Q

theorem CKN.Foundation.Euclidean.dyadic_good_part_memLp_two {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) : MeasureTheory.MemLp (dyadicGoodPart F D.cubes) 2 MeasureTheory.volume

theorem CKN.Foundation.Euclidean.dyadic_good_part_energy {F : Parabolic.Vec3 → ℝ} {level A : ℝ} (D : CZDecomposition F level) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hA : 0 ≤ A) (hAeq : dyadicL1Norm F = ENNReal.ofReal A) : ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2 ≤ 8 * level * A

theorem CKN.Foundation.Euclidean.dyadic_bad_part_memLp_two {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (Q : { Q : DyadicIndex // Q ∈ D.cubes }) : MeasureTheory.MemLp (dyadicBadPart F ↑Q) 2 MeasureTheory.volume

theorem CKN.Foundation.Euclidean.dyadic_good_bad_decomposition_ae {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) : F =ᵐ[MeasureTheory.volume] fun (x : Parabolic.Vec3) => dyadicGoodPart F D.cubes x + ∑' (Q : { Q : DyadicIndex // Q ∈ D.cubes }), dyadicBadPart F (↑Q) x

theorem CKN.Foundation.Euclidean.dyadic_bad_sum_memLp_two {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => F x - dyadicGoodPart F D.cubes x) 2 MeasureTheory.volume

theorem CKN.Foundation.Euclidean.rieszSecond_good_output_l2 {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (hL2 : RieszSecondL2Input i j) (D : CZDecomposition F level) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) : MeasureTheory.MemLp (rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicGoodPart F D.cubes) ⋯)) 2 MeasureTheory.volume ∧ ∫ (x : Parabolic.Vec3), rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicGoodPart F D.cubes) ⋯) x ^ 2 ≤ ∫ (x : Parabolic.Vec3), dyadicGoodPart F D.cubes x ^ 2

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

Second-Riesz kernel with the sign convention for pressure reconstruction.

Equations

• CKN.Foundation.Euclidean.rieszSecondPressureKernel i j z = -CKN.Foundation.Euclidean.rieszSecondKernel i j z

theorem CKN.Foundation.Euclidean.rieszSecond_bad_part_interface_of_cube {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) (hdata : ∀ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), MeasureTheory.IntegrableOn (dyadicBadPart F ↑Q) (dyadicCubeSet ↑Q) MeasureTheory.volume ∧ (∀ x ∈ (rieszSecondCubeStar ↑Q)ᶜ, MeasureTheory.IntegrableOn (fun (y : Parabolic.Vec3) => rieszSecondKernel i j (x - y) * dyadicBadPart F (↑Q) y) (dyadicCubeSet ↑Q) MeasureTheory.volume) ∧ 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)) * dyadicBadPart F (↑Q) z.2|) ((MeasureTheory.volume.restrict (rieszSecondCubeStar ↑Q)ᶜ).prod (MeasureTheory.volume.restrict (dyadicCubeSet ↑Q))) ∧ 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)) * dyadicBadPart F (↑Q) z.1|) ((MeasureTheory.volume.restrict (dyadicCubeSet ↑Q)).prod (MeasureTheory.volume.restrict (rieszSecondCubeStar ↑Q)ᶜ))) (Q : { Q : DyadicIndex // Q ∈ D.cubes }) : ∃ (Tbad : Parabolic.Vec3 → ℝ), AEMeasurable (fun (x : Parabolic.Vec3) => ENNReal.ofReal |Tbad x|) (MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), 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₂) * ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x|

theorem CKN.Foundation.Euclidean.measurableSet_rieszSecondCubeStar_assembly (Q : DyadicIndex) : MeasurableSet (rieszSecondCubeStar Q)

theorem CKN.Foundation.Euclidean.dyadicL1Norm_lt_top_of_integrable {F : Parabolic.Vec3 → ℝ} (hF : MeasureTheory.Integrable F MeasureTheory.volume) : dyadicL1Norm F < ⊤

noncomputable def CKN.Foundation.Euclidean.rieszSecondL2CzCertificateOfInterfaces {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (hL2 : RieszSecondL2Input i j) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hlevel : 0 < level) (hcountable : ∀ (D : CZDecomposition F level), ∃ (Tbad : { Q : DyadicIndex // Q ∈ D.cubes } → Parabolic.Vec3 → ℝ), (∀ᵐ (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 }), 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|) : RieszSecondL2CZCertificate hL2 F hF₂ level

Assemble a Calderón–Zygmund certificate from countable additivity and exterior estimates.

Equations

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

theorem CKN.Foundation.Euclidean.rieszSecondL2_strong_type_of_restricted_inputs {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {A₁ p : ℝ} (hTsub : ∀ (f g : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → Measurable g → MeasureTheory.MemLp g 2 MeasureTheory.volume → ∀ (x : Parabolic.Vec3), |rieszSecondL2RawOperator hL2 (f + g) x| ≤ |rieszSecondL2RawOperator hL2 f x| + |rieszSecondL2RawOperator hL2 g x|) (hWeak11 : ∀ (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 A₁ * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (hA₁ : 0 ≤ A₁) (hp1 : 1 < p) (hp2 : p < 2) {f : Parabolic.Vec3 → ℝ} (hf : Measurable f) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) (hf₂ : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∫⁻ (x : Parabolic.Vec3), absE (rieszSecondL2RawOperator hL2 f) x ^ p ≤ ENNReal.ofReal (p * (2 ^ p * (A₁ / (p - 1) + 1 ^ 2 / (2 - p)))) * ∫⁻ (x : Parabolic.Vec3), absE f x ^ p