Riesz Second Weak Countable

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

theorem CKN.Foundation.Euclidean.rieszSecond_countable_bad_additivity_infinite {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) [Infinite { Q : DyadicIndex // Q ∈ D.cubes }] (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) {C_H : ENNReal} (hC_H : C_H ≠ ⊤) (hbridge : ∀ (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 * ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x|) : (∀ᵐ (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 }), rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x) ∧ ∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, Summable fun (Q : { Q : DyadicIndex // Q ∈ D.cubes }) => |rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x|

theorem CKN.Foundation.Euclidean.rieszSecond_countable_bad_additivity {i j : Fin 3} (hL2 : RieszSecondL2Input i j) {F : Parabolic.Vec3 → ℝ} {level : ℝ} (D : CZDecomposition F level) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hF₂ : MeasureTheory.MemLp F 2 MeasureTheory.volume) {C_H : ENNReal} (hC_H : C_H ≠ ⊤) (hbridge : ∀ (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 * ∫⁻ (x : Parabolic.Vec3) in dyadicCubeSet ↑Q, ENNReal.ofReal |dyadicBadPart F (↑Q) x|) : (∀ᵐ (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 }), rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x) ∧ ∀ᵐ (x : Parabolic.Vec3) ∂MeasureTheory.volume.restrict (⋃ (Q : { Q : DyadicIndex // Q ∈ D.cubes }), rieszSecondCubeStar ↑Q)ᶜ, Summable fun (Q : { Q : DyadicIndex // Q ∈ D.cubes }) => |rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp (dyadicBadPart F ↑Q) ⋯) x|