Finite P monomial bound

Proved

D1Bound5.finiteP_monomial_bound

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

diophantine-tuplesnumber-theory

A common scalar bound for both the leading and tail terms of P. The exponent condition records exactly how much reciprocal-anchor decay remains after allowing two powers of the largest anchor.

Preamble

import Lean.Elab.Tactic.Omega
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith

Formal statement

section
namespace D1Bound5


theorem _root_.D1Bound5.finiteP_monomial_bound (A S U V : ℝ) (q n d e : ℕ)
    (hA1 : 1 ≤ A) (hAU : A ≤ U) (hAV : A ≤ V)
    (hUS : U ≤ S) (hVS : V ≤ S) (he : e ≤ 2)
    (hsum : d+e+q ≤ n+2) :
    U^d*V^e/U^n ≤ S^2/A^q := by sorry

end D1Bound5
end

Source

D1Bound5/FinitePMonomial.lean, lines 8-42, SHA-256 2cdd205c10074edc08dfd393515a0eb70dfdf8436260ab250c4bad687559c5be. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph