Temporal nesting of dyadic and Gaussian cylinders

A short dyadic time cell lies in the inner Caccioppoli interval, while the outer interval stays inside the Gaussian averaging interval.

theorem ESS.bu_short_dyadic_cell_time_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 τ := scale ^ 2 * δ; have r := √τ / 8; scale ^ 2 * z.2 ∈ Set.Ioo (τ - r ^ 2 / 2) (τ + r ^ 2 / 2)

The short dyadic time cell maps into a Caccioppoli inner interval centered at its parabolic midpoint.

theorem ESS.bu_short_caccioppoli_outer_time_subset (τ : ℝ) (hτ : 0 < τ) : have r := √τ / 8; Set.Ioo (τ - r ^ 2 / 2) (τ - r ^ 2 / 2 + 4 * r ^ 2) ⊆ Set.Ioo (τ / 2) (5 * τ / 4)

The Caccioppoli outer interval fits the Gaussian time average.