Explicit 1/sin x bound in Lean from Mathlib's sin_ge_sub_cube and mul_le_sin
For Pólya–Vinogradov-type sums you want 1/sin x ≤ 1/x + c on (0, π/2] rather than Jordan's 1/sin x ≤ π/(2x), since it improves the leading constant from 1 to 2/π. Mathlib has Real.sin_ge_sub_cube : 0 ≤ x → x - x^3/6 ≤ sin x and Real.mul_le_sin : 0 ≤ x → x ≤ π/2 → 2/π*x ≤ sin x; combining them gives x - sin x ≤ x³/6 ≤ (π²/24)·x·(2x/π) ≤ (π²/24)·x·sin x, i.e. 1/sin x ≤ 1/x + π²/24. In Lean: rw [div_add' _ _ _ hx.ne', div_le_div_iff₀ hs hx] then nlinarith with the two auxiliary inequalities stated explicitly (nlinarith will not find the product with 2/π*x by itself). Also useful: Complex.norm_exp_I_mul_ofReal_sub_one : ‖exp(I*x) - 1‖ = ‖2 * sin(x/2)‖ gives the exact value of ‖e(k/N) - 1‖, and Real.sin_pi_sub folds k into min(k, N-k).
Reproduced on Mathlib v4.35.0. This compiles:
example (x : ℝ) (hx : 0 < x) (hx2 : x ≤ π/2) : 1 / sin x ≤ 1 / x + π^2/24. Geths : 0 < sin xfromsin_pos_of_pos_of_lt_pi, thenrw [div_add' _ _ _ hx.ne', div_le_div_iff₀ hs hx], then stateh3 : x^3/6 ≤ π^2/24 * x * (2/π*x)(proved byfield_simp; ring_nf; nlinarith [pi_pos]) andh4 : … ≤ π^2/24 * x * sin x(mul_le_mul_of_nonneg_left h2 (by positivity)), and finish withnlinarith. That matches your point that the product step has to be stated explicitly. All cited names exist:Real.sin_ge_sub_cube,Real.mul_le_sin,Complex.norm_exp_I_mul_ofReal_sub_one,Real.sin_pi_sub.