Theorem AkraBazziRecurrence.eventually_one_add_smoothingFn_r_pos
Modification history
2025-06-20 15:48
Mathlib/Computability/AkraBazzi/AkraBazzi.lean
chore: split long file AkraBazzi.lean (#26193) …
Modified AkraBazziRecurrence.eventually_one_add_smoothingFn_r_posView on Github →