Theory Argmax

(* License: LGPL *)


section ‹Arg Min and Arg Max sets›

theory Argmax
  imports
    "Complex_Main"
begin

subsection ‹ Definitions and Lemmas by Julian Parsert ›


text ‹ definition of argmax and argmin returing a set. ›

definition arg_min_set :: "('a  'b::ord)  'a set  'a set"
  where
    "arg_min_set f S = {x. is_arg_min f (λx. xS) x}"

definition arg_max_set :: "('a  'b::ord)  'a set  'a set"
  where
    "arg_max_set f S = {x. is_arg_max f (λx. xS) x}"


text ‹ Useful lemmas for @{term "arg_max_set"} and @{term "arg_min_set"}. ›

lemma no_better_in_s:
  assumes "x  arg_max_set f S"
  shows "y. y  S  (f y) > (f x)"
  by (metis arg_max_set_def assms is_arg_max_def mem_Collect_eq)

lemma argmax_sol_in_s:
  assumes "x  arg_max_set f S"
  shows "x  S"
  by (metis CollectD arg_max_set_def assms is_arg_max_def)

lemma leq_all_in_sol:
  fixes f :: "'a  ('b :: preorder)"
  assumes "x  arg_max_set f S"
  shows "y  S. f y  f x  y  arg_max_set f S"
  using assms le_less_trans by (auto simp: arg_max_set_def is_arg_max_def)

lemma all_leq:
  fixes f :: "'a  ('b :: linorder)"
  assumes "x  arg_max_set f S"
  shows "y  S. f x  f y"
  by (meson assms leI no_better_in_s)

lemma all_in_argmax_equal:
  fixes f :: "'a  ('b :: linorder)"
  assumes "x  arg_max_set f S"
  shows "y  arg_max_set f S. f x = f y"
    by (meson all_leq argmax_sol_in_s assms le_less no_better_in_s)

end