Prove2Me

One amplitude threshold supplies every retained digit condition

Proved
BianchiIX.exists_retained_era_parameter_budget

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

bianchi-ix-era-statisticsdynamical-systems

Let ε>0\varepsilon>0, C≥0C\geq0, J∈NJ\in\mathbb N, 0<σ<10<\sigma<1, and 2Jσ<12J\sigma<1. There exists B∗∈(0,1)B_*\in(0,1) such that for every 0<B≤B∗0<B\leq B_*, writing β=Bσ\beta=B^\sigma, one has

0<β<1/160,B≤ε(β/2)2J,CB<β/4.0<\beta<1/160,\quad B\leq\varepsilon(\beta/2)^{2J}, \quad CB<\beta/4.

Moreover, every m∈Nm\in\mathbb N with m+1≤1/βm+1\leq1/\beta satisfies

2B(m+2−β)≤ε.2B(m+2-\beta)\leq\varepsilon.
Preamble
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Analysis.Calculus.ContDiff.Deriv
import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set
Formal statement
theorem BianchiIX.exists_retained_era_parameter_budget {ε C σ : ℝ} {J : ℕ}
    (hε : 0 < ε) (hC : 0 ≤ C) (hσ : 0 < σ) (hσone : σ < 1)
    (hσJ : σ * (2 * J : ℕ) < 1) :
    ∃ Bstar : ℝ, 0 < Bstar ∧ Bstar < 1 ∧ ∀ B ∈ Ioc 0 Bstar,
      let β := B ^ σ
      0 < β ∧ β < 1 / 160 ∧ B ≤ ε * (β / 2) ^ (2 * J) ∧ C * B < β / 4 ∧
      ∀ m : ℕ, (m : ℝ) + 1 ≤ 1 / β → B * (2 * ((m : ℝ) + 2 - β)) ≤ ε := by sorry
Source
https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/RetainedEraParameters.lean#L9-L58

View graph