Existence of the dyadic Calderón--Zygmund decomposition

This module turns the maximal-cube estimates into the consumer-facing decomposition structure. The good and bad parts are integrated directly over the disjoint cube family.

theorem CKN.Foundation.Euclidean.exists_calderonZygmund_decomposition {F : Parabolic.Vec3 → ℝ} {height : ℝ} (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hheight : 0 < height) : ∃ (D : CZDecomposition F height), D.cubes = dyadicMaximalCubes F height