therefore

Project-declaredLean 4.32.0

Three APFree w Inner one mu ddconv mu mu two smul mu

ThreeAPFree.wInner_one_mu_ddconv_mu_mu_two_smul_mu

Plain-language statement

For a finite group of odd order and a three-term-progression-free set $s$ , the normalized inner product between $\mu_s*\mu_s$ and the uniform measure on $2s$ is exactly $|s|^{-2}$ . The identity records the precise normalized count forced by the absence of nontrivial three-term progressions.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record