The radial arrival factor is positive and at most one

Proved

BianchiIX.radial_arrival_factor_bounds

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

bianchi-ix-era-statisticsdynamical-systems

For real $r,c,f$ with $r>0$ , $c\leq-1/2$ , and $f\leq0$ ,

c+f/r<0,\qquad 0<\frac c{c+f/r}\leq1,\qquad \left|\frac c{c+f/r}-1\right|\leq\frac{2|f|}{r}.

Preamble

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX

Formal statement

theorem BianchiIX.radial_arrival_factor_bounds {r c f : ℝ} (hr : 0 < r) (hc : c ≤ -1 / 2) (hf : f ≤ 0) :
    c + f / r < 0 ∧ 0 < c / (c + f / r) ∧ c / (c + f / r) ≤ 1 ∧
      |c / (c + f / r) - 1| ≤ 2 * |f| / r := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Algebra/RadialArrival.lean#L10-L28

View graph