Growth rates of floor-rounded exponents

The integer exponents obtained by rounding a nonnegative multiple of the tensor power have the intended normalized growth rate. Applying a positive base to these exponents preserves that rate after taking roots.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tendsto_floor_mul_div {c : ℝ} (hc : 0 ≤ c) : Filter.Tendsto (fun (j : ℕ) => ↑⌊↑j * c⌋₊ / ↑j) Filter.atTop (nhds c)

Rounding a nonnegative linear exponent down has vanishing normalized error.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tendsto_floor_mul_atTop {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (j : ℕ) => ⌊↑j * c⌋₊) Filter.atTop Filter.atTop

A floor-rounded exponent diverges when its linear coefficient is positive.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tendsto_pow_floor_rpow_inv {u c : ℝ} (hu : 0 < u) (hc : 0 ≤ c) : Filter.Tendsto (fun (j : ℕ) => (u ^ ⌊↑j * c⌋₊) ^ (1 / ↑j)) Filter.atTop (nhds (u ^ c))

The root growth rate of powers with floor-rounded exponents.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tendsto_pow_floor_logb_div_rpow_inv {u n s : ℝ} (hu : 1 < u) (hn : 1 ≤ n) (hs : 0 < s) : Filter.Tendsto (fun (j : ℕ) => (u ^ ⌊↑j * (Real.logb u n / s)⌋₊) ^ (1 / ↑j)) Filter.atTop (nhds (n ^ (1 / s)))

The logarithmic choice of exponent gives the prescribed root growth rate. In the tensor application, s is the exponent bound with a positive slack.