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

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.