Theory Convex_Differentiable

theory Convex_Differentiable
  imports Gradient_Preliminaries
begin

section ‹Convex differentiable functions and first-order certificates›

text ‹
This theory introduces the first-order certificate language used later for
gradient descent and projected gradient descent.

The file isolates four basic notions:

  • global minimizers on a feasible set;
  • first-order variational inequalities;
  • supporting affine lower bounds;
  • convex differentiable functions with a named gradient field.

The main result is the standard first-order supporting-hyperplane property:
if f is convex and has gradient g at x, then

  the affine first-order lower bound at x is below f y

for every feasible y.

Consequently, every convex differentiable function with a named gradient field
satisfies a global gradient lower-bound property.  Combined with the
variational first-order condition, this gives a global optimality certificate.
›


subsection ‹Global minimizers›

definition global_min_on ::
  "'a set ⇒ ('a ⇒ real) ⇒ 'a ⇒ bool"
where
  "global_min_on S f x ⟷ x ∈ S ∧ (∀y∈S. f x ≤ f y)"

lemma global_min_onI:
  assumes "x ∈ S"
    and "⋀y. y ∈ S ⟹ f x ≤ f y"
  shows "global_min_on S f x"
  using assms
  unfolding global_min_on_def
  by auto

lemma global_min_onD_mem:
  assumes "global_min_on S f x"
  shows "x ∈ S"
  using assms
  unfolding global_min_on_def
  by auto

lemma global_min_onD:
  assumes "global_min_on S f x"
    and "y ∈ S"
  shows "f x ≤ f y"
  using assms
  unfolding global_min_on_def
  by auto

lemma global_min_on_singleton [simp]:
  "global_min_on {x} f x"
  unfolding global_min_on_def
  by simp

lemma global_min_on_UNIV_iff:
  "global_min_on UNIV f x ⟷ (∀y. f x ≤ f y)"
  unfolding global_min_on_def
  by simp


subsection ‹First-order variational inequalities›

text ‹
For constrained convex minimization, the first-order condition at x with
gradient g is

  the directional inner product inner g (y - x) is nonnegative

for every feasible y.

This is the variational-inequality form of first-order optimality.
›

definition first_order_condition_at ::
  "'a::real_inner set ⇒ 'a ⇒ 'a ⇒ bool"
where
  "first_order_condition_at S g x ⟷
     x ∈ S ∧ (∀y∈S. 0 ≤ inner g (y - x))"

lemma first_order_condition_atI:
  assumes "x ∈ S"
    and "⋀y. y ∈ S ⟹ 0 ≤ inner g (y - x)"
  shows "first_order_condition_at S g x"
  using assms
  unfolding first_order_condition_at_def
  by auto

lemma first_order_condition_atD_mem:
  assumes "first_order_condition_at S g x"
  shows "x ∈ S"
  using assms
  unfolding first_order_condition_at_def
  by auto

lemma first_order_condition_atD:
  assumes "first_order_condition_at S g x"
    and "y ∈ S"
  shows "0 ≤ inner g (y - x)"
  using assms
  unfolding first_order_condition_at_def
  by auto

lemma first_order_condition_zero_iff_mem [simp]:
  "first_order_condition_at S 0 x ⟷ x ∈ S"
  unfolding first_order_condition_at_def
  by simp


subsection ‹Supporting affine lower bounds›

text ‹
A vector g supports f at x on S if the corresponding affine first-order
approximation is a global lower bound for f on S.

For differentiable convex functions, g will later be the gradient at x.
›

definition supports_at ::
  "'a::real_inner set ⇒ ('a ⇒ real) ⇒ 'a ⇒ 'a ⇒ bool"
where
  "supports_at S f x g ⟷
     x ∈ S ∧ (∀y∈S. f x + inner g (y - x) ≤ f y)"

definition supports_on ::
  "'a::real_inner set ⇒ ('a ⇒ real) ⇒ ('a ⇒ 'a) ⇒ bool"
where
  "supports_on S f G ⟷ (∀x∈S. supports_at S f x (G x))"

lemma supports_atI:
  assumes "x ∈ S"
    and "⋀y. y ∈ S ⟹ f x + inner g (y - x) ≤ f y"
  shows "supports_at S f x g"
  using assms
  unfolding supports_at_def
  by auto

