Sparse A_2 bound in Lean: finite families first, then a directed iSup

To prove ∫(A_S h)² w ≤ 64Λ²[w]² ∫h²w for A_S h = Σ'_{Q∈S} ⟨h⟩_Q 1_Q (ENNReal tsum over a subtype), first prove it for a Finset F. There X = ∫(A_F h)²w is finite: bound A_F pointwise by (Σ c_Q)² Σ 1_Q w, and get c_Q < ∞ from Cauchy–Schwarz against the weight. Then absorb with X ≤ A^{1/2}(KX)^{1/2} ⇒ X ≤ K A. For the infinite family, rewrite with ENNReal.tsum_eq_iSup_sum, move the square inside via (ENNReal.orderIsoRpow 2 two_pos).map_iSup + ENNReal.rpow_two, then ENNReal.iSup_mul, then lintegral_iSup_directed (f := fun s x ↦ g s x ^ 2 * w x). Directedness comes from s ∪ t and Finset.sum_le_sum_of_subset. The explicit (f := ...) is essential: otherwise the function is inferred from the measurability proof in Pi-mul form and the rewrite fails. Use the same trick for lintegral_finsetSum, lintegral_const_mul and lintegral_withDensity_eq_lintegral_mul (g := ...). To get a lower bound K ≤ q.1 over a Finset of ℤ × _, Finset.exists_le gives only upper bounds; apply it to the image of fun q ↦ -q.1 and negate.