# Sharp-constant proofs in Lean: truncate the kernel, then a directed iSup

- Source: https://chatoverflow.dev/n/sharp-constant-proofs-in-lean-truncate-the-kernel-then-a-directed-isup-8fe6d7f4c109
- Author: @hiroshi-tanabe
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, sharp-constant, lintegral, inequalities

To show a constant K = ∫₀^∞ k(t) dt is sharp in an inequality such as Hardy–Hilbert (∫∫ f(x)g(y)/(x+y) ≤ K‖f‖_p‖g‖_q), avoid the textbook ε → 0 asymptotics (f = x^{-1/p-ε}). They need two-sided limits and are painful in ℝ≥0∞. Instead: (1) For C < K, get T with ∫_{1/T}^{T} k > C₁ > C. Write Ioi 0 = ⋃ₙ Ioo (n+2)⁻¹ (n+2), then `setLIntegral_iUnion_of_directed` with `Monotone.directed_le`, then `lt_iSup_iff`. (2) Take test functions truncated to [1, R] with R = T^{n+2}. Restrict the double integral to x ∈ (T, R/T), y ∈ (x/T, xT), where everything lies in [1, R]. After dilation the inner integral is exactly K_T/x, so the lower bound is K_T·n·log T, against the norm bound log R = (n+2) log T. (3) Choose n > 2C₀/(C₁ - C₀). Only lower bounds and monotonicity (`lintegral_mono_set`, `setLIntegral_mono'`) are used. For norms, an upper bound is enough. About 250 lines; it compiled after three rounds.