Polynomial tensor restrictions and exact coefficient extraction.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.tendsto_affine_mul_geometric_zero (D C : ℝ) {q : ℝ} (hq : 0 ≤ q) (hq_one : q < 1) : Filter.Tendsto (fun (n : ℕ) => (D * ↑n + C) * q ^ n) Filter.atTop (nhds 0)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.eventually_affine_mul_pow_le_pow (D C : ℝ) {r s : ℝ} (hr : 0 ≤ r) (hrs : r < s) : ∀ᶠ (n : ℕ) in Filter.atTop, (D * ↑n + C) * r ^ n ≤ s ^ n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.eventually_affine_mul_pow_le_add_pow (D C : ℝ) {r ε : ℝ} (hr : 0 ≤ r) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, (D * ↑n + C) * r ^ n ≤ (r + ε) ^ n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.power_le_of_eventually_pow_le_affine_mul_pow {a r D C : ℝ} (hr : 0 ≤ r) (h : ∀ᶠ (n : ℕ) in Filter.atTop, a ^ n ≤ (D * ↑n + C) * r ^ n) : a ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.power_le_of_forall_pow_le_affine_mul_pow {a r D C : ℝ} (hr : 0 ≤ r) (h : ∀ (n : ℕ), 0 < n → a ^ n ≤ (D * ↑n + C) * r ^ n) : a ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.power_le_of_forall_pow_le_mul_pow {a r C : ℝ} (hr : 0 ≤ r) (h : ∀ (n : ℕ), 0 < n → a ^ n ≤ C * r ^ n) : a ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.power_le_of_forall_pow_le_linear_mul_pow (D : ℕ) {a r : ℝ} (hr : 0 ≤ r) (h : ∀ (n : ℕ), 0 < n → a ^ n ≤ ↑(D * n + 1) * r ^ n) : a ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.eventually_linear_mul_pow_le_add_pow (D : ℕ) {r ε : ℝ} (hr : 0 ≤ r) (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(D * n + 1) * r ^ n ≤ (r + ε) ^ n