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