A small relative error controls the logarithm

Proved

BianchiIX.abs_log_le_twice_error

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

For real $t,e$ , if $e\leq1/4$ and $|t-1|\leq e$ , then $|\log t|\leq2e$ .

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX

Formal statement

theorem BianchiIX.abs_log_le_twice_error {t e : ℝ} (he : e ≤ 1 / 4) (ht : |t - 1| ≤ e) :
    |Real.log t| ≤ 2 * e := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/InverseLogDistortion.lean#L11-L22

View graph