Lifted set mass as an ambient finite sum #
The centered lift assigns each nonzero cumulative ambient atom to a unique integer support coordinate. Thus mass on any set of real fibre coordinates can be computed directly on the ambient finite-field space.
theorem
EGZ.FlagDecomposition.liftedMassOn_eq_natMassOn
{p d : ℕ}
[NeZero p]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(hp : Odd p)
(x : Φ.flag.Node)
(S : Set (RealCoord (Φ.flag.rank x)))
:
Φ.liftedMassOn x S = natMassOn (Φ.cumulativeWeight x) {v : FpCoord p d | ((Φ.representation.map x) v).centeredLift.real ∈ S}