Vanishing of atomic mass on a coordinate fibre

Let $\iota$ be a type and $X$ a compact subset of $(\mathbb{C}\times\mathbb{C})^{\iota}$ with the product topology. Let $(a_i)_{i\in\mathbb{N}}$ be complex numbers with $\sum_i \|a_i\|$ summable, let $(x_i)_{i\in\mathbb{N}}$ be points of $X$, let $\Lambda : C(X,\mathbb{C}) \to \mathbb{C}$ be a continuous $\mathbb{C}$-linear functional, let $F$ be a finite subset of $\iota$ and let $\tau \in (\mathbb{C}\times\mathbb{C})^{\iota}$. Two hypotheses are imposed. First, $\Lambda$ carries no mass on cylinders at $F$ around $\tau$: for every $\varepsilon > 0$ there is a family of sets $U_k \subseteq \mathbb{C}\times\mathbb{C}$ with $U_k$ open and $\tau_k \in U_k$ for all $k \in F$, such that $\|\Lambda g\| < \varepsilon$ for every $g \in C(X,\mathbb{C})$ satisfying $\|g(y)\| \le 1$ for all $y$ and $g(y) = 0$ whenever $y \in X$ has $y_k \notin U_k$ for some $k \in F$. Second, $\Lambda$ is computed by the atomic sum on the coordinate algebra: $\sum'_i a_i\, g(x_i) = \Lambda g$ for every $g$ in the unital $*$-subalgebra of $C(X,\mathbb{C})$ generated by the $2|F|$ coordinate functions $y \mapsto (y_k)_1$ and $y \mapsto (y_k)_2$, $k \in F$. The conclusion is that the sum of $a_i$ over the subtype of indices $i$ with $x_i(k) = \tau(k)$ for all $k \in F$ equals $0$.

This is a separation statement for atomic measures: a functional with no mass near $\tau$ on the finitely many coordinates in $F$ forces the atoms lying in the level-$F$ fibre of $\tau$ to cancel, the coordinate $*$-algebra being uniformly dense by Stone–Weierstrass. It is used in the analytic input to the comparison of fibre sums for automorphic forms, via AutomorphicForm.forall_finset_fibreSum_sub_const_mul_fibreSum_add_eq_zero_of_forall_places_exists_noAtomicMass_wordSum_eq.