Bennett prefactor absorb

Proved

D1Bound5.bennett_prefactor_absorb

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

diophantine-tuplesnumber-theory

A prefactor at least one can be absorbed into an exponential at every positive order, allowing the preceding exact rational slack to be used.

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_prefactor_absorb (M H : ℝ) (hM : 1 ≤ M) (hH : 0 ≤ H)
    (k : ℕ) (hk : 1 ≤ k) : M * H ^ k ≤ (M * H) ^ k := by sorry

end D1Bound5
end

Source

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

View graph