Theory Minimizers_Definition

section ‹Minimizers in Topological and Metric Spaces›

theory Minimizers_Definition
  imports Auxilary_Facts
begin

subsection ‹Abstract Topological Definitions›

― ‹We first define a highly abstract set of definitions for general topological spaces.  
      In practice, we will assume we are working on a metric space to employ the geometry  
      to optimize functions.›

definition global_minimizer :: "('a::topological_space ⇒ real) ⇒ 'a ⇒ bool" where
  "global_minimizer f x_star ⟷ (∀x. f x_star ≤ f x)"

definition local_minimizer_on :: "('a::topological_space ⇒ real) ⇒ 'a ⇒ 'a set ⇒ bool" where
  "local_minimizer_on f x_star U ⟷ (open U ∧ x_star ∈ U ∧ (∀x ∈ U. f x_star ≤ f x))"

definition local_minimizer :: "('a::topological_space ⇒ real) ⇒ 'a ⇒ bool" where
  "local_minimizer f x_star ⟷ (∃U. open U ∧ x_star ∈ U ∧ (∀x ∈ U. f x_star ≤ f x))"

definition isolated_local_minimizer_on :: "('a::topological_space ⇒ real) ⇒ 'a ⇒ 'a set ⇒ bool" where
  "isolated_local_minimizer_on f x_star U ⟷ 
     (local_minimizer_on f x_star U ∧ ({x ∈ U. local_minimizer f x} = {x_star}))"

definition isolated_local_minimizer :: "('a::topological_space ⇒ real) ⇒ 'a ⇒ bool" where
  "isolated_local_minimizer f x_star ⟷ 
     (∃U. local_minimizer_on f x_star U ∧ ({x ∈ U. local_minimizer f x} = {x_star}))"

definition strict_local_minimizer_on :: "('a::topological_space ⇒ real) ⇒ 'a ⇒ 'a set ⇒ bool" where
  "strict_local_minimizer_on f x_star U ⟷ 
     (open U ∧ x_star ∈ U ∧ (∀x ∈ U - {x_star}. f x_star < f x))"

definition strict_local_minimizer :: "('a::topological_space ⇒ real) ⇒ 'a ⇒ bool" where
  "strict_local_minimizer f x_star ⟷ (∃U. strict_local_minimizer_on f x_star U)"

subsection ‹Metric Space Reformulations›

― ‹Here are simplified definitions of the above restricted to metric spaces.  
      These definitions yield sets which are easier to work with.›

lemma local_minimizer_on_def2:
  fixes f :: "'a::metric_space ⇒ real"
  assumes "local_minimizer f x_star"
  shows "∃N > 0. ∀x ∈ ball x_star N. f x_star ≤ f x"
proof -
  from assms obtain U where
    "open U" "x_star ∈ U" and local_min: "∀x ∈ U. f x_star ≤ f x"
    unfolding local_minimizer_def by auto
  then obtain N where N_pos: "N > 0" and ball_in_U: "ball x_star N ⊆ U"
    using open_contains_ball by blast 
  hence "∀x ∈ ball x_star N. f x_star ≤ f x"
    using ball_in_U local_min by auto
  thus ?thesis
    using N_pos by auto
qed

lemma local_minimizer_def2:
  fixes f :: "'a::metric_space ⇒ real"
  assumes "local_minimizer f x_star"
  shows "∃N > 0. ∀x. dist x x_star < N ⟶ f x_star ≤ f x"
proof -
  from assms obtain U where
    "open U" "x_star ∈ U" and local_min: "∀x ∈ U. f x_star ≤ f x"
    unfolding local_minimizer_def by auto
  then obtain N where N_pos: "N > 0" and ball_in_U: "ball x_star N ⊆ U"
    using open_contains_ball by blast 
  hence "∀x. dist x x_star < N ⟶ x ∈ ball x_star N"
    by (subst mem_ball, simp add: dist_commute)
  hence "∀x. dist x x_star < N ⟶ f x_star ≤ f x"
    using ball_in_U local_min by blast
  thus ?thesis
    using N_pos by auto
qed

lemma isolated_local_minimizer_on_def2:
  fixes f :: "'a::metric_space ⇒ real"
  assumes "isolated_local_minimizer_on f x_star U"
  shows "∃N > 0. ∀x ∈ ball x_star N. (local_minimizer f x ⟶ x = x_star)"
proof -
  from assms have
    "local_minimizer_on f x_star U"
    and unique_min: "{x ∈ U. local_minimizer f x} = {x_star}"
    unfolding isolated_local_minimizer_on_def by auto
  then obtain N where N_pos: "N > 0" and ball_in_U: "ball x_star N ⊆ U"
    using open_contains_ball by (metis local_minimizer_on_def)
  have "∀x ∈ ball x_star N. local_minimizer f x ⟶ x = x_star"
  proof(clarify)
    fix x
    assume "x ∈ ball x_star N"
    then have "x ∈ U" using ball_in_U by auto
    moreover assume "local_minimizer f x"
    hence "x ∈ {x ∈ U. local_minimizer f x}" using ‹x ∈ U› by auto
    hence "x ∈ {x_star}" using unique_min by auto
    ultimately show "x = x_star"
      by simp 
  qed
  thus ?thesis using N_pos by auto
