feat: Asymptotic order of divide-and-conquer recurrences (Akra-Bazzi theorem) (#6583)

This PR proves the [Akra-Bazzi theorem](https://en.wikipedia.org/wiki/Akra%E2%80%93Bazzi_method), which gives the asymptotic order of divide-and-conquer recurrences of the form
```
T n = (∑ i in Fin k, a i * T (r i n)) + g n
```
where `T : ℕ → ℝ`, and where `r i n` is close to `b i * n` for a set of coefficients `b : Fin k → ℝ`. These recurrences arise mainly in the analysis of divide-and-conquer algorithms such as mergesort or Strassen's algorithm for matrix multiplication.

Note that the traditional proof first proves a continuous version (i.e. for `T : ℝ → ℝ`) and then discretizes it to get a version that is relevant for algorithms. Here we prove the discrete version directly, which shortens the proof considerably.

Author: dupuisf

Mathlib.lean

@@ -1353,6 +1353,8 @@ import Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
 import Mathlib.Combinatorics.Young.SemistandardTableau
 import Mathlib.Combinatorics.Young.YoungDiagram
 import Mathlib.Computability.Ackermann
+import Mathlib.Computability.AkraBazzi.AkraBazzi
+import Mathlib.Computability.AkraBazzi.GrowsPolynomially
 import Mathlib.Computability.ContextFreeGrammar
 import Mathlib.Computability.DFA
 import Mathlib.Computability.Encoding

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -595,6 +595,11 @@ theorem tendsto_nat_floor_atTop {α : Type*} [LinearOrderedSemiring α] [FloorSe
   Nat.floor_mono.tendsto_atTop_atTop fun x => ⟨max 0 (x + 1), by simp [Nat.le_floor_iff]⟩
 #align tendsto_nat_floor_at_top tendsto_nat_floor_atTop
 
+lemma tendsto_nat_floor_mul_atTop {α : Type _} [LinearOrderedSemifield α] [FloorSemiring α]
+    [Archimedean α] (a : α) (ha : 0 < a) : Tendsto (fun (x:ℕ) => ⌊a * x⌋₊) atTop atTop :=
+  Tendsto.comp tendsto_nat_floor_atTop
+    <| Tendsto.const_mul_atTop ha tendsto_nat_cast_atTop_atTop
+
 variable {R : Type*} [TopologicalSpace R] [LinearOrderedField R] [OrderTopology R] [FloorRing R]
 
 theorem tendsto_nat_floor_mul_div_atTop {a : R} (ha : 0 ≤ a) :