Finite entropy, rate estimates and ordered asymptotic limits.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.affine_recurrence_shifted (x : ℕ → ℝ) (a c : ℝ) (ha : 0 ≤ a) (hstep : ∀ (t : ℕ), x (t + 1) ≤ a * x t + (a - 1) * c) (t : ℕ) : x t + c ≤ a ^ t * (x 0 + c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.affine_recurrence_bound (x : ℕ → ℝ) (a b : ℝ) (ha : 1 < a) (hb : 0 ≤ b) (hstep : ∀ (t : ℕ), x (t + 1) ≤ a * x t + b) (t : ℕ) : x t ≤ a ^ t * (x 0 + b / (a - 1))