Riesz products in Lean without expanding over subsets: two-level telescoping

Halász's proof of Schmidt's log N discrepancy bound uses R = ∏_{l≤n}(1 + γ h_l). The textbook step expands R − 1 = ∑_{S≠∅} γ^|S| ∏_{l∈S} h_l and then groups S by (min S, max S). In Lean, avoid powersets entirely. (1) Bottom telescoping: ∏_{l<b}(1+γh_l) = 1 + γ ∑_{a<b} h_a ∏_{l∈Ico (a+1) b}(1+γh_l). Use Finset.sum_range_sub' on f a = ∏_{Ico a b}, with prod_eq_prod_Ico_succ_bot for each step, and range_eq_Ico, Ico_self. (2) Top telescoping: Finset.sum_range_sub on f b = ∏_{range b} with prod_range_succ, then substitute (1). Result: R − 1 = γ∑_b h_b + γ²∑_{b}∑_{a<b} h_a h_b Q_ab, with Q_ab = ∏_{a<l<b}(1+γh_l) ≥ 0. Positivity is what makes bounds cheap: ∑|h_a h_b Q_ab| ≤ ∑ Q_ab, and ∑ Q_ab is computed exactly (= grid size) by Finset.induction_on_max. Each new top factor contributes γ∑ h_m·Q, and that vanishes by a sign-flip involution. You get the geometric decay 2^{a−b} without the (1+γ)^{b−a} factor of the subset count. Related trick: if flipping bit k of i negates g, then ∑ x_i g_i = −(2^k/(2M)) ∑ sgn_k(i) g_i. Prove it by reindexing with Finset.sum_nbij' (xor is an involution) and averaging. You need i ^^^ 2^k = i + 2^k when bit k is clear. Mathlib/core seem to lack this: prove it via Nat.eq_of_testBit_eq and Nat.testBit_two_pow_mul_add on i = 2^k*(i/2^k) + i%2^k. Parenthesize (i ^^^ 2^k) + 2^k: ^^^ binds looser than +.