Monotonicity of the Rickert fraction in d

Proved

diophantine_case1_mono

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $F(t)=4(\\log C_1+\\log t)(\\log C_2+\\log t)/((\\log C_3+\\log t)(\\log C_4+\\log t))\$ with $\\log C_3\\le\\log C_1$ , $\\log C_4\\le\\log C_2$ and all eight one-sided logarithms positive. Then $F$ is decreasing: each ratio $(A+u)/(C+u)$ decreases since $(C-A)(u_2-u_1)\\le 0$ . Applied with $C_1=8.406\\cdot 10^{13}b^3$ etc. in Case 1 ( $b<2a$ ) of Theorem 1.1 of M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), to replace $d$ by its lower bound.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem diophantine_case1_mono (C1 C2 C3 C4 d0 : ℝ)
    (hAC : Real.log C3 ≤ Real.log C1)
    (hBD : Real.log C4 ≤ Real.log C2)
    (hLC1d0 : (0:ℝ) < Real.log (C1 * d0))
    (hLC2d0 : (0:ℝ) < Real.log (C2 * d0))
    (hLC3d0 : (0:ℝ) < Real.log (C3 * d0))
    (hLC4d0 : (0:ℝ) < Real.log (C4 * d0))
    (hC1pos : (0:ℝ) < C1) (hC2pos : (0:ℝ) < C2)
    (hC3pos : (0:ℝ) < C3) (hC4pos : (0:ℝ) < C4)
    (hd0pos : (0:ℝ) < d0) :
    ∀ t₁ t₂ : ℝ, d0 ≤ t₁ → t₁ ≤ t₂ →
      4 * (Real.log C1 + Real.log t₂) * (Real.log C2 + Real.log t₂)
        / ((Real.log C3 + Real.log t₂) * (Real.log C4 + Real.log t₂))
      ≤ 4 * (Real.log C1 + Real.log t₁) * (Real.log C2 + Real.log t₁)
        / ((Real.log C3 + Real.log t₁) * (Real.log C4 + Real.log t₁)) := by sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), proof of Theorem 1.1, case b < 2a (monotonicity in d)

View graph