Theory MDP_reward_Util

theory MDP_reward_Util
  imports Blinfun_Util
begin
section ‹Auxiliary Lemmas›

subsection ‹Summability›

lemma summable_powser_const:
  fixes c :: real 
  assumes "¦c¦ < 1"
  shows "summable (λn. c^n * x)"
  using assms
  by (auto simp: mult.commute)

subsection ‹Infinite sums›

lemma suminf_split_head': 
  "summable (f :: nat ⇒ 'x :: real_normed_vector) ⟹ suminf f = f 0 + (∑n. f (Suc n))"
  by (auto simp: suminf_split_head)

lemma sum_disc_lim: 
  assumes "¦c :: real¦ < 1" 
  shows "(∑x. c^x * B) = B /(1-c)"
  by (simp add: assms suminf_geometric summable_geometric suminf_mult2[symmetric])

subsection ‹Bounded Functions›

lemma suminf_apply_bfun:
  fixes f :: "nat ⇒ 'c ⇒⇩b real"  
  assumes "summable f"
  shows "(∑i. f i) x = (∑i. f i x)"
  by (auto intro!: bounded_linear.suminf assms bounded_linear_intro[where K = 1] abs_le_norm_bfun)

lemma sum_apply_bfun:
  fixes f :: "nat ⇒ 'c ⇒⇩b real"  
  shows "(∑i<n. f i) x = (∑i<n. apply_bfun (f i) x)"
  by (induction n) auto  

subsection ‹Push-Forward of a Bounded Function›

lemma integrable_bfun_prob_space [simp]: 
  "integrable (measure_pmf P) (λt. apply_bfun f (F t) :: real)"
proof -
  obtain b where "∀t. ¦f (F t)¦ ≤ b"
    by (metis norm_le_norm_bfun real_norm_def)
  hence "(∫⇧+ x. ennreal ¦f (F x)¦ ∂P) ≤ b"
    using nn_integral_mono ennreal_leI
    by (auto intro: measure_pmf.nn_integral_le_const)
  then show ?thesis
    using ennreal_less_top le_less_trans 
    by (fastforce simp: integrable_iff_bounded)
qed

lift_definition push_exp :: "('b ⇒ 'c pmf) ⇒ ('c ⇒⇩b real) ⇒ ('b ⇒⇩b real)" is
  "λc f s. measure_pmf.expectation (c s) f"
  using bfun_integral_bound' .

declare push_exp.rep_eq[simp]

lemma norm_push_exp_le_norm: "norm (push_exp d x) ≤ norm x"
proof -
  have "⋀s. (∫s'. norm (x s') ∂d s) ≤ norm x"
    using measure_pmf.prob_space_axioms norm_le_norm_bfun[of x]
    by (auto intro!: prob_space.integral_le_const)
  hence aux: "⋀s. norm (∫s'. x s' ∂d s) ≤ norm x"
    using integral_norm_bound order_trans by blast
  have "norm (push_exp d x) = (⨆s. norm (∫s'. x s' ∂d s))"
    unfolding norm_bfun_def'
    by auto
  also have "… ≤ norm x"
    using aux by (fastforce intro!: cSUP_least)
  finally show ?thesis .
qed

lemma push_exp_bounded_linear [simp]: "bounded_linear (push_exp d)"
  using norm_push_exp_le_norm
  by (auto intro!: bounded_linear_intro[where K = 1])

lemma onorm_push_exp [simp]: "onorm (push_exp d) = 1"
proof (intro antisym)
  show "onorm (push_exp d) ≤ 1"
    using norm_push_exp_le_norm 
    by (auto intro!: onorm_bound)
