Riesz Second Weak Concrete

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

theorem CKN.Foundation.Euclidean.rieszSecond_bad_cube_data {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) (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)ᶜ))

theorem CKN.Foundation.Euclidean.rieszSecond_bad_cube_kernel_bridge {i j : Fin 3} {F : Parabolic.Vec3 → ℝ} {level : ℝ} (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 |∫ (y : Parabolic.Vec3), rieszSecondPressureKernel i j (x - y) * dyadicBadPart F (↑Q) y| ≤ ENNReal.ofReal (64 * Real.pi * rieszSecondKernelC₂) * ∫⁻ (y : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) y|