# 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)}"

"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))" .

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)"
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
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))"

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"

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)"
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
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"
qed
thus ?thesis
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

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
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"

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]:
by (auto intro!: blinfun_eqI)

using blinfun_apply_inject by fastforce

by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)

subsection â¹Powerâº

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 oâ©L 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) oâ©L 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
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"
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 oâ©L (âi. (id_blinfun - Q)^^i)) = id_blinfun"
and "(âi. (id_blinfun - Q)^^i) oâ©L 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 oâ©L (â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 oâ©L (âiâ¤n. (id_blinfun - Q)^^i))) â¤ b^Suc n"
using norm_le_aux
by auto
hence l2: "(Î»n. (id_blinfun - (Q oâ©L (â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 oâ©L (âiâ¤n. (id_blinfun - Q)^^i)) â¢ (Q oâ©L (âi. (id_blinfun - Q)^^i))"
using bounded_bilinear_blinfun_compose
by (subst Limits.bounded_bilinear.tendsto[where prod = "(oâ©L)"]) auto
hence "(Î»n. id_blinfun - (Q oâ©L (âiâ¤n. (id_blinfun - Q)^^i))) â¢
id_blinfun - (Q oâ©L (âi. (id_blinfun - Q)^^i))"
by (subst Limits.tendsto_diff) auto
thus "(Q oâ©L (âi. (id_blinfun - Q)^^i)) = id_blinfun"
using LIMSEQ_unique l2 by fastforce

have "((âiâ¤n. (id_blinfun - Q)^^i) oâ©L Q) = (id_blinfun - (id_blinfun - Q)^^(Suc n))" for n
proof (induction n)
case (Suc n)
have "sum ((^^) (id_blinfun - Q)) {..Suc n} oâ©L Q =
(sum ((^^) (id_blinfun - Q)) {..n} oâ©L Q) + ((id_blinfun - Q) ^^Suc n oâ©L Q)"
also have "â¦ = id_blinfun - (((id_blinfun - Q)^^(Suc n) oâ©L id_blinfun) -
((id_blinfun - Q) ^^Suc n oâ©L Q))"
using Suc.IH
by auto
also have "â¦ = id_blinfun - (((id_blinfun - Q)^^(Suc n) oâ©L (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) oâ©L Q)) â¤ b^Suc n"
using norm_le_aux by auto
hence l2: "(Î»n. id_blinfun - ((âiâ¤n. (id_blinfun - Q)^^i) oâ©L 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) oâ©L Q) â¢ ((âi. (id_blinfun - Q)^^i) oâ©L Q)"
using bounded_bilinear_blinfun_compose
by (subst Limits.bounded_bilinear.tendsto[where prod = "(oâ©L)"]) auto
hence "(Î»n. id_blinfun - ((âiâ¤n. (id_blinfun - Q)^^i) oâ©L Q)) â¢
id_blinfun - ((âi. (id_blinfun - Q)^^i) oâ©L Q)"
by (subst Limits.tendsto_diff) auto
thus "((âi. (id_blinfun - Q)^^i) oâ©L 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) oâ©L (âi. Q^^i) = id_blinfun"
"(âi. Q^^i) oâ©L (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âº

using assms
by auto

using assms
by auto

obtains g where "f oâ©L g = id_blinfun" "g oâ©L f = id_blinfun"
using assms
by auto

using assms
by auto

by auto

using blinfun_compose_assoc  blinfun_compose_id(1)
by metis

by auto

by auto

by (auto intro!: the_equality)

by auto

by blast

by blast

using inv_app1 blinfun_apply_blinfun_compose id_blinfun.rep_eq
by metis

using inv_app2 blinfun_apply_blinfun_compose id_blinfun.rep_eq
by metis

shows "f x = y â· x = invâ©L f y"

assumes "norm (X :: 'b :: banach ââ©L 'b) < 1"
using Blinfun_Util.inv_norm_le[OF assms] assms
by blast

fixes X :: "'b :: banach ââ©L _"
assumes "norm X < 1"
shows "invâ©L (id_blinfun - X) = (âi. X ^^ i)"
using Blinfun_Util.inv_norm_le[OF assms] assms

simp: inv_app2'[OF assms(1)] inv_app2'[OF assms(2)] inv_app1'[OF assms(1)] inv_app1'[OF assms(2)])

by blast

by blast

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:
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Â¦)"
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:
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':
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:
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:
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)"
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âº

"summable (f :: nat â 'x :: real_normed_vector) â¹ suminf f = f 0 + (ân. f (Suc n))"

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)"
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"
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)))"
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
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"
ultimately have 2: "eventually (Î»n. dist (h n) x â¤