Logarithmic repair budget and change of base

Proved

mme_repair_budget_log_le

by Robertboy18 · Sep 22, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

regional-extractiontensor-complexity

For every natural repair scale d and capacity C, the logarithm of the power-of-eight repair budget is at most log 8 plus (log 8 / log d) times log C. The statement uses the total natural and real logarithm conventions, including zero.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Algebra.Order.Archimedean.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
set_option autoImplicit false
universe u

Formal statement

theorem mme_repair_budget_log_le (d C : ℕ) :
    Real.log ((8 : ℝ) ^ (Nat.log d C + 1)) ≤
      Real.log 8 + (Real.log 8 / Real.log d) * Real.log C := by sorry

Source

Natural logarithm repair budgets, finite profile capacities, and exact-step copy rounding.

View graph