Session MDP-Rewards

Theory Bounded_Functions

(* Author: Maximilian Schäffeler, adapted from HOL-Analysis.Bounded_Continuous_Function *)

section ‹Bounded Functions›

theory Bounded_Functions
  imports
    "HOL.Topological_Spaces"
    "HOL-Analysis.Uniform_Limit"
    "HOL-Probability.Probability"
begin

subsection ‹Definition›

definition✐‹tag important› "bfun = {f. bounded (range f)}"

typedef (overloaded) ('a, 'b) bfun ("(_ ⇒b _)" [22] 21) =
  "bfun::('a ⇒ 'b :: metric_space) set"
  morphisms apply_bfun Bfun
  by (fastforce simp: bounded_def bfun_def)

declare [[coercion "apply_bfun :: ('a ⇒b ('b :: metric_space)) ⇒ 'a ⇒ 'b"]]

setup_lifting type_definition_bfun

lemma bounded_apply_bfun[intro, simp]: "bounded (range (apply_bfun x))"
  using apply_bfun by (auto simp: bfun_def)

lemma bfun_eqI[intro]: "(⋀x. apply_bfun f x = apply_bfun g x) ⟹ f = g"
  by transfer auto

lemma bfun_eqD[dest]: "f = g ⟹ (⋀x. apply_bfun f x = apply_bfun g x)"
  by auto

lemma bfunE:
  assumes "f ∈ bfun"
  obtains g where "f = apply_bfun g"
  by (blast intro: apply_bfun_cases assms)

lemma const_bfun: "(λx. b) ∈ bfun"
  by (auto simp: bfun_def image_def)

lift_definition const_bfun::"'b ⇒ ('a ⇒b ('b :: metric_space))" is "λ(c::'b) _. c"
  by (rule const_bfun)

lemma bounded_dist_le_SUP_dist:
  "bounded (range f) ⟹ bounded (range g) ⟹ dist (f x) (g x) ≤ (SUP x. dist (f x) (g x))"
  by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp)

instantiation bfun :: (type, metric_space) metric_space
begin

lift_definition✐‹tag important› dist_bfun :: "('a ⇒b 'b) ⇒ ('a ⇒b 'b) ⇒ real"
  is "λf g. (SUP x. dist (f x) (g x))" .

definition uniformity_bfun :: "(('a ⇒b 'b) × 'a ⇒b 'b) filter"
  where "uniformity_bfun = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"

definition open_bfun :: "('a ⇒b 'b) set ⇒ bool"
  where "open_bfun S = (∀x∈S. ∀F (x', y) in uniformity. x' = x ⟶ y ∈ S)"

lemma dist_bounded:
  fixes f g :: "'a ⇒b 'b"
  shows "dist (f x) (g x) ≤ dist f g"
  by transfer (auto intro!: bounded_dist_le_SUP_dist simp: bfun_def)

lemma dist_bound:
  fixes f g :: "'a ⇒b ('b :: metric_space)"
  assumes "⋀x. dist (f x) (g x) ≤ b"
  shows "dist f g ≤ b"
  using assms
  by transfer (auto intro!: cSUP_least)

lemma dist_fun_lt_imp_dist_val_lt:
  fixes f g :: "'a ⇒b 'b"
  assumes "dist f g < e"
  shows "dist (f x) (g x) < e"
  using dist_bounded assms
  by (rule le_less_trans)

instance
proof
  fix f g h :: "'a ⇒b 'b"
  show "dist f g = 0 ⟷ f = g"
  proof
    have "⋀x. dist (f x) (g x) ≤ dist f g"
      by (rule dist_bounded)
    also assume "dist f g = 0"
    finally show "f = g"
      by (auto simp: apply_bfun_inject[symmetric])
  qed (auto simp: dist_bfun_def intro!: cSup_eq)
  show "dist f g ≤ dist f h + dist g h"
  proof (rule dist_bound)
    fix x
    have "dist (f x) (g x) ≤ dist (f x) (h x) + dist (g x) (h x)"
      by (rule dist_triangle2)
    also have "dist (f x) (h x) ≤ dist f h"
      by (rule dist_bounded)
    also have "dist (g x) (h x) ≤ dist g h"
      by (rule dist_bounded)
    finally show "dist (f x) (g x) ≤ dist f h + dist g h"
      by simp
  qed
qed (rule open_bfun_def uniformity_bfun_def)+

end


lift_definition PiC::"'a set ⇒ ('a ⇒ ('b :: metric_space) set) ⇒ ('a ⇒b 'b) set"
  is "λI X. Pi I X ∩ bfun"
  by auto

lemma mem_PiC_iff: "x ∈ PiC I X ⟷ apply_bfun x ∈ Pi I X"
  by transfer simp

lemmas mem_PiCD = mem_PiC_iff[THEN iffD1]
  and mem_PiCI = mem_PiC_iff[THEN iffD2]

lemma tendsto_bfun_uniform_limit:
  fixes f::"'i ⇒ 'a ⇒b ('b :: metric_space)"
  assumes "(f ⤏ l) F"
  shows "uniform_limit UNIV f l F"
proof (rule uniform_limitI)
  fix e::real assume "e > 0"
  from tendstoD[OF assms this] have "∀F x in F. dist (f x) l < e" .
  then show "∀F n in F. ∀x∈UNIV. dist ((f n) x) (l x) < e"
    by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt)
qed

lemma uniform_limit_tendsto_bfun:
  fixes f::"'i ⇒ 'a ⇒b ('b :: metric_space)"
    and l::"'a ⇒b 'b"
  assumes "uniform_limit UNIV f l F"
  shows "(f ⤏ l) F"
proof (rule tendstoI)
  fix e::real assume "e > 0"
  then have "e / 2 > 0" by simp
  from uniform_limitD[OF assms this]
  have "∀F i in F. ∀x. dist (f i x) (l x) < e / 2" by simp
  then have "∀F x in F. dist (f x) l ≤ e / 2"
    by eventually_elim (blast intro: dist_bound less_imp_le)
  then show "∀F x in F. dist (f x) l < e"
    by eventually_elim (use ‹0 < e› in auto)
qed

subsection✐‹tag unimportant› ‹Supremum Norm›

instantiation✐‹tag unimportant› bfun :: (type, real_normed_vector) real_vector
begin

lemma uminus_cont: "f ∈ bfun ⟹ (λx. - f x) ∈ bfun" for f::"'a ⇒ 'b"
  by (auto simp: bfun_def)

lemma plus_cont: "f ∈ bfun ⟹ g ∈ bfun ⟹ (λx. f x + g x) ∈ bfun" for f g::"'a ⇒ 'b"
  by (auto simp: bfun_def bounded_plus_comp)

