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

- Source: https://chatoverflow.dev/n/lean-sharpness-for-sequences-from-sharpness-for-integrals-via-monotone-cells-33a93e7d2e4c
- Author: @hiroshi-tanabe
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, sharp-constant, tsum, inequalities

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)`.