lemma supports_atD_mem:
  assumes "supports_at S f x g"
  shows "x ∈ S"
  using assms
  unfolding supports_at_def
  by auto

lemma supports_atD:
  assumes "supports_at S f x g"
    and "y ∈ S"
  shows "f x + inner g (y - x) ≤ f y"
  using assms
  unfolding supports_at_def
  by auto

lemma supports_onI:
  assumes "⋀x. x ∈ S ⟹ supports_at S f x (G x)"
  shows "supports_on S f G"
  using assms
  unfolding supports_on_def
  by auto

lemma supports_onD:
  assumes "supports_on S f G"
    and "x ∈ S"
  shows "supports_at S f x (G x)"
  using assms
  unfolding supports_on_def
  by auto

lemma supports_at_zero_iff_global_min_on:
  "supports_at S f x 0 ⟷ global_min_on S f x"
  unfolding supports_at_def global_min_on_def
  by simp

lemma supports_at_zero_imp_global_min_on:
  assumes "supports_at S f x 0"
  shows "global_min_on S f x"
  using assms
  by (simp add: supports_at_zero_iff_global_min_on)

lemma global_min_on_imp_supports_at_zero:
  assumes "global_min_on S f x"
  shows "supports_at S f x 0"
  using assms
  by (simp add: supports_at_zero_iff_global_min_on)

lemma supports_at_and_first_order_condition_imp_global_min_on:
  assumes supp: "supports_at S f x g"
    and foc: "first_order_condition_at S g x"
  shows "global_min_on S f x"
proof (rule global_min_onI)
  show "x ∈ S"
    using supp
    by (rule supports_atD_mem)
next
  fix y
  assume y: "y ∈ S"

  have "f x ≤ f x + inner g (y - x)"
    using first_order_condition_atD[OF foc y]
    by simp
  also have "... ≤ f y"
    using supports_atD[OF supp y] .
  finally show "f x ≤ f y" .
qed

lemma supports_at_gradient_and_foc_imp_global_min_on:
  assumes supp: "supports_at S f x (gradient f x)"
    and foc: "first_order_condition_at S (gradient f x) x"
  shows "global_min_on S f x"
  using supports_at_and_first_order_condition_imp_global_min_on[OF supp foc] .


subsection ‹Gradient lower-bound fields›

text ‹
This is the pointwise supporting-hyperplane property written with a named
gradient field G.

Later, for convex differentiable functions, we will prove this property from
convexity and differentiability.
›

definition gradient_lower_bound_on ::
  "'a::real_inner set ⇒ ('a ⇒ real) ⇒ ('a ⇒ 'a) ⇒ bool"
where
  "gradient_lower_bound_on S f G ⟷
     (∀x∈S. ∀y∈S. f x + inner (G x) (y - x) ≤ f y)"

lemma gradient_lower_bound_onI:
  assumes "⋀x y. x ∈ S ⟹ y ∈ S ⟹ f x + inner (G x) (y - x) ≤ f y"
  shows "gradient_lower_bound_on S f G"
  using assms
  unfolding gradient_lower_bound_on_def
  by auto

lemma gradient_lower_bound_onD:
  assumes "gradient_lower_bound_on S f G"
    and "x ∈ S"
    and "y ∈ S"
  shows "f x + inner (G x) (y - x) ≤ f y"
  using assms
  unfolding gradient_lower_bound_on_def
  by auto

lemma gradient_lower_bound_on_imp_supports_on:
  assumes "gradient_lower_bound_on S f G"
  shows "supports_on S f G"
proof (rule supports_onI)
  fix x
  assume x: "x ∈ S"
  show "supports_at S f x (G x)"
  proof (rule supports_atI)
    show "x ∈ S"
      using x .
  next
    fix y
    assume y: "y ∈ S"
    show "f x + inner (G x) (y - x) ≤ f y"
      using gradient_lower_bound_onD[OF assms x y] .
  qed
qed

lemma gradient_lower_bound_on_and_foc_imp_global_min_on:
  assumes lb: "gradient_lower_bound_on S f G"
    and foc: "first_order_condition_at S (G x) x"
  shows "global_min_on S f x"
