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. x∈S) x}"

definition arg_max_set :: "('a ⇒ 'b::ord) ⇒ 'a set ⇒ 'a set"
  where
    "arg_max_set f S = {x. is_arg_max f (λx. x∈S) 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