qed

lemma isolated_local_minimizer_def2:
  fixes f :: "'a::metric_space ⇒ real"
  assumes "isolated_local_minimizer f x_star"
  shows "∃N > 0. ∀x ∈ ball x_star N. (local_minimizer f x ⟶ x = x_star)"
proof -
  from assms obtain U where
    "local_minimizer_on f x_star U"
    and unique_min: "{x ∈ U. local_minimizer f x} = {x_star}"
    unfolding isolated_local_minimizer_def by auto
  then obtain N where N_pos: "N > 0" and ball_in_U: "ball x_star N ⊆ U"
    using open_contains_ball by (metis local_minimizer_on_def)
  have "∀x ∈ ball x_star N. local_minimizer f x ⟶ x = x_star"
  proof(clarify)
    fix x
    assume "x ∈ ball x_star N"
    then have "x ∈ U" using ball_in_U by auto
    moreover assume "local_minimizer f x"
    hence "x ∈ {x ∈ U. local_minimizer f x}" using ‹x ∈ U› by auto
    hence "x ∈ {x_star}" using unique_min by auto
    ultimately show "x = x_star" by simp
  qed
  thus ?thesis using N_pos by auto
qed

lemma strict_local_minimizer_on_def2:
  fixes f :: "'a::metric_space ⇒ real"
  assumes "strict_local_minimizer_on f x_star U"
  shows "∃N > 0. ∀x ∈ ball x_star N - {x_star}. f x_star < f x"
proof -
  from assms have
    "open U" "x_star ∈ U" and strict_min: "∀x ∈ U - {x_star}. f x_star < f x"
    unfolding strict_local_minimizer_on_def by auto
  then obtain N where N_pos: "N > 0" and ball_in_U: "ball x_star N ⊆ U"
    using open_contains_ball by metis
  have "∀x ∈ ball x_star N - {x_star}. f x_star < f x"
  proof
    fix x
    assume "x ∈ ball x_star N - {x_star}"
    hence "x ∈ U - {x_star}" using ball_in_U by auto
    thus "f x_star < f x"
      using strict_min by auto
  qed
  thus ?thesis using N_pos by auto
qed

lemma strict_local_minimizer_def2:
  fixes f :: "'a::metric_space ⇒ real"
  assumes "strict_local_minimizer f x_star"
  shows "∃N > 0. ∀x ∈ ball x_star N - {x_star}. f x_star < f x"
proof -
  from assms obtain U where
    "strict_local_minimizer_on f x_star U"
    unfolding strict_local_minimizer_def by auto
  then have
    "open U" "x_star ∈ U" and strict_min: "∀x ∈ U - {x_star}. f x_star < f x"
    unfolding strict_local_minimizer_on_def by auto
  then obtain N where N_pos: "N > 0" and ball_in_U: "ball x_star N ⊆ U"
    using open_contains_ball by metis
  have "∀x ∈ ball x_star N - {x_star}. f x_star < f x"
  proof
    fix x
    assume "x ∈ ball x_star N - {x_star}"
    hence "x ∈ U - {x_star}" using ball_in_U by auto
    thus "f x_star < f x"
      using strict_min by auto
  qed
  thus ?thesis using N_pos by auto
qed

lemma local_minimizer_neighborhood:
  fixes f :: "real ⇒ real"
  assumes loc_min: "local_minimizer f x_min"
  shows "∃δ > 0. ∀h. ¦h¦ < δ ⟶ f (x_min + h) ≥ f x_min"
proof -
  obtain N where N_pos: "N > 0" and N_prop: "∀x. dist x x_min < N ⟶ f x_min ≤ f x"
    using local_minimizer_def2[OF loc_min] by auto
  then have "∀h. abs h < N ⟶ f (x_min + h) ≥ f x_min"
    by (simp add: dist_real_def)
  then show ?thesis
    using N_pos by blast 
qed

lemma local_minimizer_from_neighborhood:
  fixes f :: "real ⇒ real" and x_min :: real
  assumes "∃δ > 0. ∀x. ¦x - x_min¦ < δ ⟶ f x_min ≤ f x"
  shows "local_minimizer f x_min"
proof -
  from assms obtain δ where δ_pos: "δ > 0" and H: "∀x. ¦x - x_min¦ < δ ⟶ f x_min ≤ f x"
    by auto
  obtain U where U_def: "U = {x. ¦x - x_min¦ < δ}"
    by simp
  then have "open U"
    by (smt (verit) dist_commute dist_real_def mem_Collect_eq metric_space_class.open_ball subsetI topological_space_class.openI) 
  moreover have "x_min ∈ U"
    using U_def δ_pos by force 
  moreover have "∀x ∈ U. f x_min ≤ f x"
    using H U_def by blast
  ultimately show ?thesis
    unfolding local_minimizer_def by auto
qed

end