next
  show "1 ≤ onorm (push_exp d)"
    using onorm[of _ 1, OF push_exp_bounded_linear] 
    by (auto simp: norm_bfun_def')
qed

lemma push_exp_return[simp]: "push_exp return_pmf = id"
  by (auto simp: eq_id_iff[symmetric])

subsection ‹Boundedness›

lemma bounded_abs[intro]: 
  "bounded (X' :: real set) ⟹ bounded (abs ` X')"
  by (auto simp: bounded_iff)

lemma bounded_abs_range[intro]: 
  "bounded (range f :: real set) ⟹ bounded (range (λx. abs (f x)))"
  by (auto simp: bounded_iff)

subsection ‹Probability Theory›

lemma integral_measure_pmf_bind: 
  assumes "(⋀x. ¦(f :: 'b ⇒ real) x¦ ≤ B)"
  shows "(∫x. f x ∂((measure_pmf M) ⤜ (λx. measure_pmf (N x)))) = (∫x. ∫y. f y ∂N x ∂M)"
  using assms
  by (subst integral_bind[of _ "count_space UNIV" B]) (auto simp: measure_pmf_in_subprob_space)

lemma lemma_4_3_1': 
  assumes "set_pmf p ⊆ W" 
    and "bounded ((w :: 'c ⇒ real) ` W)" 
    and "W ≠ {}"
    and "measure_pmf.expectation p w = (⨆p ∈ {p. set_pmf p ⊆ W}. measure_pmf.expectation p w)" 
  shows "∃x ∈ W. measure_pmf.expectation p w = w x"
proof -
  have abs_w_le_sup: "y ∈ W ⟹ ¦w y¦ ≤ (⨆x ∈ W. ¦w x¦)" for y
    using assms bounded_abs[OF assms(2)]
    by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: image_image)
  have "False" if "x ∈ set_pmf p" "w x < ⨆(w ` W)" for x
  proof -
    have ex_gr: "∃x'. x' ∈ W ∧ w x < w x'"
      using cSUP_least[of W w "w x"] that assms
      by fastforce
    let ?s = "λs. (if x = s then SOME x'. x' ∈ W ∧ w x < w x' else s)"
    have "measure_pmf.expectation p w < measure_pmf.expectation p (λxa. w (?s xa))"
    proof (intro measure_pmf.integral_less_AE[where A = "{x}"])
      show "integrable (measure_pmf p) w"
        using assms abs_w_le_sup 
        by (fastforce simp: AE_measure_pmf_iff 
            intro!: measure_pmf.integrable_const_bound)
      show "integrable (measure_pmf p) (λxa. w (?s xa))"
        using assms(1) ex_gr someI[where P = "λx'. (x' ∈ W) ∧ (w x < w x')"]
        by (fastforce simp: AE_measure_pmf_iff 
            intro!: abs_w_le_sup measure_pmf.integrable_const_bound)
      show "emeasure (measure_pmf p) {x} ≠ 0"
        by (simp add: emeasure_pmf_single_eq_zero_iff ‹x ∈ p›)
      show "{x} ∈ measure_pmf.events p"
        by auto
      show "AE xa∈{x} in p. w xa ≠ w (?s xa)" "AE xa in p. w xa ≤ w (?s xa)"
        using someI[where P = "λx'. (x' ∈ W) ∧ (w x < w x')"] ex_gr
        by (fastforce intro!: AE_pmfI)+
    qed
    hence "measure_pmf.expectation p w < ⨆((λp. measure_pmf.expectation p w) ` {p. set_pmf p ⊆ W})"
    proof (subst less_cSUP_iff, goal_cases)
      case 1
      then show ?case 
        using assms(1) 
        by blast
    next
      case 2
      then show ?case 
        using abs_w_le_sup
        by (fastforce 
            simp: AE_measure_pmf_iff 
            intro: cSUP_upper2 bdd_aboveI[where M = "(⨆x∈W. ¦w x¦)"]
            intro!: measure_pmf.integral_le_const measure_pmf.integrable_const_bound)
    next
      case 3
      then show ?case 
        using ex_gr someI[where P = "λx'. (x' ∈ W) ∧ (w x < w x')"] assms(1) 
        by (auto intro!: exI[of _ "map_pmf ?s p"])
    qed
    thus False
      using assms by auto
  qed
  hence 1: "x ∈ set_pmf p ⟹ w x = ⨆ (w ` W)" for x
    using assms
    by (fastforce intro: antisym simp: bounded_imp_bdd_above cSUP_upper)
  hence "w (SOME x. x ∈ set_pmf p) =  ⨆ (w ` W)"
    by (simp add: set_pmf_not_empty some_in_eq)
  thus ?thesis
    using 1 assms(1) set_pmf_not_empty some_in_eq 
    by (fastforce intro!: bexI[of _ "SOME x. x ∈ set_pmf p"]
        simp: AE_measure_pmf_iff Bochner_Integration.integral_cong_AE[where ?g = "λ_. ⨆ (w ` W)"])
