ConcaveSlopes.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.antitone_increments_of_discrete_concavity line 22
Source documentation
The usual second-difference inequality makes the increments decreasing.
```
theorem 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) := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.concave_sequence_le_affine line 32

Source documentation

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

theorem 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) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.increment_nonneg_of_antitone line 46
Source documentation
Every increment of a nonnegative discretely concave sequence is nonnegative.
```
theorem 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 := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.monotone_of_nonneg_of_antitone_increments line 59
Source documentation
A nonnegative discretely concave sequence is increasing.
```
theorem monotone_of_nonneg_of_antitone_increments {u : ℕ → ℝ}
    (hu : ∀ n, 0 ≤ u n) (hd : Antitone (fun n => u (n + 1) - u n)) :
    Monotone u := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.tendsto_div_nat_of_tendsto_increments line 68

Source documentation

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

theorem tendsto_div_nat_of_tendsto_increments {u : ℕ → ℝ} {g : ℝ}
    (hd : Tendsto (fun n => u (n + 1) - u n) atTop (𝓝 g)) :
    Tendsto (fun n => u n / (n : ℝ)) atTop (𝓝 g) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nonneg_limit_of_antitone_increments line 79

Source documentation

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

theorem exists_nonneg_limit_of_antitone_increments {u : ℕ → ℝ}
    (hu : ∀ n, 0 ≤ u n) (hd : Antitone (fun n => u (n + 1) - u n)) :
    ∃ g : ℝ, 0 ≤ g ∧
      Tendsto (fun n => u (n + 1) - u n) atTop (𝓝 g) ∧
      Tendsto (fun n => u n / (n : ℝ)) atTop (𝓝 g) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_concave_slope_limit line 96

Source documentation

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

theorem 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)) ∧
      Tendsto (fun n => P (n + 2) - P (n + 1)) atTop (𝓝 g) ∧
      Tendsto (fun n => P n / (n : ℝ)) atTop (𝓝 g) := by
…