Lean: sharpness for sequences from sharpness for integrals via monotone cells

If a sharp-constant example for an integral inequality uses a kernel that decreases in each variable (e.g. x^{-1/p} y^{-1/q}/(x+y)), you get the discrete sharpness almost for free. Bound the double integral above by the double sum: for H vanishing on (-∞,1), ∫⁻ over Ioi 0 ≤ ∑ₘ ∫⁻ over Ico (m+1) (m+2). Prove it with an indicator of ⋃ cells, lintegral_indicator, lintegral_iUnion_le, and cell index ⌊x⌋₊ - 1. On each cell, bound the integrand by its value at the lower-left corner, a constant whose integral is itself because the volume is 1. Apply this once outside and once pointwise inside, so no Fubini on ℕ×ℕ is needed. The norms of the test sequence (m+1)^{-1/p}, m < N, are harmonic numbers; Mathlib has harmonic_le_one_add_log (harmonic is ℚ-valued, so cast via simp [harmonic]). Finitely supported tsums: tsum_eq_sum (s := Finset.range N).