qed

lemma lemma_4_3_1: 
  assumes "set_pmf p ⊆ W" "integrable (measure_pmf p) w" "bounded ((w :: 'c ⇒ real) ` W)"
  shows "measure_pmf.expectation p w ≤ ⨆(w ` W)"
  using assms bounded_has_Sup(1) prob_space_measure_pmf
  by (fastforce simp: AE_measure_pmf_iff intro!: prob_space.integral_le_const)

lemma bounded_integrable: 
  assumes "bounded (range v)" "v ∈ borel_measurable (measure_pmf p)" 
  shows "integrable (measure_pmf p) (v :: 'c ⇒ real)"
  using assms
  by (auto simp: bounded_iff AE_measure_pmf_iff intro!: measure_pmf.integrable_const_bound)

subsection ‹Argmax›
lemma finite_is_arg_max: "finite X ⟹ X ≠ {} ⟹ ∃x. is_arg_max (f :: 'c ⇒ real) (λx. x ∈ X) x"
  unfolding is_arg_max_def
proof (induction rule: finite_induct)
  case (insert x F)
  then show ?case
  proof (cases "∀y ∈ F. f y ≤ f x")
    case True
    then show ?thesis
      by (auto intro!: exI[of _ x])
  next
    case False
    then show ?thesis
      using insert by force
  qed
qed simp

lemma finite_arg_max_le:
  assumes "finite (X :: 'c set)" "X ≠ {}"
  shows "s ∈ X ⟹ (f :: 'c ⇒ real) s ≤ f (arg_max_on (f :: 'c ⇒ real) X)"
  unfolding arg_max_def arg_max_on_def
  by (metis assms(1) assms(2) finite_is_arg_max is_arg_max_linorder someI_ex)

lemma arg_max_on_in:
  assumes "finite (X :: 'c set)" "X ≠ {}"
  shows "(arg_max_on (f :: 'c ⇒ real)  X) ∈ X"
  unfolding arg_max_on_def arg_max_def
  by (metis assms(1) assms(2) finite_is_arg_max is_arg_max_def someI)

lemma finite_arg_max_eq_Max:
  assumes "finite (X :: 'c set)" "X ≠ {}"
  shows "(f :: 'c ⇒ real) (arg_max_on f X) = Max (f ` X)"
  using assms
  by (auto intro!: Max_eqI[symmetric] finite_arg_max_le arg_max_on_in)


lemma arg_max_SUP: "is_arg_max (f :: 'b ⇒ real) (λx. x ∈ X) m ⟹ f m = (⨆(f ` X))"
  unfolding is_arg_max_def
  by (auto intro!: antisym cSUP_upper bdd_aboveI[of _ "f m"] cSUP_least)

definition "has_max X ≡ ∃x ∈ X. ∀x' ∈ X. x' ≤ x"
definition "has_arg_max f X ≡ ∃x. is_arg_max f (λx. x ∈ X) x"

lemma "has_max ((f :: 'b ⇒ real) ` X) ⟷ has_arg_max f X"
  unfolding has_max_def has_arg_max_def is_arg_max_def
  using not_less by (auto dest!: leD simp: not_less)

lemma has_arg_max_is_arg_max: "has_arg_max f X ⟹ is_arg_max f (λx. x ∈ X) (arg_max f (λx. x ∈ X))"
  unfolding has_arg_max_def arg_max_def
  by (auto intro: someI)