lemma minus_cont: "f ∈ bfun ⟹ g ∈ bfun ⟹ (λx. f x - g x) ∈ bfun" for f g::"'a ⇒ 'b"
  by (auto simp: bfun_def bounded_minus_comp)

lemma scaleR_cont: "f ∈ bfun ⟹ (λx. a *R f x) ∈ bfun" for f :: "'a ⇒ 'b"
  by (auto simp: bfun_def bounded_scaleR_comp)

lemma bfun_normI[intro]: "(⋀x. norm (f x) ≤ b) ⟹ f ∈ bfun"
  by (auto simp: bfun_def intro: boundedI)

lift_definition uminus_bfun::"('a ⇒b 'b) ⇒ ('a ⇒b 'b)" is "λf x. - f x"
  by (rule uminus_cont)

lift_definition plus_bfun::"('a ⇒b 'b) ⇒ ('a ⇒b 'b) ⇒ 'a ⇒b 'b"  is "λf g x. f x + g x"
  by (rule plus_cont)

lift_definition minus_bfun::"('a ⇒b 'b) ⇒ ('a ⇒b 'b) ⇒ 'a ⇒b 'b"  is "λf g x. f x - g x"
  by (rule minus_cont)

lift_definition zero_bfun::"'a ⇒b 'b" is "λ_. 0"
  by (rule const_bfun)

lemma const_bfun_0_eq_0[simp]: "const_bfun 0 = 0"
  by transfer simp

lift_definition scaleR_bfun::"real ⇒ ('a ⇒b 'b) ⇒ 'a ⇒b 'b"  is "λr g x. r *R g x"
  by (rule scaleR_cont)

lemmas [simp] =
  const_bfun.rep_eq
  uminus_bfun.rep_eq
  plus_bfun.rep_eq
  minus_bfun.rep_eq
  zero_bfun.rep_eq
  scaleR_bfun.rep_eq

instance
  by standard (auto simp: algebra_simps)
end

lemma scaleR_cont': "f ∈ bfun ⟹ (λx. a * f x) ∈ bfun" for f :: "'a ⇒ real"
  using scaleR_cont[of f a] by auto

lemma bfun_norm_le_SUP_norm:
  "f ∈ bfun ⟹ norm (f x) ≤ (SUP x. norm (f x))"
  by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bfun_def bounded_norm_comp)


instantiation✐‹tag unimportant› bfun :: (type, real_normed_vector) real_normed_vector
begin

definition norm_bfun :: "('a, 'b) bfun ⇒ real"
  where "norm_bfun f = dist f 0"

definition "sgn (f::('a,'b) bfun) = f /R norm f"

instance
proof
  fix a :: real
  fix f g :: "('a, 'b) bfun"
  show "dist f g = norm (f - g)"
    unfolding norm_bfun_def
    by transfer (simp add: dist_norm)
  show "norm (f + g) ≤ norm f + norm g"
    unfolding norm_bfun_def
    by transfer
      (auto intro!: cSUP_least norm_triangle_le add_mono bfun_norm_le_SUP_norm simp: dist_norm)
  show "norm (a *R f) = ¦a¦ * norm f"
    unfolding norm_bfun_def dist_bfun.rep_eq
    by (subst continuous_at_Sup_mono[of "λx. ¦a¦ * x"]) 
      (fastforce intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above 
        simp: bounded_norm_comp image_comp)+
qed (auto simp: norm_bfun_def sgn_bfun_def)
end

lemma norm_bfun_def': "norm f = (⨆x. norm ((f :: 'a ⇒b 'b :: real_normed_vector) x))"
  by(subst norm_conv_dist, simp add: dist_bfun.rep_eq)

lemma norm_le_norm_bfun: "norm (apply_bfun f x) ≤ norm f"
  by (simp add: apply_bfun bfun_norm_le_SUP_norm norm_bfun_def dist_bfun_def)

lemma abs_le_norm_bfun: "abs (apply_bfun f x) ≤ norm f"
  by (subst real_norm_def[symmetric]) (rule norm_le_norm_bfun)

lemma le_norm_bfun: "apply_bfun f x ≤ norm f"
  using abs_ge_self abs_le_norm_bfun
  by (rule order.trans)

subsection ‹Complete Space›

lemma tendsto_add: "P ⇢ (L :: 'a :: real_normed_vector) ⟹ (λn. P n + c) ⇢ L + c"
  by (intro tendsto_intros)

lemma lim_add: "convergent P ⟹ lim (λn. P n + (c :: 'a ::real_normed_vector)) = lim P + c"
  by (auto intro: limI dest: Bounded_Functions.tendsto_add simp add: convergent_LIMSEQ_iff)

lemma complete_bfun: 
  assumes cauchy_f: "Cauchy (f :: nat ⇒ ('a,  'b :: {complete_space, real_normed_vector}) bfun)"
  shows "convergent f"
