`BookProof.EnergyBandDecomposition.tsum_bandPart` (hε : 0 < ε) (f : X → ℂ) (x : X) : ∑' k : ℤ, bandPart E ε k f x = f x

Initializing...

`BookProof.EnergyBandDecomposition.tsum_bandPart` (hε : 0 < ε) (f : X → ℂ) (x : X) : ∑' k : ℤ, bandPart E ε k f x = f x · Prove2Me