Slopes of positive discretely concave sequences

The row sequences in Section 6 have decreasing consecutive increments. A nonnegative sequence cannot have a negative increment of this kind: every later increment would be at least as negative. Consequently the increments converge to a nonnegative limit, and the sequence divided by its index has the same limit.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.antitone_increments_of_discrete_concavity {u : ℕ → ℝ} (hu : ∀ (n : ℕ), u (n + 2) + u n ≤ 2 * u (n + 1)) : Antitone fun (n : ℕ) => u (n + 1) - u n

The usual second-difference inequality makes the increments decreasing.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.concave_sequence_le_affine {u : ℕ → ℝ} (hd : Antitone fun (n : ℕ) => u (n + 1) - u n) (n k : ℕ) : u (n + k) ≤ u n + ↑k * (u (n + 1) - u n)

A tangent-line upper bound for a sequence with decreasing increments.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.increment_nonneg_of_antitone {u : ℕ → ℝ} (hu : ∀ (n : ℕ), 0 ≤ u n) (hd : Antitone fun (n : ℕ) => u (n + 1) - u n) (n : ℕ) : 0 ≤ u (n + 1) - u n

Every increment of a nonnegative discretely concave sequence is nonnegative.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.monotone_of_nonneg_of_antitone_increments {u : ℕ → ℝ} (hu : ∀ (n : ℕ), 0 ≤ u n) (hd : Antitone fun (n : ℕ) => u (n + 1) - u n) : Monotone u

A nonnegative discretely concave sequence is increasing.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.tendsto_div_nat_of_tendsto_increments {u : ℕ → ℝ} {g : ℝ} (hd : Filter.Tendsto (fun (n : ℕ) => u (n + 1) - u n) Filter.atTop (nhds g)) : Filter.Tendsto (fun (n : ℕ) => u n / ↑n) Filter.atTop (nhds g)

Telescoping and Cesàro convergence identify the linear growth rate.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_nonneg_limit_of_antitone_increments {u : ℕ → ℝ} (hu : ∀ (n : ℕ), 0 ≤ u n) (hd : Antitone fun (n : ℕ) => u (n + 1) - u n) : ∃ (g : ℝ), 0 ≤ g ∧ Filter.Tendsto (fun (n : ℕ) => u (n + 1) - u n) Filter.atTop (nhds g) ∧ Filter.Tendsto (fun (n : ℕ) => u n / ↑n) Filter.atTop (nhds g)

The limiting increment of a nonnegative discretely concave sequence is nonnegative, and it is also its linear growth rate.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exists_concave_slope_limit {P : ℕ → ℝ} (hP : ∀ (n : ℕ), 0 < P (n + 1)) (hd : Antitone fun (n : ℕ) => P (n + 2) - P (n + 1)) : ∃ (g : ℝ), 0 ≤ g ∧ (∀ (n : ℕ), g ≤ P (n + 2) - P (n + 1)) ∧ Filter.Tendsto (fun (n : ℕ) => P (n + 2) - P (n + 1)) Filter.atTop (nhds g) ∧ Filter.Tendsto (fun (n : ℕ) => P n / ↑n) Filter.atTop (nhds g)

Positive-index version, suitable for the rows in Section 6. The value at index zero is irrelevant.