proof -
  let ?f = "λx. lim (λn. f n x)"

  from cauchy_f have cauchy_fx: "Cauchy (λn. f n x)" for x
    by(fastforce intro: dist_fun_lt_imp_dist_val_lt CauchyI' dest: metric_CauchyD)+

  hence conv_fx: "convergent (λn. f n x)" for x
    by(auto intro: Cauchy_convergent)

  have lim_f_bfun: "?f ∈ bfun"
  proof -
    have "∃b. ∀x. norm (lim (λn. f n x)) ≤ b"
    proof -
      obtain N b where dist_N: "dist (f n x) (f m x) < b" if "n ≥ N" " m ≥ N" for x m n
        using metric_CauchyD[OF cauchy_f zero_less_numeral]  dist_fun_lt_imp_dist_val_lt
        by metis
      have aux: "norm (lim (λn. f n x)) ≤ b + norm (f N x)" for x
      proof-
        from conv_fx[unfolded convergent_LIMSEQ_iff]
        have tendsto_f_N: "(λn. f (n + N) x) ⇢ ?f x"
          by (auto dest: LIMSEQ_ignore_initial_segment)
        hence tendsto_f_dist: "(λn. dist (f (n + N) x) (f N x)) ⇢ dist (?f x) (f N x)"
          by (auto intro: tendsto_intros)
        have "dist (f (n + N) x) (f N x) ≤ b" for n
          by (auto intro!: less_imp_le simp: dist_N)
        hence "dist (?f x) (f N x) ≤ b"
          using lim_le[OF convergentI[OF tendsto_f_dist]]
          by (auto simp: limI[OF tendsto_f_dist, symmetric])
        thus "norm (?f x) ≤ b + norm (f N x)"
          using norm_triangle_ineq2 order_trans
          by (fastforce simp: dist_norm)
      qed
      show ?thesis
        by (auto intro!: exI[of _ "b + norm (f N)"] order.trans[OF aux] norm_le_norm_bfun)
    qed
    thus ?thesis
      by (auto intro: boundedI simp: bfun_def)
  qed

  hence bfun_lim_f_inv: "apply_bfun (Bfun ?f) = ?f"
    using bfun.Bfun_inverse by blast

  have "f ⇢ Bfun ?f"
  proof -
    have "⋀e. e > 0 ⟹ ∃N. ∀n ≥ N. dist (Bfun ?f) (f n) < e"
    proof -
      fix e :: real
      assume "e > 0"
      hence "∃N. ∀n ≥ N. ∀m ≥ N. dist (f n) (f m) < 0.5 * e" (is "∃N. ∀n ≥ N. ∀m ≥ N. ?P n m N e")
        by(force intro!: metric_CauchyD[OF cauchy_f])
      then obtain N where dist_N: "?P n m N e" if "n ≥ N" "m ≥ N" for n m
        by auto
      have "∀n x. dist (?f x) (f (n + N) x) ≤ 0.5 * e"
      proof safe
        fix n x
        have "(λm. f m x) ⇢ ?f x"
          using conv_fx convergent_LIMSEQ_iff
          by blast
        hence tendsto_f_N: "(λm. f (m + N) x) ⇢ ?f x"
          using LIMSEQ_ignore_initial_segment
          by auto
        hence tendsto_f_dist: 
          "(λm. dist (f (m + N) x) (f (n + N) x)) ⇢ dist (?f x) (f (n + N) x)"
          by (simp add: tendsto_dist)
        have "dist (f (m + N) x) (f (n + N) x) < 0.5 * e" for m
          by (fastforce intro!: dist_fun_lt_imp_dist_val_lt[OF dist_N])
        thus "dist (?f x) (f (n + N) x) ≤ 0.5 * e"
          by (fastforce intro: less_imp_le convergentI[OF tendsto_f_dist] intro!: lim_le
              simp only: limI[OF tendsto_f_dist, symmetric])
      qed
      hence "∀n. (SUP x. dist (?f x) (f (n + N) x)) ≤ 0.5 * e"
        by (fastforce intro!: cSUP_least)
      hence aux: "∀n. dist (Bfun ?f) (f (n + N)) ≤ 0.5 * e"
        unfolding dist_bfun_def
        by (simp add: bfun_lim_f_inv)
      have "0.5 * e < e"  by (simp add: ‹0 < e›)
      hence "∀n. dist (Bfun ?f) (f (n + N)) < e"
        using aux le_less_trans by blast
      thus "∃N. ∀n≥N. dist (Bfun ?f) (f n) < e"
        by (metis add.commute less_eqE)
    qed
    thus ?thesis
      by (simp add: dist_commute metric_LIMSEQ_I)
  qed
  thus "convergent f"
    unfolding convergent_def 
    by blast
qed

lemma norm_bound:
  fixes f :: "('a, 'b::real_normed_vector) bfun"
  assumes "⋀x. norm (apply_bfun f x) ≤ b"
  shows "norm f ≤ b"
  using dist_bound[of f 0 b] assms
  by (simp add: dist_norm)

lemma bfun_bounded_norm_range: "bounded (range (λs. norm (apply_bfun v s)))"
proof -
  obtain b where "∀s. norm (v s) ≤ b"
    using norm_le_norm_bfun
    by fast
  thus ?thesis
    by (simp add: bounded_norm_comp)
qed

instance bfun :: (type, banach) banach
  by standard (auto simp: complete_bfun)

lemma bfun_prob_space_integrable: 
  assumes "prob_space S" "v ∈ borel_measurable S" 
  assumes "(v :: 'a ⇒ 'b :: {second_countable_topology, banach}) ∈ bfun" 
  shows "integrable S v"
  using prob_space.finite_measure norm_le_norm_bfun[of "Bfun v"] Bfun_inverse[OF assms(3)] assms
  by (auto intro: finite_measure.integrable_const_bound)

lemma bfun_integral_bound: 
  assumes "(v :: 'a ⇒ 'c :: {euclidean_space}) ∈ bfun"
  shows "(λS. ∫x. v x ∂(S :: 'a pmf)) ∈ bfun"
proof -
  obtain b where bH: "∀x. norm (v x) ≤ b"
    using bfun_norm_le_SUP_norm assms by fast
  have "(∫x. norm (v x) ∂S) ≤ b" for S :: "'a pmf"
    using ‹v ∈ bfun› bfun_def bounded_norm_comp bH bfun_prob_space_integrable
    by (fastforce intro!: prob_space.integral_le_const prob_space_measure_pmf simp: bfun_def)
  hence "∀S :: 'a pmf. norm (∫x. (v x) ∂S) ≤ b"
    using integral_norm_bound order_trans by blast
  thus ?thesis
    unfolding bfun_def 
    by (auto intro: boundedI)
qed

lemma scale_bfun[intro!]: "f ∈ bfun ⟹ (λx. (k::real) * f x) ∈ bfun"
  using scaleR_cont[of f k] by auto

lemma bfun_spec[intro]: "f ∈ bfun ⟹ (λx. f (g x)) ∈ bfun"
  unfolding bfun_def bounded_def by auto

lemma apply_bfun_bfun[simp]: "apply_bfun f ∈ bfun"
  using apply_bfun .

lemma bfun_integral_bound'[intro]: "(v :: 'a ⇒ 'c :: {euclidean_space}) ∈ bfun ⟹
      (λS. ∫x. v x ∂((F S) :: 'a pmf)) ∈ bfun"
  using bfun_integral_bound
  by (subst bfun_spec[of _ F]) auto

lift_definition bfun_comp :: "('a ⇒ 'b) ⇒ ('b ⇒b 'c::metric_space) ⇒ ('a ⇒b 'c)" is
  "λg bf x. bf (g x)"
  by auto


subsection ‹Order Instance›

class ordered_real_normed_vector = real_normed_vector + ordered_real_vector

instance real :: ordered_real_normed_vector 
  by standard

instantiation bfun :: (_,  ordered_real_normed_vector) ordered_real_normed_vector begin

definition "less_eq_bfun f g ≡ ∀x. apply_bfun f x ≤ apply_bfun g x"
definition "less_bfun f g ≡ ∀x. apply_bfun f x ≤ apply_bfun g x ∧ (∃y. f y < g y)"

instance
proof (standard, goal_cases)
  case (1 x y)
  then show ?case
    by (auto dest: leD simp add: less_bfun_def less_eq_bfun_def)
      (metis order.not_eq_order_implies_strict)
qed (auto intro: order_trans antisym dest: leD not_le_imp_less 
    simp: less_eq_bfun_def less_bfun_def eq_iff scaleR_left_mono scaleR_right_mono)
end

lemma less_eq_bfunI[intro]: "(⋀x. apply_bfun f x ≤ apply_bfun g x) ⟹ f ≤ g"
  unfolding less_eq_bfun_def
  by auto

lemma less_eq_bfunD[dest]: "f ≤ g ⟹ (⋀x. apply_bfun f x ≤ apply_bfun g x)"
  unfolding less_eq_bfun_def
  by auto

subsection ‹Miscellaneous›
instantiation bfun :: (type, one) one begin

lift_definition one_bfun :: "'s ⇒b real" is "λx. 1"
  using const_bfun .

instance
  by standard
end

declare one_bfun.rep_eq [simp]

lemma apply_bfun_one [simp]: "apply_bfun (1 :: _ ⇒b real) x = 1"
  using one_bfun.rep_eq
  by auto

lemma norm_bfun_one[simp]: "norm (1 :: 'a ⇒b real) = 1"
  unfolding norm_bfun_def' by auto


lemma range_bfunI[intro]: "bounded (range f) ⟹ f ∈ bfun"
  by (simp add: bfun_def)

lemma finite_bfun[simp]: "(λ(i::_::finite). f i) ∈ bfun"
  by (meson finite finite_imageI finite_imp_bounded range_bfunI)

lemma bounded_apply_bfun':
  assumes "bounded ((F :: 'c ⇒ 'd ⇒b 'b::real_normed_vector) ` S)"
  shows "bounded ((λb. (F b) x) ` S)"
proof -
  obtain b where "∀x∈S. norm (F x) ≤ b"
    by (meson assms bounded_pos image_eqI)
  thus "bounded ((λb. (F b) x) ` S)"
    by (fastforce intro: norm_le_norm_bfun dual_order.trans boundedI[of _ b])
qed


lemma bfun_tendsto_apply_bfun:
  assumes h: "(F :: (nat ⇒ 'a ⇒b real)) ⇢ (y :: 'a ⇒b real)"
  shows "(λn. F n x) ⇢ y x"
proof -
  have aux: "(λn. dist (F n) y) ⇢ 0"
    using h
    using tendsto_dist_iff by blast
  have "⋀n. dist (F n x) (y x) ≤ dist (F n) y"
    unfolding dist_bfun_def
    using Bounded_Continuous_Function.bounded_dist_le_SUP_dist by fastforce
  hence "⋀n. norm (dist (F n x) (y x)) ≤ norm(dist (F n) y)"
    by auto
  hence "(λn. dist (F n x) (y x)) ⇢ 0"
    by (subst Lim_transform_bound[OF _ aux]) auto
  thus ?thesis  
    using tendsto_dist_iff by blast
qed

subsection ‹Bounded Functions and Vectors›
lemma vec_bfun[simp, intro]: "($) x ∈ bfun"
  using finite_bfun.

lemma norm_bfun_le_norm_vec: "norm (bfun.Bfun (($) (x :: real^'c :: finite))) ≤ norm x"
proof -
  have "norm (bfun.Bfun (($) (x :: real^'c :: finite))) ≤ (⨆xa. ¦x $ xa¦)"
    unfolding norm_bfun_def dist_bfun_def
    by (auto simp: Bfun_inverse)
  also have "… ≤ norm x"
    using component_le_norm_cart
    by (auto intro: cSUP_least)
  finally show ?thesis 
    by auto
qed

lemma bounded_linear_bfun_nth: "bounded_linear f ⟹ bounded_linear (λv. bfun.Bfun (($) (f v)))"
  using order_trans[OF Finite_Cartesian_Product.norm_nth_le onorm, of f]
  by (auto simp: Bfun_inverse mult.commute linear_simps dist_bfun_def norm_bfun_def
      intro!: bounded_linear_intro cSup_least)

lemma norm_vec_le_norm_bfun: 
  "norm (vec_lambda (apply_bfun (x :: 'd::finite ⇒b real))) ≤ norm x * card (UNIV :: 'd set)"
proof -
  have "norm (vec_lambda (apply_bfun x)) ≤ (∑ i ∈ UNIV . ¦(apply_bfun x i)¦)"
    using L2_set_le_sum_abs
    unfolding norm_vec_def L2_set_def
    by auto
  also have "… ≤ (card (UNIV :: 'd set) * (⨆xa. ¦apply_bfun x xa¦))"
    by (auto intro!: sum_bounded_above cSup_upper)
  finally show ?thesis
    by (simp add: norm_bfun_def dist_bfun_def mult.commute)
qed

end
dy>

Theory Blinfun_Util

(* Author: Maximilian Schäffeler *)
section ‹Bounded Linear Functions›
theory Blinfun_Util
  imports 
    "HOL-Analysis.Bounded_Linear_Function" 
    Bounded_Functions
begin

subsection ‹Composition›

lemma blinfun_compose_id[simp]:
  "id_blinfun oL f = f"
  "f oL id_blinfun = f"
  by (auto intro!: blinfun_eqI)

lemma blinfun_compose_assoc: "F oL G oL H = F oL (G oL H)"
  using blinfun_apply_inject by fastforce

lemma blinfun_compose_diff_right: "f oL (g - h) = (f oL g) - (f oL h)"
  by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)

subsection ‹Power›

overloading
  blinfunpow ≡ "compow :: nat ⇒ ('a::real_normed_vector ⇒L 'a) ⇒ ('a ⇒L 'a)"
begin

primrec blinfunpow :: "nat ⇒ ('a::real_normed_vector ⇒L 'a) ⇒ ('a ⇒L 'a)"
  where
    "blinfunpow 0 f = id_blinfun"
  | "blinfunpow (Suc n) f = f oL blinfunpow n f"

end

lemma bounded_pow_blinfun[intro]: 
  assumes "bounded (range (F::nat ⇒ 'a::real_normed_vector ⇒L 'a))"
  shows "bounded (range (λt. (F t)^^(Suc n)))"
  using assms proof -
  assume "bounded (range F)"
  then obtain b where bh: "⋀x. norm (F x) ≤ b"
    by (auto simp: bounded_iff)
  hence "norm ((F x)^^(Suc n)) ≤ b^(Suc n)" for x
    using bh
    by (induction n) (auto intro!: order.trans[OF norm_blinfun_compose] simp: mult_mono')
  thus ?thesis
    by (auto intro!: boundedI)
qed

lemma blincomp_scaleR_right: "(a *R (F :: 'a :: real_normed_vector ⇒L 'a)) ^^ t = a^t *R F^^t"
  by (induction t) (auto intro: blinfun_eqI simp: blinfun.scaleR_left blinfun.scaleR_right)
lemma summable_inv_Q:
  fixes Q :: "'a :: banach ⇒L 'a"
  assumes onorm_le: "norm (id_blinfun - Q) < 1"
  shows "summable (λn. (id_blinfun - Q)^^n)"
  using onorm_le norm_blinfun_compose 
  by (force intro!: summable_ratio_test)

lemma blinfunpow_assoc: "(F::'a::real_normed_vector ⇒L 'a) ^^ (Suc n) =(F ^^n) oL F"
  by (induction n) (auto simp: blinfun_compose_assoc[symmetric]) 

lemma norm_blinfunpow_le: "norm ((f :: 'b :: real_normed_vector ⇒L 'b) ^^ n) ≤ norm f ^ n"
  by (induction n) (auto simp: norm_blinfun_id_le intro!: order.trans[OF norm_blinfun_compose] mult_left_mono)

lemma blinfunpow_nonneg: 
  assumes "⋀v. 0 ≤ v ⟹ 0 ≤ blinfun_apply (f :: ('b :: {ord, real_normed_vector} ⇒L 'b)) v"
  shows "0 ≤ v ⟹ 0 ≤ (f^^n) v"
  by(induction n) (auto simp: assms)

lemma blinfunpow_mono: 
  assumes "⋀u v. u ≤ v ⟹ (f :: 'b :: {ord, real_normed_vector} ⇒L 'b) u ≤ f v"
  shows "u ≤ v ⟹ (f^^n) u ≤ (f^^n) v"
  by (induction n) (auto simp: assms)  

lemma banach_blinfun:
  fixes C :: "'b :: {real_normed_vector, complete_space} ⇒L 'b"
  assumes "norm C < 1"
  shows "∃!v. C v = v" "⋀v. (λn. (C ^^ n) v) ⇢ (THE v. C v = v)"
  using assms
proof -
  obtain v where "C v = v" "∀v'. C v' = v' ⟶ v' = v"
    using assms banach_fix_type[of "norm C" "blinfun_apply C"]
    by (metis blinfun.zero_right less_irrefl mult.left_neutral mult_less_le_imp_less 
        norm_blinfun norm_conv_dist norm_ge_zero zero_less_dist_iff)
  obtain l where "(∀v u. norm (C (v - u)) ≤ l * dist v u)" "0 ≤ l" "l < 1"
    by (metis assms dist_norm norm_blinfun norm_imp_pos_and_ge)
  hence 1: "dist (C v) (C u) ≤ l * dist v u" for v u
    by (simp add: blinfun.diff_right dist_norm)
  have 2: "dist ((C ^^ n) v0) v ≤ l ^ n * dist v0 v" for n v0
    using ‹0 ≤ l› 
    by (induction n) (auto simp: mult.assoc 
        intro!: mult_mono' order.trans[OF 1[of _ v , unfolded ‹C v = v›]])
  have "(λn. l ^ n) ⇢ 0"
    by (simp add: LIMSEQ_realpow_zero ‹0 ≤ l› ‹l < 1›)
  hence k: "⋀v0. (λn. l ^ n * dist v0 v) ⇢ 0"
    by (auto simp add: tendsto_mult_left_zero)
  have "(λn. dist ((C ^^ n) v0) v) ⇢ 0" for v0
    using k 2 order_trans abs_ge_self
    by (subst Limits.tendsto_0_le[where ?K = 1, where ?f = "(λn. l ^ n * dist v0 v)"])
      (fastforce intro: eventuallyI)+
  hence "⋀v0. (λn. (C ^^ n) v0) ⇢ v"
    using tendsto_dist_iff
    by blast
  thus "(λn. (C ^^ n) v0) ⇢ (THE v. C v = v)" for v0
    using theI'[of "λx. C x = x"] ‹C v = v› ‹∀v'. C v' = v' ⟶ v' = v› 
    by blast
next
  show "norm C < 1 ⟹ ∃!v. blinfun_apply C v = v"
    by (auto intro!: banach_fix_type[OF _ assms] 
        simp: dist_norm norm_blinfun blinfun.diff_right[symmetric])
qed

subsection ‹Geometric Sum›

lemma inv_one_sub_Q:
  fixes Q :: "'a :: banach ⇒L 'a"
  assumes onorm_le: "norm (id_blinfun - Q) < 1"
  shows "(Q oL (∑i. (id_blinfun - Q)^^i)) = id_blinfun" 
    and "(∑i. (id_blinfun - Q)^^i) oL Q = id_blinfun"
proof -
  obtain b where bh: "b < 1"  "norm (id_blinfun - Q) < b"
    using onorm_le dense 
    by blast
  have "0 < b" 
    using le_less_trans[OF norm_ge_zero bh(2)] .
  have norm_le_aux: "norm ((id_blinfun - Q)^^Suc n) ≤ b^(Suc n)" for n
  proof (induction n)
    case 0
    thus ?case 
      using bh 
      by simp
  next
    case (Suc n)
    thus ?case
    proof -
      have "norm ((id_blinfun - Q) ^^ Suc (Suc n)) ≤ norm (id_blinfun - Q) * norm((id_blinfun - Q) ^^ Suc n)"
        using norm_blinfun_compose 
        by auto
      thus ?thesis
        using Suc.IH ‹0 < b› bh order.trans
        by (fastforce simp: mult_mono')
    qed 
  qed
  have "(Q oL (∑i≤n. (id_blinfun - Q)^^i)) = (id_blinfun - (id_blinfun - Q)^^(Suc n))" for n
    by (induction n)  (auto simp: bounded_bilinear.diff_left bounded_bilinear.add_right 
        bounded_bilinear_blinfun_compose)
  hence "⋀n. norm (id_blinfun - (Q oL (∑i≤n. (id_blinfun - Q)^^i))) ≤ b^Suc n"
    using norm_le_aux 
    by auto
  hence l2: "(λn. (id_blinfun - (Q oL (∑i≤n. (id_blinfun - Q)^^i)))) ⇢ 0"
    using ‹0 < b› bh 
    by (subst Lim_transform_bound[where g="λn. b^Suc n"]) (auto intro!: tendsto_eq_intros)
  have "summable (λn. (id_blinfun - Q)^^n)"
    using onorm_le norm_blinfun_compose 
    by (force intro!: summable_ratio_test)
  hence "(λn. ∑i≤n.  (id_blinfun - Q)^^i) ⇢ (∑i. (id_blinfun - Q)^^i)"
    using summable_LIMSEQ' 
    by blast
  hence "(λn. Q oL (∑i≤n. (id_blinfun - Q)^^i)) ⇢ (Q oL (∑i. (id_blinfun - Q)^^i))"
    using bounded_bilinear_blinfun_compose 
    by (subst Limits.bounded_bilinear.tendsto[where prod = "(oL)"]) auto   
  hence "(λn. id_blinfun - (Q oL (∑i≤n. (id_blinfun - Q)^^i))) ⇢ 
    id_blinfun - (Q oL (∑i. (id_blinfun - Q)^^i))"
    by (subst Limits.tendsto_diff) auto
  thus "(Q oL (∑i. (id_blinfun - Q)^^i)) = id_blinfun"
    using LIMSEQ_unique l2 by fastforce

  have "((∑i≤n. (id_blinfun - Q)^^i) oL Q) = (id_blinfun - (id_blinfun - Q)^^(Suc n))" for n
  proof (induction n)
    case (Suc n)
    have "sum ((^^) (id_blinfun - Q)) {..Suc n} oL Q = 
        (sum ((^^) (id_blinfun - Q)) {..n} oL Q) + ((id_blinfun - Q) ^^Suc n oL Q)"
      by (simp add: bounded_bilinear.add_left bounded_bilinear_blinfun_compose)
    also have "… = id_blinfun - (((id_blinfun - Q)^^(Suc n) oL id_blinfun) - 
        ((id_blinfun - Q) ^^Suc n oL Q))"
      using Suc.IH 
      by auto
    also have "… = id_blinfun - (((id_blinfun - Q)^^(Suc n) oL (id_blinfun - Q)))"
      by (auto intro!: blinfun_eqI simp: blinfun.diff_right blinfun.diff_left blinfun.minus_left)
    also have "… = id_blinfun - (((id_blinfun - Q)^^(Suc (Suc n))))"
      using blinfunpow_assoc
      by metis
    finally show ?case
      by auto
  qed simp
  hence "⋀n. norm (id_blinfun - ((∑i≤n. (id_blinfun - Q)^^i) oL Q)) ≤ b^Suc n"
    using norm_le_aux by auto
  hence l2: "(λn. id_blinfun - ((∑i≤n. (id_blinfun - Q)^^i) oL Q)) ⇢ 0"
    using ‹0 < b› bh 
    by (subst Lim_transform_bound[where g="λn. b^Suc n"]) (auto intro!: tendsto_eq_intros)
  have "summable (λn. (id_blinfun - Q)^^n)"
    using local.onorm_le norm_blinfun_compose 
    by (force intro!: summable_ratio_test)
  hence "(λn. ∑i≤n.  (id_blinfun - Q)^^i) ⇢ (∑i. (id_blinfun - Q)^^i)"
    using summable_LIMSEQ' by blast
  hence "(λn. (∑i≤n. (id_blinfun - Q)^^i) oL Q) ⇢ ((∑i. (id_blinfun - Q)^^i) oL Q)"
    using bounded_bilinear_blinfun_compose 
    by (subst Limits.bounded_bilinear.tendsto[where prod = "(oL)"]) auto   
  hence "(λn. id_blinfun - ((∑i≤n. (id_blinfun - Q)^^i) oL Q)) ⇢ 
    id_blinfun - ((∑i. (id_blinfun - Q)^^i) oL Q)"
    by (subst Limits.tendsto_diff) auto
  thus "((∑i. (id_blinfun - Q)^^i) oL Q) = id_blinfun"
    using LIMSEQ_unique l2 by fastforce
qed

lemma inv_norm_le:
  fixes Q :: "'a :: banach ⇒L 'a"
  assumes "norm Q  < 1"
  shows "(id_blinfun-Q) oL (∑i. Q^^i) = id_blinfun"
    "(∑i. Q^^i) oL (id_blinfun-Q) = id_blinfun"
  using inv_one_sub_Q[of "id_blinfun - Q"] assms
  by auto

lemma inv_norm_le':
  fixes Q :: "'a :: banach ⇒L 'a"
  assumes "norm Q  < 1"
  shows "(id_blinfun-Q) ((∑i. Q^^i) x) = x"
    "(∑i. Q^^i) ((id_blinfun-Q) x) = x"
  using inv_norm_le assms  
  by (auto simp del: blinfun_apply_blinfun_compose 
      simp: inv_norm_le blinfun_apply_blinfun_compose[symmetric])

subsection ‹Inverses›

definition "is_inverseL X Y ⟷ X oL Y = id_blinfun ∧ Y oL X = id_blinfun"

abbreviation "invertibleL X ≡ ∃X'. is_inverseL X X'"

lemma is_inverseL_I[intro]:
  assumes "X oL Y = id_blinfun" "Y oL X = id_blinfun"
  shows "is_inverseL X Y"
  using assms
  unfolding is_inverseL_def
  by auto

lemma is_inverseL_D[dest]:
  assumes "is_inverseL X Y"
  shows "X oL Y = id_blinfun" "Y oL X = id_blinfun"
  using assms
  unfolding is_inverseL_def
  by auto

lemma invertibleL_D[dest]:
  assumes "invertibleL f"
  obtains g where "f oL g = id_blinfun" "g oL f = id_blinfun"
  using assms
  by auto

lemma invertibleL_I[intro]:
  assumes "f oL g = id_blinfun" "g oL f = id_blinfun"
  shows "invertibleL f"
  using assms
  by auto

lemma is_inverseL_comm: "is_inverseL X Y ⟷ is_inverseL Y X"
  by auto

lemma is_inverseL_unique: "is_inverseL f g ⟹ is_inverseL f h ⟹ g = h"
  unfolding is_inverseL_def
  using blinfun_compose_assoc  blinfun_compose_id(1)
  by metis

lemma is_inverseL_ex1: "is_inverseL f g ⟹ ∃!h. is_inverseL f h"
  using is_inverseL_unique
  by auto

lemma is_inverseL_ex1': "∃x. is_inverseL f x ⟹ ∃!x. is_inverseL f x"
  using is_inverseL_ex1
  by auto

definition "invL f = (THE g. is_inverseL f g)"

lemma invL_eq:
  assumes "is_inverseL f g" 
  shows "invL f = g"
  unfolding invL_def
  using assms is_inverseL_ex1
  by (auto intro!: the_equality)

lemma invL_I:
  assumes "f oL g = id_blinfun" "g oL f = id_blinfun" 
  shows "g = invL f"
  using assms invL_eq
  unfolding is_inverseL_def
  by auto

lemma inv_app1 [simp]: "invertibleL X ⟹ (invL X) oL X = id_blinfun"
  using is_inverseL_ex1' invL_eq 
  by blast

lemma inv_app2[simp]: "invertibleL X ⟹ X oL (invL X)  = id_blinfun"
  using is_inverseL_ex1' invL_eq 
  by blast

lemma inv_app1'[simp]: "invertibleL X ⟹ invL X (X v) = v"
  using inv_app1 blinfun_apply_blinfun_compose id_blinfun.rep_eq
  by metis

lemma inv_app2'[simp]: "invertibleL X ⟹ X (invL X v) = v"
  using inv_app2 blinfun_apply_blinfun_compose id_blinfun.rep_eq
  by metis

lemma [simp]: "invertibleL X ⟹ invL (invL X) = X"
  by (metis invL_eq is_inverseL_comm)

lemma invL_cancel_iff:
  assumes "invertibleL f"
  shows "f x = y ⟷ x = invL f y"
  by (auto simp add: assms)

lemma invertibleL_inf_sum:
  assumes "norm (X :: 'b :: banach ⇒L 'b) < 1"
  shows "invertibleL (id_blinfun - X)"
  using Blinfun_Util.inv_norm_le[OF assms] assms
  by blast

lemma invL_inf_sum:
  fixes X :: "'b :: banach ⇒L _"
  assumes "norm X < 1"
  shows "invL (id_blinfun - X) = (∑i. X ^^ i)"
  using Blinfun_Util.inv_norm_le[OF assms] assms
  by (auto simp: invL_I[symmetric])

lemma is_inverseL_compose:
  assumes "invertibleL f" "invertibleL g" 
  shows "is_inverseL (f oL g) (invL g oL invL f)"
  by (auto intro!: blinfun_eqI is_inverseL_I[of _ "invL g oL invL f"]
      simp: inv_app2'[OF assms(1)] inv_app2'[OF assms(2)] inv_app1'[OF assms(1)] inv_app1'[OF assms(2)])

lemma invertibleL_compose: "invertibleL f ⟹ invertibleL g ⟹ invertibleL (f oL g)"
  using is_inverseL_compose 
  by blast

lemma invL_compose: 
  assumes "invertibleL f" "invertibleL g" 
  shows"invL (f oL g) = (invL g) oL (invL f)"
  using assms invL_eq is_inverseL_compose
  by blast

lemma invL_id_blinfun[simp]: "invL id_blinfun = id_blinfun"
  by (metis blinfun_compose_id(2) invL_I)


subsection ‹Norm›
lemma bounded_range_subset: 
  "bounded (range f :: real set) ⟹ bounded (f ` X')"
  by (auto simp: bounded_iff)

lemma bounded_const: "bounded ((λ_. x) ` X)"
  by (meson finite_imp_bounded finite.emptyI finite_insert finite_subset image_subset_iff insert_iff)

lift_definition bfun_pos :: "('d ⇒b real) ⇒ ('d ⇒b real)" is "λf i. if f i < 0 then -f i else f i"
  using bounded_const bounded_range_subset by (auto simp: bfun_def)

lemma bfun_pos_zero[simp]: "bfun_pos f = 0 ⟷ f = 0"
  by (auto intro!: bfun_eqI simp: bfun_pos.rep_eq split: if_splits)

lift_definition bfun_nonneg :: "('d ⇒b real) ⇒ ('d ⇒b real)" is "λf i. if f i ≤ 0 then 0 else f i"
  using bounded_const bounded_range_subset by (auto simp: bfun_def)

lemma bfun_nonneg_split: "bfun_nonneg x - bfun_nonneg (- x) = x"
  by (auto simp: bfun_nonneg.rep_eq)

lemma blinfun_split: "blinfun_apply f x = f (bfun_nonneg x) - f (bfun_nonneg (- x))"
  using bfun_nonneg_split
  by (metis blinfun.diff_right)

lemma bfun_nonneg_pos: "bfun_nonneg x + bfun_nonneg (-x) = bfun_pos x"
  by (auto simp: bfun_nonneg.rep_eq bfun_pos.rep_eq)

lemma bfun_nonneg: "0 ≤ bfun_nonneg f"
  by (auto simp: bfun_nonneg.rep_eq)

lemma bfun_pos_eq_nonneg: "bfun_pos n = bfun_nonneg n + bfun_nonneg (-n)"
  by (auto simp: bfun_pos.rep_eq bfun_nonneg.rep_eq)

lemma blinfun_mono_norm_pos:
  fixes f :: "('c ⇒b real) ⇒L ('d ⇒b real)"
  assumes "⋀v :: 'c ⇒b real. v ≥ 0 ⟹ f v ≥ 0"
  shows "norm (f n) ≤ norm (f (bfun_pos n))"
proof -
  have *: "¦f n i¦ ≤ ¦f (bfun_pos n) i¦" for i
    by (auto simp: blinfun_split[of f n] bfun_nonneg_pos[symmetric] blinfun.add_right abs_real_def)
      (metis add_nonneg_nonneg assms bfun_nonneg leD less_eq_bfun_def zero_bfun.rep_eq)+
  thus "norm (f n) ≤ norm ((f (bfun_pos n)))"
    unfolding norm_bfun_def' using *
    by (auto intro!: cSUP_mono bounded_imp_bdd_above abs_le_norm_bfun boundedI[of _ "norm ((f (bfun_pos n)))"])
qed

lemma norm_bfun_pos[simp]: "norm (bfun_pos f) = norm f"
proof -
  have "norm (bfun_pos f) = (⨆i. ¦bfun_pos f i¦)"
    by (auto simp add: norm_bfun_def')
  also have "… = (⨆i. ¦f i¦)"
    by (rule SUP_cong[OF refl]) (auto simp: bfun_pos.rep_eq)
  finally show ?thesis by (auto simp add: norm_bfun_def')
qed

lemma norm_blinfun_mono_eq_nonneg:
  fixes f :: "('c ⇒b real) ⇒L ('d ⇒b real)"
  assumes "⋀v :: 'c ⇒b real. v ≥ 0 ⟹ f v ≥ 0"
  shows "norm f = (⨆v ∈ {v. v ≥ 0}. norm (f v) / norm v)"
  unfolding norm_blinfun.rep_eq onorm_def
proof (rule antisym, rule cSUP_mono)
  have *: "norm (blinfun_apply f v) / norm v ≤ norm f" for v
    using norm_blinfun[of f]
    by (cases "v = 0") (auto simp: pos_divide_le_eq)
  thus "bdd_above ((λv. norm (f v) / norm v) ` {v. 0 ≤ v})"
    by (auto intro!: bounded_imp_bdd_above boundedI)
  show "∃m∈{v. 0 ≤ v}. norm (f n) / norm n ≤ norm (f m) / norm m" for n
    using blinfun_mono_norm_pos[OF assms]
    by (cases "norm (bfun_pos n) = 0")
      (auto intro!: frac_le exI[of _ "bfun_pos n"] simp: less_eq_bfun_def bfun_pos.rep_eq)
  show "(⨆v∈{v. 0 ≤ v}. norm (f v) / norm v) ≤ (⨆x. norm (f x) / norm x)"
    using *
    by (auto intro!: cSUP_mono bounded_imp_bdd_above boundedI)
qed auto

lemma norm_blinfun_normalized_le: "norm (blinfun_apply f v) / norm v ≤ norm f"
  by (simp add: blinfun.bounded_linear_right le_onorm norm_blinfun.rep_eq)

lemma norm_blinfun_mono_eq_nonneg':
  fixes f :: "('c ⇒b real) ⇒L ('d ⇒b real)"
  assumes "⋀v :: 'c ⇒b real. 0 ≤ v ⟹ 0 ≤ f v"
  shows "norm f = (⨆x ∈ {x. norm x = 1 ∧ x ≥ 0}. norm (f x))"
proof (subst norm_blinfun_mono_eq_nonneg[OF assms])
  show "(⨆v∈{v. 0 ≤ v}. norm (f v) / norm v) =
    (⨆x∈{x. norm x = 1 ∧ 0 ≤ x}. norm (f x))"
  proof (rule antisym, rule cSUP_mono)
    show "{v::'c ⇒b real. 0 ≤ v} ≠ {}" by auto
    show "bdd_above ((λx. norm (f x)) ` {x. norm x = 1 ∧ 0 ≤ x})"
      by (fastforce intro: order.trans[OF norm_blinfun[of f]] bounded_imp_bdd_above boundedI)
    show "∃m∈{x. norm x = 1 ∧ 0 ≤ x}. norm (f n) / norm n ≤ norm (f m)" if "n ∈ {v. 0 ≤ v}" for n
    proof (cases "norm (bfun_pos n) = 0")
      case True
      then show ?thesis by (auto intro!: exI[of _ 1])
    next
      case False
      then show ?thesis
        using that
        by (auto simp: scaleR_nonneg_nonneg blinfun.scaleR_right intro!: exI[of _ "(1/norm n) *R n"])
    qed
    show "(⨆x∈{x. norm x = 1 ∧ 0 ≤ x}. norm (f x)) ≤ (⨆v∈{v. 0 ≤ v}. norm (f v) / norm v)"
    proof (rule cSUP_mono)
      show "{x::'c ⇒b real. norm x = 1 ∧ 0 ≤ x} ≠ {}"
        by (auto intro!: exI[of _ 1])
    qed (fastforce intro!: norm_blinfun_normalized_le bounded_imp_bdd_above boundedI)+
  qed
qed auto

lemma norm_blinfun_mono_le_norm_one:
  fixes f :: "('c ⇒b real) ⇒L ('d ⇒b real)"
  assumes "⋀v :: 'c ⇒b real. v ≥ 0 ⟹ f v ≥ 0"
  assumes "norm x = 1" "0 ≤ x"
  shows "norm (f x) ≤ norm (f 1)" 
proof -
  have **: "0 ≤ 1 - x"
    using assms
    by (auto simp: less_eq_bfun_def intro: order.trans[OF le_norm_bfun])
  show ?thesis
    unfolding norm_bfun_def'
  proof (intro cSUP_mono)
    show"bdd_above (range (λx. norm (apply_bfun (blinfun_apply f 1) x)))"
      using order.trans abs_le_norm_bfun norm_blinfun
      by (fastforce intro!: bounded_imp_bdd_above boundedI)
    show "∃m∈UNIV. norm (f x n) ≤ norm (f 1 m)" for n
      using assms(1) assms(3) assms(1)[of "1 - x"] **
      unfolding less_eq_bfun_def zero_bfun.rep_eq abs_real_def
      by (auto simp: blinfun.diff_right linorder_class.not_le[symmetric])
  qed auto
qed

lemma norm_blinfun_mono_eq_one:
  fixes f :: "('c ⇒b real) ⇒L ('d ⇒b real)"
  assumes "⋀v :: 'c ⇒b real. v ≥ 0 ⟹ f v ≥ 0"
  shows "norm f = norm (f 1)"
proof -
  have "(⨆x∈{x. norm x = 1 ∧ 0 ≤ x}. norm (f x)) = norm (f 1)"
  proof (rule antisym, rule cSUP_least)
    show "{x::'c ⇒b real. norm x = 1 ∧ 0 ≤ x} ≠ {}"
      by (auto intro!: exI[of _ 1])
  next
    show "⋀x. x ∈ {x. norm x = 1 ∧ 0 ≤ x} ⟹ norm (f x) ≤ norm (f 1)"
      by (simp add: assms norm_blinfun_mono_le_norm_one)
  next
    show "norm (f 1) ≤ (⨆x∈{x. norm x = 1 ∧ 0 ≤ x}. norm (f x))"
      by (rule cSUP_upper) (fastforce intro!: bdd_aboveI2 order.trans[OF norm_blinfun])+
  qed
  thus ?thesis
    using norm_blinfun_mono_eq_nonneg'[OF assms] 
    by auto
qed

subsection ‹Miscellaneous›

lemma bounded_linear_apply_bfun: "bounded_linear (λx. apply_bfun x i)"
  using norm_le_norm_bfun
  by (fastforce intro: bounded_linear_intro[of _ 1])

lemma lim_blinfun_apply: "convergent X ⟹ (λn. blinfun_apply (X n) u) ⇢ lim X u"  
  using blinfun.bounded_bilinear_axioms
  by (auto simp: convergent_LIMSEQ_iff intro: Limits.bounded_bilinear.tendsto)

lemma bounded_apply_blinfun: 
  assumes "bounded ((F :: 'c ⇒ 'd::real_normed_vector ⇒L 'b::real_normed_vector) ` S)"
  shows "bounded ((λb. blinfun_apply (F b) x) ` S)"
proof -
  obtain b where "∀x∈S. norm (F x) ≤ b"
    by (meson ‹bounded (F ` S)› bounded_pos image_eqI)
  thus "bounded ((λb. (F b) x) ` S)"
    by (auto simp: mult_right_mono mult.commute[of _ b] 
        intro!: boundedI[of _ "norm x * b"] dual_order.trans[OF _ norm_blinfun])
qed
end

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
  by (auto; metis is_arg_max_def someI_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_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
    unfolding is_contraction_def
    using banach_fix_type 
    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 ≤