BoundaryTelescoping.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The cancellation of boundary losses along an eligible path in §11.

theorem OAI.LipschitzHilbert.sum_range_shift_difference line 12

Source documentation

Shifting a finite difference sum leaves only its two boundary blocks.

theorem sum_range_shift_difference (a : ℕ → ℝ) (k r : ℕ) :
    (∑ i ∈ Finset.range k, (a i - a (i + r))) =
      (∑ i ∈ Finset.range r, a i) - ∑ i ∈ Finset.range r, a (i + k) := by
…

theorem OAI.LipschitzHilbert.boundary_loss_sum_le line 34

Source documentation

The number of path levels does not enter the boundary-loss estimate. Here r is the shift coming from the ratio of two angular radii.

theorem boundary_loss_sum_le (a loss : ℕ → ℝ) (k r : ℕ) {B : ℝ}
    (ha : ∀ i, 0 ≤ a i) (hbound : ∀ i < r, a i ≤ B)
    (hloss : ∀ i < k, loss i ≤ a i - a (i + r)) :
    (∑ i ∈ Finset.range k, loss i) ≤ (r : ℝ) * B := by
…