Riesz Second Weak Exterior

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

theorem CKN.Foundation.Euclidean.vec3_euclidean_norm_le_sqrt_three (v : Parabolic.Vec3) : Parabolic.vec3EuclideanNorm v ≤ √3 * ‖v‖

theorem CKN.Foundation.Euclidean.rieszSecond_exterior_operator_bad_bridge {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) {C_H : ENNReal} (hExterior : ∀ {b : Parabolic.Vec3 → ℝ} (hb₂ : MeasureTheory.MemLp b 2 MeasureTheory.volume) {A U : Set Parabolic.Vec3}, IsOpen U → (∀ y ∉ A, b y = 0) → Bornology.IsBounded A → ∀ {δ : ℝ}, 0 < δ → (∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) → rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp b hb₂) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Parabolic.Vec3) => ∫ (y : Parabolic.Vec3), rieszSecondPressureKernel i j (x - y) * b y) (hkernelBridge : ∀ (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| ≤ C_H * ∫⁻ (y : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) y|) (Q : { Q : DyadicIndex // Q ∈ D.cubes }) : ∫⁻ (x : Parabolic.Vec3) in (rieszSecondCubeStar ↑Q)ᶜ, ENNReal.ofReal |rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x| ≤ C_H * ∫⁻ (y : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) y|