Theory Gradient_Descent

theory Gradient_Descent
  imports Smooth_Convex
begin

section ‹Gradient descent sequences›

text ‹
This theory lifts the one-step descent estimates from @{text ‹Smooth_Convex›} to
gradient descent sequences.

The purpose of this file is deliberately modest: it packages the recurrence

  x (Suc n) = @{text ‹gradient_step›} alpha G (x n)

and proves the basic monotonicity consequences that follow from the smooth
upper-bound interface.
›


subsection ‹Gradient descent recurrence›

definition gradient_descent_iterates ::
  "real ⇒ ('a::real_vector ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ bool"
where
  "gradient_descent_iterates alpha G x ⟷
     (∀n. x (Suc n) = gradient_step alpha G (x n))"

lemma gradient_descent_iteratesI:
  assumes "⋀n. x (Suc n) = gradient_step alpha G (x n)"
  shows "gradient_descent_iterates alpha G x"
  using assms
  unfolding gradient_descent_iterates_def
  by auto

lemma gradient_descent_iteratesD:
  assumes "gradient_descent_iterates alpha G x"
  shows "x (Suc n) = gradient_step alpha G (x n)"
  using assms
  unfolding gradient_descent_iterates_def
  by auto

lemma gradient_descent_iteratesE:
  assumes "gradient_descent_iterates alpha G x"
  obtains "x (Suc n) = gradient_step alpha G (x n)"
  using gradient_descent_iteratesD[OF assms, of n]
  by auto


subsection ‹Feasible iterates›

definition feasible_iterates ::
  "'a set ⇒ (nat ⇒ 'a) ⇒ bool"
where
  "feasible_iterates S x ⟷ (∀n. x n ∈ S)"

lemma feasible_iteratesI:
  assumes "⋀n. x n ∈ S"
  shows "feasible_iterates S x"
  using assms
  unfolding feasible_iterates_def
  by auto

lemma feasible_iteratesD:
  assumes "feasible_iterates S x"
  shows "x n ∈ S"
  using assms
  unfolding feasible_iterates_def
  by auto

lemma feasible_iterates_subset:
  assumes "feasible_iterates S x"
    and "S ⊆ T"
  shows "feasible_iterates T x"
proof (rule feasible_iteratesI)
  fix n
  have "x n ∈ S"
    using assms(1)
    by (rule feasible_iteratesD)
  then show "x n ∈ T"
    using assms(2)
    by auto
qed

lemma gradient_descent_step_mem:
  assumes gd: "gradient_descent_iterates alpha G x"
    and feasible: "feasible_iterates S x"
  shows "gradient_step alpha G (x n) ∈ S"
proof -
  have next_mem: "x (Suc n) ∈ S"
    using feasible
    by (rule feasible_iteratesD)

  have step_eq: "x (Suc n) = gradient_step alpha G (x n)"
    using gd
    by (rule gradient_descent_iteratesD)

  show ?thesis
    using next_mem step_eq
    by simp
qed


subsection ‹Objective value sequences›

definition objective_values ::
  "('a ⇒ real) ⇒ (nat ⇒ 'a) ⇒ nat ⇒ real"
where
  "objective_values f x n = f (x n)"

lemma objective_values_simp [simp]:
  "objective_values f x n = f (x n)"
  unfolding objective_values_def
  by simp

definition nonincreasing_sequence ::
  "(nat ⇒ real) ⇒ bool"
where
  "nonincreasing_sequence a ⟷ (∀n. a (Suc n) ≤ a n)"

lemma nonincreasing_sequenceI:
  assumes "⋀n. a (Suc n) ≤ a n"
  shows "nonincreasing_sequence a"
  using assms
  unfolding nonincreasing_sequence_def
  by auto

lemma nonincreasing_sequenceD:
  assumes "nonincreasing_sequence a"
  shows "a (Suc n) ≤ a n"
  using assms
  unfolding nonincreasing_sequence_def
  by auto


subsection ‹One-step estimates along gradient descent iterates›

lemma gradient_descent_one_step_bound:
  assumes smooth: "smooth_upper_bound_on L S f G"
    and gd: "gradient_descent_iterates alpha G x"
    and feasible: "feasible_iterates S x"
  shows
    "f (x (Suc n))
      ≤ f (x n) - alpha * norm (G (x n)) ^ 2
          + (L / 2) * alpha ^ 2 * norm (G (x n)) ^ 2"
proof -
  have xn_mem: "x n ∈ S"
    using feasible
    by (rule feasible_iteratesD)

  have step_mem: "gradient_step alpha G (x n) ∈ S"
    using gd feasible
    by (rule gradient_descent_step_mem)

  have step_eq: "x (Suc n) = gradient_step alpha G (x n)"
    using gd
    by (rule gradient_descent_iteratesD)

  have bound:
    "f (gradient_step alpha G (x n))
      ≤ f (x n) - alpha * norm (G (x n)) ^ 2
          + (L / 2) * alpha ^ 2 * norm (G (x n)) ^ 2"
    using smooth_upper_bound_gradient_step[OF smooth xn_mem step_mem] .

  show ?thesis
    using bound step_eq
    by simp
qed

lemma gradient_descent_one_step_decrease:
  assumes smooth: "smooth_upper_bound_on L S f G"
    and gd: "gradient_descent_iterates alpha G x"
    and feasible: "feasible_iterates S x"
    and alpha_nonneg: "0 ≤ alpha"
    and step_size: "alpha * L ≤ 1"
  shows
    "f (x (Suc n))
      ≤ f (x n) - (alpha / 2) * norm (G (x n)) ^ 2"
