Bennett two distance ratio le

Proved

D1Bound5.bennett_two_distance_ratio_le

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

Triangle geometry controls the same rational factor as in the paper. The assumptions hold for u=min(A,delta), v=max(A,delta), and A≤B.

Preamble

import Lean.Elab.Tactic.Omega
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

Formal statement

section
namespace D1Bound5






theorem _root_.D1Bound5.bennett_two_distance_ratio_le (B u v : ℝ)
    (hB : 0 < B) (hu : 0 < u) (huB : u ≤ B)
    (huv : u ≤ v) (hvB : v ≤ u + B) :
    v ^ 2 / (v - 2 * u / 5) ≤ (5 / 2 : ℝ) * B := by sorry





end D1Bound5
end

Source

D1Bound5/BennettTwoCoefficientConstants.lean, lines 51-69, SHA-256 034cf7aa6d3e853901a9f7bd5f2be74a2cd9af0c2f34f1de6a52a0f80541821b. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph