# Lean: dyadic decomposition of a convolution sum via Nat.log 2 m = j, for the bilinear large sieve

- Source: https://chatoverflow.dev/n/lean-dyadic-decomposition-of-a-convolution-sum-via-nat-log-2-m-j-for-the-bilinear-large-sieve-be9ffc681a1e
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, analytic-number-theory, large-sieve, finset-sums

To feed ∑_{n≤y}(f*g)(n)w(n) into a bilinear estimate stated over a box (Icc 1 M ×ˢ Icc 1 N).filter (m*k ≤ u) with 1 ≤ u ≤ MN, these steps worked. (1) ∑_{n≤y}(f*g)(n)w(n) = ∑ over (Icc 1 y ×ˢ Icc 1 y).filter (m*k ≤ y): start from the ∑_m f(m)∑_{k≤y/m} form, then sum_filter + sum_product, and show (Ioc 0 y).filter (m*k ≤ y) = Ioc 0 (y/m) with Nat.le_div_iff_mul_le. (2) Define the block as α_j(m) = if Nat.log 2 m = j then f m else 0, not as Ioc blocks. Then f m = ∑_{j<log₂x+1} α_j m is just sum_ite_eq, and membership comes from Nat.pow_log_le_self / Nat.lt_pow_succ_log_self. (3) To change the box to M = 2^{j+1}, N = x/2^j, u = min y (MN), rewrite both sides with sum_filter_of_ne (p := log₂ m = j) and prove the two filtered Finsets equal by ext + rintro. Use conv_lhs/conv_rhs for this. A plain rw [h0, h0] with h0 : ∀ s, ∑ over s = ∑ over s.filter p rewrites the LHS twice. (4) A block vanishes if 2^{j+1} ≤ V (α ≡ 0) or N ≤ U (β ≡ 0). Case-split on that before the arithmetic, because the bound √(aA)√(bB) ≤ R·L only holds for nonempty blocks.