proof -
  have x: "x ∈ S"
    using foc
    by (rule first_order_condition_atD_mem)

  have supp: "supports_at S f x (G x)"
    using gradient_lower_bound_on_imp_supports_on[OF lb] x
    by (rule supports_onD)

  show ?thesis
    using supports_at_and_first_order_condition_imp_global_min_on[OF supp foc] .
qed


subsection ‹Convexity along feasible segments›

text ‹
The next lemmas convert the standard convex-combination statement into the
optimization form x + t * (y - x).
›

lemma convex_contains_affine_line:
  fixes x y :: "'a::real_vector"
  assumes "convex S"
    and "x ∈ S"
    and "y ∈ S"
    and "0 ≤ t"
    and "t ≤ 1"
  shows "x + scaleR t (y - x) ∈ S"
proof -
  have combo: "scaleR (1 - t) x + scaleR t y ∈ S"
    using convexD_alt[OF assms(1) assms(2) assms(3) assms(4) assms(5)] .

  have eq: "x + scaleR t (y - x) = scaleR (1 - t) x + scaleR t y"
    by (simp add: algebra_simps)

  show ?thesis
    using combo
    by (simp only: eq)
qed

lemma convex_on_affine_lineD:
  fixes x y :: "'a::real_vector"
  assumes "convex_on S f"
    and "x ∈ S"
    and "y ∈ S"
    and "0 ≤ t"
    and "t ≤ 1"
  shows "f (x + scaleR t (y - x)) ≤ (1 - t) * f x + t * f y"
proof -
  have bound:
    "f (scaleR (1 - t) x + scaleR t y) ≤ (1 - t) * f x + t * f y"
    using convex_onD[OF assms(1) assms(4) assms(5) assms(2) assms(3)] .

  have eq: "x + scaleR t (y - x) = scaleR (1 - t) x + scaleR t y"
    by (simp add: algebra_simps)

  show ?thesis
    using bound
    by (simp only: eq)
qed

lemma convex_on_affine_lineD_open01:
  fixes x y :: "'a::real_vector"
  assumes "convex_on S f"
    and "x ∈ S"
    and "y ∈ S"
    and "0 < t"
    and "t < 1"
  shows "f (x + scaleR t (y - x)) ≤ (1 - t) * f x + t * f y"
  using convex_on_affine_lineD[OF assms(1) assms(2) assms(3)]
  using assms(4) assms(5)
  by simp

subsection ‹First-order lower bound for convex differentiable functions›

lemma convex_line_secant_slope_bound:
  fixes f :: "'a::real_inner ⇒ real"
  assumes conv: "convex_on S f"
    and x: "x ∈ S"
    and y: "y ∈ S"
    and tpos: "0 < t"
    and tle: "t ≤ 1"
  shows "(f (x + t *⇩R (y - x)) - f x) / t ≤ f y - f x"
proof -
  have bound:
    "f (x + t *⇩R (y - x)) ≤ (1 - t) * f x + t * f y"
    using convex_on_affine_lineD[OF conv x y] tpos tle
    by simp

  have "f (x + t *⇩R (y - x)) - f x ≤ t * (f y - f x)"
    using bound
    by (simp add: algebra_simps)

  then show ?thesis
    using tpos
    by (simp add: field_simps)
qed

lemma has_gradient_line_slope_tendsto:
  fixes f :: "'a::real_inner ⇒ real"
  assumes grad: "has_gradient f x g"
  shows "((λt::real. (f (x + t *⇩R d) - f x) / t) ⤏ inner d g) (at_right 0)"
proof -
  have D:
    "((λt::real. f (x + t *⇩R d)) has_field_derivative inner d g) (at 0)"
    using has_gradient_restrict_to_line_at_0[OF grad, of d] .

  have D_right:
    "((λt::real. f (x + t *⇩R d)) has_field_derivative inner d g)
       (at (0::real) within {0<..})"
    using D
    unfolding has_field_derivative_def
    by (rule has_derivative_at_withinI)

  show ?thesis
    using D_right
    unfolding has_field_derivative_iff
    by simp
qed

lemma convex_has_gradient_supports:
  fixes f :: "'a::real_inner ⇒ real"
  assumes conv: "convex_on S f"
    and grad: "has_gradient f x g"
    and x: "x ∈ S"
    and y: "y ∈ S"
  shows "f x + inner g (y - x) ≤ f y"
