FirstDerivativeSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.weighted_difference_sum line 9

Source documentation

A finite integration-by-parts identity with endpoint terms exposed.

theorem weighted_difference_sum (a b : ℕ → ℂ) (n : ℕ) :
    (∑ j ∈ Finset.range (n + 1), b j * (a (j + 1) - a j)) =
      b n * a (n + 1) - b 0 * a 0 -
        ∑ j ∈ Finset.range n, (b (j + 1) - b j) * a (j + 1) := by
…

theorem OAI.Problem337.real_finite_variation_le line 21

Source documentation

The total variation of a real monotone finite sequence is bounded by twice a uniform absolute-value bound.

theorem real_finite_variation_le (f : ℕ → ℝ) (n : ℕ) (B : ℝ)
    (hB : ∀ j ≤ n, |f j| ≤ B)
    (hmono : (∀ j < n, f j ≤ f (j + 1)) ∨
      (∀ j < n, f (j + 1) ≤ f j)) :
    (∑ j ∈ Finset.range n, |f (j + 1) - f j|) ≤ 2 * B := by
…

theorem OAI.Problem337.first_derivative_sum_bound line 50

Source documentation

Abel cancellation when reciprocal increments lie on a vertical line and move monotonically along it. This is the algebraic first-derivative test.

theorem first_derivative_sum_bound (a b : ℕ → ℂ) (n : ℕ) (B : ℝ)
    (ha : ∀ j ≤ n + 1, ‖a j‖ ≤ 1)
    (hb : ∀ j ≤ n, ‖b j‖ ≤ B)
    (hreal : ∀ j ≤ n, (b j).re = (b 0).re)
    (hmono : (∀ j < n, (b j).im ≤ (b (j + 1)).im) ∨
      (∀ j < n, (b (j + 1)).im ≤ (b j).im))
    (hrel : ∀ j ≤ n, b j * (a (j + 1) - a j) = a j) :
    ‖∑ j ∈ Finset.range (n + 1), a j‖ ≤ 4 * B := by
…