Theory Abstract_Descent

theory Abstract_Descent
  imports "HOL-Analysis.Analysis"
begin

section ‹Abstract descent and telescoping lemmas›

text ‹
This theory contains abstract sequence and finite-sum lemmas used in descent
analyses.  These results are independent of gradients, projections, and
particular optimization algorithms.
›

subsection ‹Finite-sum telescoping›

text ‹
If each local progress term is bounded by the decrease of a potential, then
the sum of all progress terms is bounded by the total decrease of the
potential.
›

lemma sum_progress_le_initial_gap:
  fixes a c :: "nat ⇒ real"
  assumes step: "⋀n. n < N ⟹ c n ≤ a n - a (Suc n)"
  shows "sum c {..<N} ≤ a 0 - a N"
  using step
proof (induction N)
  case 0
  show ?case by simp
next
  case (Suc N)
  have IH: "sum c {..<N} ≤ a 0 - a N"
  proof (rule Suc.IH)
    fix n
    assume n_lt: "n < N"
    then show "c n ≤ a n - a (Suc n)"
      using Suc.prems by simp
  qed

  have last: "c N ≤ a N - a (Suc N)"
    using Suc.prems by simp

  have "sum c {..<Suc N} = sum c {..<N} + c N"
    by simp
  also have "... ≤ (a 0 - a N) + (a N - a (Suc N))"
    using IH last by linarith
  also have "... = a 0 - a (Suc N)"
    by simp
  finally show ?case .
qed

text ‹
A version in which the terminal value of the potential is replaced by a lower
bound.
›

lemma sum_progress_le_initial_minus_lower_bound:
  fixes a c :: "nat ⇒ real"
  assumes step: "⋀n. n < N ⟹ c n ≤ a n - a (Suc n)"
  assumes lower: "B ≤ a N"
  shows "sum c {..<N} ≤ a 0 - B"
proof -
  have "sum c {..<N} ≤ a 0 - a N"
    using step by (rule sum_progress_le_initial_gap)
  also have "... ≤ a 0 - B"
    using lower by linarith
  finally show ?thesis .
qed

subsection ‹Average bounds›

text ‹
If a finite sum is bounded above, then at least one term is bounded by the
corresponding average.
›

lemma exists_le_average_of_sum_bound:
  fixes a :: "nat ⇒ real"
  assumes N_pos: "N > 0"
  assumes nonneg: "⋀n. n < N ⟹ 0 ≤ a n"
  assumes sum_bound: "sum a {..<N} ≤ B"
  shows "∃n<N. a n ≤ B / real N"
proof (rule ccontr)
  assume not_exists: "¬ (∃n<N. a n ≤ B / real N)"

  have gt: "⋀n. n < N ⟹ B / real N < a n"
  proof -
    fix n
    assume n_lt: "n < N"
    have "¬ a n ≤ B / real N"
      using not_exists n_lt by auto
    then show "B / real N < a n"
      by simp
  qed

  have const_sum: "sum (λn. B / real N) {..<N} = B"
    using N_pos by simp

  have strict_sum: "sum (λn. B / real N) {..<N} < sum a {..<N}"
    using N_pos gt by (intro sum_strict_mono) auto

  have "B < sum a {..<N}"
    using const_sum strict_sum by simp
  then show False
    using sum_bound by linarith
qed

lemma exists_le_average_of_nonnegative_sum:
  fixes a :: "nat ⇒ real"
  assumes N_pos: "N > 0"
  assumes nonneg: "⋀n. n < N ⟹ 0 ≤ a n"
  shows "∃n<N. a n ≤ sum a {..<N} / real N"
proof -
  have sum_bound: "sum a {..<N} ≤ sum a {..<N}"
    by simp
  show ?thesis
    using exists_le_average_of_sum_bound[OF N_pos nonneg sum_bound] .
qed

subsection ‹Linear recurrences›

text ‹
A one-step linear recurrence can be iterated to obtain a geometric bound.
›

lemma sequence_linear_rate_from_step:
  fixes a :: "nat ⇒ real"
  assumes q_nonneg: "0 ≤ q"
  assumes step: "⋀n. a (Suc n) ≤ q * a n"
  shows "a n ≤ q ^ n * a 0"
proof (induction n)
  case 0
  show ?case by simp
next
  case (Suc n)
  have "a (Suc n) ≤ q * a n"
    by (rule step)
  also have "... ≤ q * (q ^ n * a 0)"
  proof (rule mult_left_mono)
    show "a n ≤ q ^ n * a 0"
      using Suc.IH .
    show "0 ≤ q"
      using q_nonneg .
  qed
  also have "... = q ^ Suc n * a 0"
    by (simp add: algebra_simps)
  finally show ?case .
qed

end