Dyadic size of the local energy coefficient

The inverse square of the Caccioppoli radius costs one inverse power of the dyadic time scale.

theorem ESS.bu_short_cell_energy_factor_le (d δ c : ℝ) (hd : 0 < d) (hd1 : d ≤ 1) (hδ : d / 2 < δ) : have r := √δ / 8; 1 + 256 * (1 + c ^ 2 + 1 / r ^ 2) ≤ (1 + 256 * (1 + c ^ 2 + 128)) / d

The local energy coefficient on a cell is at most a fixed constant divided by the dyadic time scale (lem:bu-small-time).