lemma has_arg_max_arg_max: "has_arg_max f X ⟹ (arg_max f (λx. x ∈ X)) ∈ X"
  unfolding has_arg_max_def arg_max_def is_arg_max_def by (auto intro: someI2_ex)
  

lemma app_arg_max_ge: "has_arg_max (f :: 'b ⇒ real) X ⟹ x ∈ X ⟹ f x ≤ f (arg_max_on f X)"
  unfolding has_arg_max_def arg_max_on_def arg_max_def is_arg_max_def
  using someI[where ?P = "λx. x ∈ X ∧ (∄y. y ∈ X ∧ f x < f y)"] le_less_linear
  by auto

lemma app_arg_max_eq_SUP: "has_arg_max (f :: 'b ⇒ real) X ⟹ f (arg_max_on f X) = ⨆(f ` X)"
  by (simp add: arg_max_SUP arg_max_on_def has_arg_max_is_arg_max)

lemma SUP_is_arg_max: 
  assumes "x ∈ X" "bdd_above (f ` X)" "(f :: 'c ⇒ real) x = ⨆(f ` X)" 
  shows "is_arg_max f (λx. x ∈ X) x"
  unfolding is_arg_max_def
  using not_less assms cSUP_upper[of _ X f] 
  by auto

lemma is_arg_max_linorderI[intro]: fixes f :: "'c ⇒ 'b :: linorder"
  assumes "P x" "⋀y. (P y ⟹ f x ≥ f y)"
  shows "is_arg_max f P x"
  using assms by (auto simp: is_arg_max_linorder)

lemma is_arg_max_linorderD[dest]: fixes f :: "'c ⇒ 'b :: linorder"
  assumes "is_arg_max f P x"
  shows "P x" "(P y ⟹ f x ≥ f y)"
  using assms by (auto simp: is_arg_max_linorder)

lemma is_arg_max_cong: 
  assumes "⋀x. P x ⟹ f x = g x"
  shows "is_arg_max f P x ⟷ is_arg_max g P x"
  unfolding is_arg_max_def using assms by auto

lemma is_arg_max_cong':
  assumes "⋀x. P x ⟹ f x = g x"
  shows "is_arg_max f P = is_arg_max g P"
  using assms by (auto cong: is_arg_max_cong)

lemma is_arg_max_congI: 
  assumes "is_arg_max f P x" "⋀x. P x ⟹ f x = g x" 
  shows "is_arg_max g P x" 
  using is_arg_max_cong assms by force

subsection ‹Contraction Mappings›

definition "is_contraction C ≡ ∃l. 0 ≤ l ∧ l < 1 ∧ (∀v u. dist (C v) (C u) ≤ l * dist v u)"

lemma banach':
  fixes C :: "'b :: complete_space ⇒ 'b"
  assumes "is_contraction C"
  shows "∃!v. C v = v" "⋀v. (λn. (C ^^ n) v) ⇢ (THE v. C v = v)"
