Spatial nesting of dyadic and Gaussian cylinders

A rescaled dyadic cube lies in the inner Caccioppoli ball at its center, and the outer ball lies inside the Gaussian averaging ball.

theorem ESS.bu_short_dyadic_cell_space_inner (k : ℤ) (m : Fin 3 → ℤ) (ell : Fin 2048) (scale : ℝ) (hscale : 0 < scale) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ CKN.Foundation.buSmallTimeDyadicCell k m ell) : have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2; have X := scale • (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1; have r := √(scale ^ 2 * δ) / 8; scale • z.1 ∈ CKN.Foundation.Parabolic.vec3Ball X r

Spatial points of a dyadic cell map into the inner Caccioppoli ball at the dyadic midpoint.

theorem ESS.bu_short_caccioppoli_outer_space_subset (X : CKN.Foundation.Parabolic.Vec3) (τ : ℝ) (hτ : 0 < τ) : have r := √τ / 8; CKN.Foundation.Parabolic.vec3Ball X (2 * r) ⊆ CKN.Foundation.Parabolic.vec3Ball X √(3 * τ / 2)

The Caccioppoli outer ball is contained in the Gaussian averaging ball at the same physical center.