Reciprocal branches preserve digit-square value accuracy and logarithmic distortion

Proved

BianchiIX.reciprocal_gauss_estimates

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

bianchi-ix-era-statisticsdynamical-systems

Let $k:\mathbb R\to\mathbb R$ , $n\geq1$ , $y\geq0$ , $k(y)\geq n$ , and suppose $k'(y)=d>0$ , $|k(y)-(n+y)|\leq E\leq1/4$ , and $|\log d|\leq D$ . For $h(z)=1/k(z)$ and $g_n(z)=1/(n+z)$ , one has

h'(y)=-d/k(y)^2<0,\qquad |h(y)-g_n(y)|\leq E/n^2,

\left|\log\frac{|h'(y)|}{|g_n'(y)|}\right|\leq D+4E.

Preamble

import Definitions.Def_BianchiIX_Statistics_GaussInverse
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Mathlib.Analysis.Calculus.Deriv.Inv
import Mathlib.Analysis.Calculus.Deriv.Add
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Data.List.Induction

noncomputable section
open BianchiIX

Formal statement

theorem BianchiIX.reciprocal_gauss_estimates {k : ℝ → ℝ} {n y d E D : ℝ}
    (hn : 1 ≤ n) (hy : 0 ≤ y) (hk : n ≤ k y)
    (Hk : HasDerivAt k d y) (hd : 0 < d)
    (hvalue : |k y - (n + y)| ≤ E) (hsmall : E ≤ 1 / 4)
    (hlog : |Real.log d| ≤ D) :
    let h := fun z => 1 / k z
    HasDerivAt h (-d / (k y) ^ 2) y ∧ deriv h y < 0 ∧
      |h y - gaussInv n y| ≤ E / n ^ 2 ∧
      |Real.log (|deriv h y| / |deriv (gaussInv n) y|)| ≤ D + 4 * E := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/ReciprocalGaussEstimates.lean#L8-L52

View graph