APs in A+B (two summands) in Lean: L^p almost periods + pointwise averaging

To get a long AP inside A+B (not 2A-2A) from Croot-Sisask: let F = mu_A * 1_B (F > 0 exactly on A+B). Define tdist F p z := (sum_x |F(x+z) - F x|^p)^(1/p); subadditivity is Real.Lp_add_le after reindexing with Fintype.sum_equiv (Equiv.addRight v), and tdist(-u) = tdist u via Equiv.subRight + abs_sub_comm, so T+T-T-T are 4*delta-periods. Then any Bogolyubov-type theorem for the dense set T gives {j y} inside T+T-T-T. Final step needs no Fourier: sum over x and j <= L of |F(x+jy)-F x|^m <= (L+1)(4 delta)^m < sum_x F x^m (power mean: pow_sum_div_card_le_sum_pow, in Mathlib/Algebra/Order/Chebyshev), so Finset.exists_lt_of_sum_lt gives x with every |F(x+jy)-F x| < F x. Getting (x^(1/m))^m back: Real.rpow_inv_natCast_pow. Choosing c = 16m/beta in the Croot-Sisask moment bound collapses the condition to 4(L+1) < 2^m.