proof -
  obtain v where C: "C v = v" "∀v'. C v' = v' ⟶ v' = v" 
    by (metis assms is_contraction_def banach_fix_type)
  obtain l where cont: "dist (C v) (C u) ≤ l * dist v u" "0 ≤ l" "l < 1" for v u
    using assms is_contraction_def by blast
  have *: "⋀n v0. dist ((C ^^ n) v0) v ≤ l ^ n * dist v0 v"
  proof -
    fix n v0
    show "dist ((C ^^ n) v0) v ≤ l ^ n * dist v0 v"
    proof (induction n)
      case (Suc n)
      thus "dist ((C ^^ Suc n) v0) v ≤ l ^ Suc n * dist v0 v"
        using ‹0 ≤ l›
        by (subst C(1)[symmetric]) (auto simp: algebra_simps intro!: order_trans[OF cont(1)] mult_left_mono)
    qed simp
  qed
  have "(λn. l ^ n) ⇢ 0"
    by (simp add: LIMSEQ_realpow_zero ‹0 ≤ l› ‹l < 1›)
  hence "⋀v0. (λn. l ^ n * dist v0 v) ⇢ 0"
    by (simp add: tendsto_mult_left_zero)
  hence "(λn. dist ((C ^^ n) v0) v) ⇢ 0" for v0
      using * order_trans abs_ge_self
      by (subst Limits.tendsto_0_le[of "(λn. l ^ n * dist v0 v)" _ _ 1]) 
        (fastforce intro!: eventuallyI)+
  hence "⋀v0. (λn. (C ^^ n) v0) ⇢ v"
    using tendsto_dist_iff by blast
  thus "⋀v0. (λn. (C ^^ n) v0) ⇢ (THE v. C v = v)"
    by (metis (mono_tags, lifting) C theI')
next
  show "∃!v. C v = v"
    using assms banach_fix_type unfolding is_contraction_def by blast
qed

lemma contraction_dist:
  fixes C :: "'b :: complete_space ⇒ 'b"
  assumes "⋀v u. dist (C v) (C u) ≤ c  * dist v u"
  assumes "0 ≤ c" "c < 1"
  shows "(1 - c) * dist v (THE v. C v = v) ≤ dist v (C v)"
proof -
  have "is_contraction C"
    unfolding is_contraction_def using assms by auto
  then obtain v_fix where v_fix: "v_fix = (THE v. C v = v)"
    using the1_equality by blast
  hence "(λn. (C ^^ n) v) ⇢ v_fix"
    using banach'[OF ‹is_contraction C›] by simp
  have dist_contr_le_pow: "⋀n. dist ((C ^^ n) v) ((C ^^ Suc n) v) ≤ c ^ n * dist v (C v)"
  proof -
    fix n 
    show "dist ((C ^^ n) v) ((C ^^ Suc n) v) ≤ c ^ n * dist v (C v)"
      using assms
      by (induction n) (auto simp: algebra_simps intro!: order.trans[OF assms(1)] mult_left_mono)
  qed
  have summable_C: "summable (λi. dist ((C ^^ i) v) ((C ^^ Suc i) v))"
        using dist_contr_le_pow assms summable_powser_const
        by (intro summable_comparison_test[of "(λi. dist ((C ^^ i) v) ((C ^^ Suc i) v))" "λi. c^i * dist v (C v)"]) 
          auto
  have "∀e > 0. dist v v_fix ≤ (∑i. dist ((C ^^ i) v) ((C ^^ (Suc i)) v)) + e"
  proof safe
    fix e ::real assume "0 < e"
    have "∀⇩F n in sequentially. dist ((C^^n) v) v_fix < e"
      using ‹(λn. (C ^^ n) v) ⇢ v_fix› ‹0 < e› tendsto_iff by force
    then obtain N where "dist ((C^^N) v) v_fix < e"
      by fastforce
    hence *: "dist v v_fix ≤ dist v ((C^^N) v) + e"
      by (metis add_le_cancel_left dist_commute dist_triangle_le less_eq_real_def)
    have "dist v ((C^^N) v) ≤ (∑i≤N. dist ((C ^^ i) v) ((C ^^ (Suc i)) v))"
    proof (induction N arbitrary: v)
      case 0
      then show ?case by simp
    next
      case (Suc N)      
      have "dist v ((C ^^ Suc N) v) ≤ dist v (C v) + dist (C v) ((C^^(Suc N)) v)"
        by metric
      also have "… =  dist v (C v) + dist (C v) ((C^^N) (C v))"
        by (metis funpow_simps_right(2) o_def)
      also have "… ≤ dist v (C v) + (∑i≤N. dist ((C ^^ i) (C v)) ((C ^^ Suc i) (C v)))"
        using Suc.IH add_le_cancel_left by blast
      also have "… ≤ dist v (C v) + (∑i≤N. dist ((C ^^Suc i) v) ((C ^^ (Suc (Suc i))) v))"
        by (simp only: funpow_simps_right(2) o_def)
      also have "… ≤ (∑i≤Suc N. dist ((C ^^ i) v) ((C ^^ (Suc i)) v))"
        by (subst sum.atMost_Suc_shift) simp
      finally show "dist v ((C ^^ Suc N) v) ≤ (∑i≤Suc N. dist ((C ^^ i) v) ((C ^^ Suc i) v))" .
    qed
    moreover have 
      "(∑i≤N. dist ((C ^^ i) v) ((C ^^ Suc i) v)) ≤ (∑i. dist ((C ^^ i) v) ((C ^^ (Suc i)) v))"
      using summable_C 
      by (auto intro: sum_le_suminf)
    ultimately have "dist v ((C^^N) v) ≤ (∑i. dist ((C ^^ i) v) ((C ^^ (Suc i)) v))"
      by linarith
    thus "dist v v_fix ≤ (∑i. dist ((C ^^ i) v) ((C ^^ Suc i) v)) + e"
      using * by fastforce
  qed
  hence le_suminf: "dist v v_fix ≤ (∑i. dist ((C ^^ i) v) ((C ^^ Suc i) v))"
    using field_le_epsilon by blast
  have "dist v v_fix ≤ (∑i. c ^ i * dist v (C v))"
    using dist_contr_le_pow summable_C assms summable_powser_const
    by (auto intro!: order_trans[OF le_suminf] suminf_le)
  hence "dist v v_fix ≤ dist v (C v) / (1 - c)"
    using sum_disc_lim
    by (metis sum_disc_lim abs_of_nonneg assms(2) assms(3))
  hence "(1 - c) * dist v v_fix ≤ dist v (C v)"
    using assms(3) mult.commute pos_le_divide_eq 
    by (metis diff_gt_0_iff_gt)
  thus ?thesis
    using v_fix by blast
qed

subsection ‹Limits›
lemma tendsto_bfun_sandwich:
  assumes 
    "(f :: nat ⇒ 'b ⇒⇩b real) ⇢ x" "(g :: nat ⇒ 'b ⇒⇩b real) ⇢ x" 
    "eventually (λn. f n ≤ h n) sequentially" "eventually (λn. h n ≤ g n) sequentially"
  shows "(h :: nat ⇒ 'b ⇒⇩b real) ⇢ x"
proof -
  have 1: "(λn.  dist (f n) (g n) + dist (g n) x) ⇢ 0"
    using tendsto_dist[OF assms(1) assms(2)] tendsto_dist_iff assms
    by (auto intro!: tendsto_add_zero)
  have "eventually (λn. dist (h n) (g n) ≤ dist (f n) (g n)) sequentially"    
    using assms(3) assms(4)
  proof eventually_elim
    case (elim n)
    hence "dist (h n a) (g n a) ≤ dist (f n a) (g n a)" for a
    proof - 
      have "f n a ≤ h n a" "h n a ≤ g n a"
        using elim unfolding less_eq_bfun_def by auto
      thus ?thesis
        using dist_real_def by fastforce
    qed
    thus ?case
      unfolding dist_bfun.rep_eq
      by (auto intro!: cSUP_mono bounded_imp_bdd_above simp: dist_real_def bounded_minus_comp bounded_abs_range)
  qed
  moreover have "eventually (λn. dist (h n) x ≤ dist (h n) (g n) + dist (g n) x) sequentially"
    by (simp add: dist_triangle)
  ultimately have 2: "eventually (λn. dist (h n) x ≤ dist (f n) (g n) + dist (g n) x) sequentially"
    using eventually_elim2 by fastforce
  have "(λn. dist (h n) x) ⇢ 0"
  proof (subst tendsto_iff, safe)
    fix e ::real
    assume "e > 0"
    hence 3: "∀⇩F xa in sequentially. dist (f xa) (g xa) + dist (g xa) x < e"
      using 1 
      by (auto simp: tendsto_iff)
    show "∀⇩F xa in sequentially. dist (dist (h xa) x) 0 < e"
      by (rule eventually_mp[OF _ 3]) (fastforce intro: 2 eventually_mono)
  qed
  thus ?thesis
    using tendsto_dist_iff
    by auto
qed

subsection ‹Supremum›

lemma SUP_add_le: 
  assumes "X ≠ {}" "bounded (B ` X)" "bounded (A' ` X)" 
  shows "(⨆c ∈ X. (B :: 'a ⇒ real) c + A' c) ≤ (⨆b ∈ X. B b) + (⨆a ∈ X. A' a)"
  using assms 
  by (auto simp: add_mono bounded_has_Sup(1) intro!: cSUP_least)+

lemma le_SUP_diff':
  assumes ne: "X ≠ {}"
    and bdd: "bounded (B ` X)" "bounded (A' ` X)" 
    and sup_le: "(⨆a ∈ X. (A' :: 'a ⇒ real) a) ≤ (⨆b ∈ X. B b)"
  shows  "(⨆b ∈ X. B b) - (⨆a ∈ X. (A' :: 'a ⇒ real) a) ≤ (⨆c ∈ X. B c - A' c)"
proof -
  have "bounded ((λx. (B x - A' x)) ` X)"
    using bdd bounded_minus_comp by blast
  have "(⨆b ∈ X. B b) - (⨆a ∈ X. A' a) - e ≤ (⨆c ∈ X. B c - A' c)" if e: "e > 0" for e
  proof -
    obtain z where z: "(⨆b ∈ X. B b) - e≤ B z" "z ∈ X"
       using e ne
       by (subst less_cSupE[where ?y = "⨆ (B ` X) - e", where ?X = "B`X"]) fastforce+
    hence " ((⨆a ∈ X. A' a) ≤ B z + e)"
      using sup_le
      by force
    hence "A' z ≤ B z + e"
      using ‹z ∈ X› bdd bounded_has_Sup(1) by fastforce
    thus "(⨆b ∈ X. B b) - (⨆a ∈ X. A' a) -e ≤ (⨆c ∈ X. B c - A' c)"
      using ‹bounded ((λx. B x - A' x) ` X)› z bounded_has_Sup(1)[OF bdd(2)]
      by (subst cSUP_upper2[where x = z]) (fastforce intro!: bounded_imp_bdd_above)+
  qed
  thus ?thesis
    by (subst field_le_epsilon) fastforce+
qed

lemma le_SUP_diff:
  fixes A' :: "'a ⇒ real"
  assumes "X ≠ {}" "bounded (B ` X)" "bounded (A' ` X)" "(⨆a ∈ X. A' a) ≤ (⨆b ∈ X. B b)"
  shows  "0 ≤ (⨆c ∈ X. B c - A' c)"
  using assms
  by (auto intro!: order.trans[OF _ le_SUP_diff'])

lemma bounded_SUP_mul[simp]: 
  "X ≠ {} ⟹ 0 ≤ l ⟹ bounded (f ` X) ⟹ (⨆x ∈ X. (l :: real) * f x) = (l * (⨆x ∈ X. f x))" 
proof -
  assume "X ≠ {} "" bounded (f ` X)" "0 ≤ l"
  have "(⨆x ∈ X. ereal l * ereal (f x)) = (l * (⨆x ∈ X. ereal (f x)))"
    by (simp add: Sup_ereal_mult_left' ‹0 ≤ l› ‹X ≠ {}›)
  obtain b where "∀a ∈X. ¦f a¦ ≤ b"
    using ‹bounded (f ` X)› bounded_real by auto
  have "∀a ∈X. ¦ereal (f a)¦ ≤ b"
    by (simp add: ‹∀a∈X. ¦f a¦ ≤ b›)
  hence sup_leb: "(⨆a∈X. ¦ereal (f a)¦)≤ b"
    by (simp add: SUP_least)
  have "(⨆a∈X. ereal (f a)) ≤ (⨆a∈X. ¦ereal (f a)¦)"
    by (auto intro: Complete_Lattices.SUP_mono')
  moreover have "-(⨆a∈X. ereal (f a)) ≤ (⨆a∈X. ¦ereal (f a)¦)"
    using ‹X ≠ {}›
    by (auto intro!: Inf_less_eq cSUP_upper2 simp add: ereal_INF_uminus_eq[symmetric])
  ultimately have "¦(⨆a∈X. ereal (f a))¦ ≤ (⨆a∈X. ¦ereal (f a)¦)"
    by (auto intro: ereal_abs_leI)
  hence "¦⨆a∈X. ereal (f a)¦ ≤ b"
    using sup_leb by auto
  hence "¦⨆a∈X. ereal (f a)¦ ≠ ∞"
    by auto
  hence "(⨆x ∈ X. ereal (f x)) = ereal (⨆x ∈ X. (f x))"
    using ereal_SUP by metis
  hence "(⨆x ∈ X. ereal (l * f x)) = ereal (l * (⨆x ∈ X. f x))"
    using ‹(⨆x∈X. ereal l * ereal (f x)) = ereal l * (⨆x∈X. ereal (f x))› by auto
  hence "ereal (⨆x ∈ X. l * f x) = ereal (l * (⨆x ∈ X. f x))"
    by (simp add: ereal_SUP)
  thus ?thesis
    by auto
qed

lemma abs_cSUP_le[intro]: 
  "X ≠ {} ⟹ bounded (F ` X) ⟹ ¦⨆x ∈ X. (F x) :: real¦ ≤ (⨆x ∈ X. ¦F x¦)"
  by (auto intro!: cSup_abs_le cSUP_upper2 bounded_imp_bdd_above simp: image_image[symmetric])

section ‹Least argmax›
definition "least_arg_max f P = (LEAST x. is_arg_max f P x)"

lemma least_arg_max_prop: "∃x::'a::wellorder. P x ⟹ finite {x. P x} ⟹ P (least_arg_max (f :: _ ⇒ real) P)"
  unfolding least_arg_max_def
  apply (rule LeastI2_ex)
  using finite_is_arg_max[of "{x. P x}", where f = f]
  by auto

lemma is_arg_max_apply_eq: "is_arg_max (f :: _ ⇒ _ :: linorder)  P x ⟹ is_arg_max f P y ⟹ f x = f y"
  by (auto simp: is_arg_max_def not_less dual_order.eq_iff)
  
lemma least_arg_max_apply:
  assumes "is_arg_max (f :: _ ⇒ _ :: linorder) P (x::_::wellorder)" 
  shows "f (least_arg_max f P) = f x"
proof -
  have "is_arg_max f P (least_arg_max f P)"
    by (metis LeastI_ex assms least_arg_max_def)
  thus ?thesis
    using is_arg_max_apply_eq assms by metis
qed

lemma apply_arg_max_eq_max: "finite {x . P x} ⟹ is_arg_max (f :: _ ⇒ _ :: linorder) P x ⟹ f x = Max (f ` {x. P x})"
  by (auto simp: is_arg_max_def intro!: Max_eqI[symmetric])

lemma apply_arg_max_eq_max': "finite X⟹ is_arg_max (f :: _ ⇒ _ :: linorder) (λx. x ∈ X) x ⟹ (MAX x ∈ X. f x) = f x"
  by (auto simp: is_arg_max_linorder intro!: Max_eqI)

lemma least_arg_max_is_arg_max: "P ≠ {} ⟹ finite P ⟹ is_arg_max f (λx::_::wellorder. x ∈ P) (least_arg_max (f :: _ ⇒ real) (λx. x ∈ P))"
  unfolding least_arg_max_def
  apply (rule LeastI_ex)
  using finite_is_arg_max 
  by auto

lemma is_arg_max_const: "is_arg_max (f :: _ ⇒ _ :: linorder) (λy. y = c) x ⟷ x = c"
  unfolding is_arg_max_def
  by auto

lemma least_arg_max_cong': 
  assumes "⋀x. is_arg_max f P x = is_arg_max g P x"
  shows "least_arg_max f P = least_arg_max g P"
  unfolding least_arg_max_def using assms by metis

end