proof -
  have xn_mem: "x n ∈ S"
    using feasible
    by (rule feasible_iteratesD)

  have step_mem: "gradient_step alpha G (x n) ∈ S"
    using gd feasible
    by (rule gradient_descent_step_mem)

  have step_eq: "x (Suc n) = gradient_step alpha G (x n)"
    using gd
    by (rule gradient_descent_iteratesD)

  have decrease:
    "f (gradient_step alpha G (x n))
      ≤ f (x n) - (alpha / 2) * norm (G (x n)) ^ 2"
    using smooth_upper_bound_gradient_step_decrease[
      OF smooth xn_mem step_mem alpha_nonneg step_size] .

  show ?thesis
    using decrease step_eq
    by simp
qed

lemma gradient_descent_objective_mono_step:
  assumes smooth: "smooth_upper_bound_on L S f G"
    and gd: "gradient_descent_iterates alpha G x"
    and feasible: "feasible_iterates S x"
    and alpha_nonneg: "0 ≤ alpha"
    and step_size: "alpha * L ≤ 1"
  shows "f (x (Suc n)) ≤ f (x n)"
proof -
  have decrease:
    "f (x (Suc n))
      ≤ f (x n) - (alpha / 2) * norm (G (x n)) ^ 2"
    using gradient_descent_one_step_decrease[
      OF smooth gd feasible alpha_nonneg step_size] .

  have nonneg:
    "0 ≤ (alpha / 2) * norm (G (x n)) ^ 2"
  proof -
    have "0 ≤ alpha / 2"
      using alpha_nonneg
      by simp

    moreover have "0 ≤ norm (G (x n)) ^ 2"
      by simp

    ultimately show ?thesis
      by (rule mult_nonneg_nonneg)
  qed

  show ?thesis
    using decrease nonneg
    by linarith
qed

lemma gradient_descent_objective_nonincreasing:
  assumes smooth: "smooth_upper_bound_on L S f G"
    and gd: "gradient_descent_iterates alpha G x"
    and feasible: "feasible_iterates S x"
    and alpha_nonneg: "0 ≤ alpha"
    and step_size: "alpha * L ≤ 1"
  shows "nonincreasing_sequence (objective_values f x)"
proof (rule nonincreasing_sequenceI)
  fix n
  show "objective_values f x (Suc n) ≤ objective_values f x n"
    using gradient_descent_objective_mono_step[
      OF smooth gd feasible alpha_nonneg step_size, of n]
    by simp
qed

lemma gradient_descent_step_progress:
  assumes smooth: "smooth_upper_bound_on L S f G"
    and gd: "gradient_descent_iterates alpha G x"
    and feasible: "feasible_iterates S x"
    and alpha_nonneg: "0 ≤ alpha"
    and step_size: "alpha * L ≤ 1"
  shows
    "(alpha / 2) * norm (G (x n)) ^ 2
      ≤ f (x n) - f (x (Suc n))"
proof -
  have decrease:
    "f (x (Suc n))
      ≤ f (x n) - (alpha / 2) * norm (G (x n)) ^ 2"
    using gradient_descent_one_step_decrease[
      OF smooth gd feasible alpha_nonneg step_size] .

  show ?thesis
    using decrease
    by linarith
qed


subsection ‹Locale form›

locale gradient_descent =
  smooth_convex S f G L
  for S :: "'a::real_inner set"
    and f :: "'a ⇒ real"
    and G :: "'a ⇒ 'a"
    and L :: real +
  fixes alpha :: real
    and x :: "nat ⇒ 'a"
  assumes iterates: "gradient_descent_iterates alpha G x"
    and feasible: "feasible_iterates S x"
    and alpha_nonneg: "0 ≤ alpha"
    and step_size: "alpha * L ≤ 1"
begin

lemma iterate:
  "x (Suc n) = gradient_step alpha G (x n)"
  using iterates
  by (rule gradient_descent_iteratesD)

lemma iterate_mem:
  "x n ∈ S"
  using feasible
  by (rule feasible_iteratesD)

lemma step_mem:
  "gradient_step alpha G (x n) ∈ S"
  using iterates feasible
  by (rule gradient_descent_step_mem)

lemma one_step_bound:
  "f (x (Suc n))
    ≤ f (x n) - alpha * norm (G (x n)) ^ 2
        + (L / 2) * alpha ^ 2 * norm (G (x n)) ^ 2"
  using gradient_descent_one_step_bound[OF smooth_bound iterates feasible] .

lemma one_step_decrease:
  "f (x (Suc n))
    ≤ f (x n) - (alpha / 2) * norm (G (x n)) ^ 2"
  using gradient_descent_one_step_decrease[
    OF smooth_bound iterates feasible alpha_nonneg step_size] .

lemma objective_mono_step:
  "f (x (Suc n)) ≤ f (x n)"
  using gradient_descent_objective_mono_step[
    OF smooth_bound iterates feasible alpha_nonneg step_size] .

lemma objective_nonincreasing:
  "nonincreasing_sequence (objective_values f x)"
  using gradient_descent_objective_nonincreasing[
    OF smooth_bound iterates feasible alpha_nonneg step_size] .

lemma step_progress:
  "(alpha / 2) * norm (G (x n)) ^ 2
    ≤ f (x n) - f (x (Suc n))"
  using gradient_descent_step_progress[
    OF smooth_bound iterates feasible alpha_nonneg step_size] .

end

text ‹
This file turns the pointwise gradient-step descent estimates into sequence
statements for gradient descent.

The main consequence is that, under the smooth upper-bound assumption and the
standard step-size condition that alpha * L is at most one, the objective values along a
feasible gradient descent sequence form a nonincreasing sequence.
›

end