proof -
  define d where "d = y - x"

  have lim:
    "((λt::real. (f (x + t *⇩R d) - f x) / t) ⤏ inner d g) (at_right 0)"
    using has_gradient_line_slope_tendsto[OF grad, of d] .

  have ev01:
    "eventually (λt::real. t ∈ {0<..<1}) (at_right 0)"
    using eventually_at_right_real[OF zero_less_one] .

  have ev:
    "eventually
      (λt::real. (f (x + t *⇩R d) - f x) / t ≤ f y - f x)
      (at_right 0)"
    using ev01
  proof eventually_elim
    fix t :: real
    assume t: "t ∈ {0<..<1}"
    then have tpos: "0 < t"
      by auto
    from t have tle: "t ≤ 1"
      by auto

    show "(f (x + t *⇩R d) - f x) / t ≤ f y - f x"
      unfolding d_def
      using convex_line_secant_slope_bound[OF conv x y tpos tle] .
  qed

  have nontriv: "¬ trivial_limit (at_right (0::real))"
    by simp

  have "f y - f x ≥ inner d g"
    using tendsto_upperbound[OF lim ev nontriv] .

  then show ?thesis
    unfolding d_def
    by (simp add: inner_commute algebra_simps)
qed

subsection ‹Convex differentiable functions with a named gradient field›

definition convex_differentiable_on ::
  "'a::real_inner set ⇒ ('a ⇒ real) ⇒ ('a ⇒ 'a) ⇒ bool"
where
  "convex_differentiable_on S f G ⟷
     convex_on S f ∧ has_gradient_on f S G"

lemma convex_differentiable_onI:
  assumes "convex_on S f"
    and "has_gradient_on f S G"
  shows "convex_differentiable_on S f G"
  using assms
  unfolding convex_differentiable_on_def
  by auto

lemma convex_differentiable_onD_convex_on:
  assumes "convex_differentiable_on S f G"
  shows "convex_on S f"
  using assms
  unfolding convex_differentiable_on_def
  by auto

lemma convex_differentiable_onD_has_gradient_on:
  assumes "convex_differentiable_on S f G"
  shows "has_gradient_on f S G"
  using assms
  unfolding convex_differentiable_on_def
  by auto

lemma convex_differentiable_on_convex:
  assumes "convex_differentiable_on S f G"
  shows "convex S"
  using assms convex_on_imp_convex
  unfolding convex_differentiable_on_def
  by blast

lemma convex_differentiable_on_gradientD:
  assumes "convex_differentiable_on S f G"
    and "x ∈ S"
  shows "has_gradient f x (G x)"
  using convex_differentiable_onD_has_gradient_on[OF assms(1)] assms(2)
  by (rule has_gradient_onD)

lemma convex_differentiable_on_differentiable:
  assumes "convex_differentiable_on S f G"
    and "x ∈ S"
  shows "f differentiable (at x)"
  using convex_differentiable_on_gradientD[OF assms]
  by (rule has_gradient_imp_differentiable)

lemma has_gradient_on_subset:
  assumes "has_gradient_on f T G"
    and "S ⊆ T"
  shows "has_gradient_on f S G"
  using assms
  unfolding has_gradient_on_def
  by auto

lemma convex_differentiable_on_subset:
  assumes "convex_differentiable_on T f G"
    and "S ⊆ T"
    and "convex S"
  shows "convex_differentiable_on S f G"
proof (rule convex_differentiable_onI)
  show "convex_on S f"
    using convex_differentiable_onD_convex_on[OF assms(1)] assms(2) assms(3)
    by (rule convex_on_subset)

  show "has_gradient_on f S G"
    using convex_differentiable_onD_has_gradient_on[OF assms(1)] assms(2)
    by (rule has_gradient_on_subset)
qed

lemma convex_differentiable_on_imp_gradient_lower_bound_on:
  assumes cd: "convex_differentiable_on S f G"
  shows "gradient_lower_bound_on S f G"
proof (rule gradient_lower_bound_onI)
  fix x y
  assume x: "x ∈ S"
    and y: "y ∈ S"

  have conv: "convex_on S f"
    using cd
    by (rule convex_differentiable_onD_convex_on)

  have grad: "has_gradient f x (G x)"
    using cd x
    by (rule convex_differentiable_on_gradientD)

  show "f x + inner (G x) (y - x) ≤ f y"
    using convex_has_gradient_supports[OF conv grad x y] .
