Lebesgue differentiation theorem along shrinking cubes

Let $f:\mathbb{R}^d\to E$ be locally integrable, where $E$ is a real Banach space. Then for almost every $x\in\mathbb{R}^d$ the following holds: whenever $(a_j,s_j)_{j}$ is a family of corners and side lengths, indexed along a filter, such that $s_j\to 0^+$ and eventually $x\in Q(a_j,s_j)$, then

where $Q(a,s)=\{y:\ a_i\le y_i\le a_i+s\ \forall i\}$ is the closed cube with corner $a$ and side $s$. The exceptional null set does not depend on the family of cubes.

This is the Lebesgue differentiation theorem for (not necessarily centred) cubes shrinking to a point, in the form used when a function is compared with its averages over cubes.

Formalization Note. closedCube a s comes from Definitions.Def_DbarRegularity_Setting; $\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. The average is Mathlib's ⨍ y in Q, f y (setAverage). "Eventually" and the convergence $s_j\to0^+$ (Tendsto s l (𝓝[>] 0)) are with respect to an arbitrary filter l on an arbitrary index type; the quantifier over ι, l, a, s sits inside the almost-everywhere statement.