Floor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.tendsto_floor_mul_div line 21
Source documentation
Rounding a nonnegative linear exponent down has vanishing normalized error.
```
theorem tendsto_floor_mul_div {c : ℝ} (hc : 0 ≤ c) :
    Tendsto (fun j : ℕ => (⌊(j : ℝ) * c⌋₊ : ℝ) / (j : ℝ))
      atTop (𝓝 c) := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.tendsto_floor_mul_atTop line 29
Source documentation
A floor-rounded exponent diverges when its linear coefficient is positive.
```
theorem tendsto_floor_mul_atTop {c : ℝ} (hc : 0 < c) :
    Tendsto (fun j : ℕ => ⌊(j : ℝ) * c⌋₊) atTop atTop := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tendsto_pow_floor_rpow_inv line 34

Source documentation

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

theorem tendsto_pow_floor_rpow_inv {u c : ℝ} (hu : 0 < u) (hc : 0 ≤ c) :
    Tendsto (fun j : ℕ => (u ^ ⌊(j : ℝ) * c⌋₊) ^ (1 / (j : ℝ)))
      atTop (𝓝 (u ^ c)) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tendsto_pow_floor_logb_div_rpow_inv line 46
Source documentation
The logarithmic choice of exponent gives the prescribed root growth rate. In the tensor application, s is the exponent bound with a positive slack.
```
theorem tendsto_pow_floor_logb_div_rpow_inv {u n s : ℝ}
    (hu : 1 < u) (hn : 1 ≤ n) (hs : 0 < s) :
    Tendsto
      (fun j : ℕ => (u ^ ⌊(j : ℝ) * (Real.logb u n / s)⌋₊) ^ (1 / (j : ℝ)))
      atTop (𝓝 (n ^ (1 / s))) := by
…
```