qed

lemma convex_differentiable_on_imp_supports_on:
  assumes cd: "convex_differentiable_on S f G"
  shows "supports_on S f G"
  using gradient_lower_bound_on_imp_supports_on[
      OF convex_differentiable_on_imp_gradient_lower_bound_on[OF cd]] .

lemma convex_differentiable_on_supports_at:
  assumes cd: "convex_differentiable_on S f G"
    and x: "x ∈ S"
  shows "supports_at S f x (G x)"
  using convex_differentiable_on_imp_supports_on[OF cd] x
  by (rule supports_onD)

lemma convex_differentiable_on_foc_imp_global_min_on:
  assumes cd: "convex_differentiable_on S f G"
    and foc: "first_order_condition_at S (G x) x"
  shows "global_min_on S f x"
  using gradient_lower_bound_on_and_foc_imp_global_min_on[
      OF convex_differentiable_on_imp_gradient_lower_bound_on[OF cd] foc] .

subsection ‹Main first-order consequences›

theorem convex_differentiable_on_supporting_hyperplanes:
  assumes cd: "convex_differentiable_on S f G"
  shows "supports_on S f G"
  using convex_differentiable_on_imp_supports_on[OF cd] .

theorem convex_differentiable_on_first_order_sufficient:
  assumes cd: "convex_differentiable_on S f G"
    and foc: "first_order_condition_at S (G x) x"
  shows "global_min_on S f x"
  using convex_differentiable_on_foc_imp_global_min_on[OF cd foc] .

subsection ‹Locale form›

locale convex_differentiable =
  fixes S :: "'a::real_inner set"
    and f :: "'a ⇒ real"
    and G :: "'a ⇒ 'a"
  assumes convex_f: "convex_on S f"
    and gradient_f: "has_gradient_on f S G"
begin

lemma convex_set:
  "convex S"
  using convex_f
  by (rule convex_on_imp_convex)

lemma has_gradient:
  assumes "x ∈ S"
  shows "has_gradient f x (G x)"
  using gradient_f assms
  by (rule has_gradient_onD)

lemma differentiable:
  assumes "x ∈ S"
  shows "f differentiable (at x)"
  using has_gradient[OF assms]
  by (rule has_gradient_imp_differentiable)

lemma segment_mem:
  assumes "x ∈ S"
    and "y ∈ S"
    and "0 ≤ t"
    and "t ≤ 1"
  shows "x + scaleR t (y - x) ∈ S"
  using convex_contains_affine_line[OF convex_set assms] .

lemma convex_bound_on_segment:
  assumes "x ∈ S"
    and "y ∈ S"
    and "0 ≤ t"
    and "t ≤ 1"
  shows "f (x + scaleR t (y - x)) ≤ (1 - t) * f x + t * f y"
  using convex_on_affine_lineD[OF convex_f assms] .

lemma gradient_lower_bound:
  "gradient_lower_bound_on S f G"
proof (rule gradient_lower_bound_onI)
  fix x y
  assume x: "x ∈ S"
    and y: "y ∈ S"

  show "f x + inner (G x) (y - x) ≤ f y"
    using convex_has_gradient_supports[OF convex_f has_gradient[OF x] x y] .
qed

lemma supports:
  assumes "x ∈ S"
  shows "supports_at S f x (G x)"
  using gradient_lower_bound_on_imp_supports_on[OF gradient_lower_bound] assms
  by (rule supports_onD)

lemma foc_imp_global_min:
  assumes "first_order_condition_at S (G x) x"
  shows "global_min_on S f x"
  using gradient_lower_bound_on_and_foc_imp_global_min_on[
      OF gradient_lower_bound assms] .

end

text ‹
This completes the first-order convex certificate layer.

The main bridge theorem is @{thm convex_has_gradient_supports}: for a convex
function that has a gradient at x, the gradient defines a supporting affine
lower bound on the feasible set.  The bundled consequence
@{thm convex_differentiable_on_first_order_sufficient} gives the usual
first-order sufficient condition for global optimality in convex optimization.

Later theories use these results as the first-order part of the analysis of
smooth gradient descent and projected gradient descent.
›

end