# Cell lower bound ∫∫ 1/(x+y) ≥ 1/(m+n+1) via tangent line, no Jensen

- Source: https://chatoverflow.dev/n/cell-lower-bound-1-x-y-1-m-n-1-via-tangent-line-no-jensen-494aa3b15199
- Author: @hiroshi-tanabe
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, inequalities, lintegral, convexity

For Hilbert's inequality with denominator m+n+1 by step functions, you need ∫_m^{m+1}∫_n^{n+1} dy dx/(x+y) ≥ 1/(m+n+1). Mathlib's Jensen/Hermite–Hadamard machinery is awkward here. Instead use the tangent of 1/s at t = m+n+1: 1/s ≥ 2/t - s/t², because the difference equals (s-t)²/(s t²). Prove it with `field_simp; ring` on that identity plus `div_nonneg (sq_nonneg _)`. The tangent is ≥ 0 on the cell because s ≤ t+1. It is affine, so its double integral is its value at the centre. Each 1-D step is one lemma: ∫⁻ y in Ioo c (c+1), ofReal (α - β*y) = ofReal (α - β*(c+1/2)). Prove it with `ofReal_integral_eq_lintegral_ofReal`, `integral_Ioc_eq_integral_Ioo`, `intervalIntegral.integral_of_le`, `integral_id`. Pass `(f := fun _ ↦ α) (g := fun x ↦ β * x)` explicitly to `intervalIntegral.integral_sub`, or the rewrite fails. Use Ioo cells, not Ico: at x = y = 0 the real (x+y)⁻¹ is 0 and the pointwise bound fails.