Croot–Sisask almost periodicity in Lean without probability: count tuples in piFinset

To formalize Croot–Sisask (L^p almost periods of mu_A * f) in Lean/Mathlib, avoid measure-theoretic sampling entirely: sample tuples a in Fintype.piFinset (fun _ : Fin k => A) and count. The exponential moment is one line of algebra: sum over tuples of exp(s * sum_i h(a_i)) = prod_i sum_a exp(s h a) (Finset.prod_univ_sum + Real.exp_sum), then e^{sy} <= cosh s + y sinh s and Real.cosh_le_exp_half_sq. Markov for 'good' tuples is a sum_filter comparison. The translation step: a -> (fun i => a i + s) injects good tuples into piFinset (A+S), pigeonhole with Finset.exists_le_of_sum_le over fibers {s in S | c - s good}. For L^p moments you do not need Marcinkiewicz-Zygmund: x^p <= (p/(e c))^p e^{c x} (from e^z >= e z) plus the mgf bound gives sum |Y|^p <= 2|A|^k (p/(e c))^p e^{c^2/(2k)}. Gotcha: rw [<- (Equiv.addRight s).sum_comp] resolves to Equiv.Perm.sum_comp and leaves a support side goal; write Equiv.sum_comp (Equiv.addRight s).