Theory Splitting_Methods
theory Splitting_Methods
imports
Value_Iteration
Policy_Iteration
begin
section ‹Value Iteration using Splitting Methods›
subsection ‹Regular Splittings for Matrices and Bounded Linear Functions›
definition "is_splitting_blin X Q R ⟷
X = Q - R ∧ invertible⇩L Q ∧ nonneg_blinfun (inv⇩L Q) ∧ nonneg_blinfun R"
lemma is_splitting_blinD[dest]:
assumes "is_splitting_blin X Q R"
shows "X = Q - R" "invertible⇩L Q" "nonneg_blinfun (inv⇩L Q)" "nonneg_blinfun R"
using is_splitting_blin_def assms by auto
lemma is_splitting_blinI[intro]:
assumes "X = Q - R" "invertible⇩L Q" "nonneg_blinfun (inv⇩L Q)" "nonneg_blinfun R"
shows "is_splitting_blin X Q R"
using is_splitting_blin_def assms by auto
subsection ‹Splitting Methods for MDPs›
locale MDP_QR = MDP_att_ℒ A K r l
for A :: "'s::countable ⇒ 'a::countable set"
and K :: "('s × 'a) ⇒ 's pmf"
and r l +
fixes Q R :: "('s ⇒ 'a) ⇒ ('s ⇒⇩b real) ⇒⇩L ('s ⇒⇩b real)"
assumes is_splitting: "⋀d. d ∈ D⇩D ⟹ is_splitting_blin (id_blinfun - l *⇩R 𝒫⇩1 (mk_dec_det d)) (Q d) (R d)"
and QR_contraction: "(⨆d∈D⇩D. norm (inv⇩L (Q d) o⇩L R d)) < 1"
and QR_bdd: "bdd_above ((λd. norm (inv⇩L (Q d) o⇩L R d)) ` D⇩D)"
and Q_bdd: "bounded ((λd. norm (inv⇩L (Q d))) ` D⇩D)"
and arg_max_ex_split: "∃d. ∀s. is_arg_max (λd. inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d v) s) (λd. d ∈ D⇩D) d"
begin
lemma inv_Q_mono: "d ∈ D⇩D ⟹ u ≤ v ⟹ (inv⇩L (Q d)) u ≤ (inv⇩L (Q d)) v"
using is_splitting
by (auto intro!: nonneg_blinfun_mono)
lemma splitting_eq: "d ∈ D⇩D ⟹ Q d - R d = (id_blinfun - l *⇩R 𝒫⇩1 (mk_dec_det d))"
using is_splitting
by fastforce
lemma Q_nonneg: "d ∈ D⇩D ⟹ 0 ≤ v ⟹ 0 ≤ inv⇩L (Q d) v"
using is_splitting nonneg_blinfun_nonneg
by auto
lemma Q_invertible: "d ∈ D⇩D ⟹ invertible⇩L (Q d)"
using is_splitting
by auto
lemma R_nonneg: "d ∈ D⇩D ⟹ 0 ≤ v ⟹ 0 ≤ R d v"
using is_splitting_blinD[OF is_splitting]
by (fastforce simp: nonneg_blinfun_nonneg intro: nonneg_blinfun_mono)
lemma R_mono: "d ∈ D⇩D ⟹ u ≤ v ⟹ (R d) u ≤ (R d) v"
using R_nonneg[of d "v - u"]
by (auto simp: blinfun.bilinear_simps)
lemma QR_nonneg: "d ∈ D⇩D ⟹ 0 ≤ v ⟹ 0 ≤ (inv⇩L (Q d) o⇩L R d) v"
by (simp add: Q_nonneg R_nonneg)
lemma QR_mono: "d ∈ D⇩D ⟹ u ≤ v ⟹ (inv⇩L (Q d) o⇩L R d) u ≤ (inv⇩L (Q d) o⇩L R d) v"
using QR_nonneg[of d "v - u"]
by (auto simp: blinfun.bilinear_simps)
lemma norm_QR_less_one: "d ∈ D⇩D ⟹ norm (inv⇩L (Q d) o⇩L R d) < 1"
using QR_bdd
by (auto intro: cSUP_lessD[OF _ QR_contraction])
lemma splitting: "d ∈ D⇩D ⟹ id_blinfun - l *⇩R 𝒫⇩1 (mk_dec_det d) = Q d - R d"
using is_splitting
by auto
subsection ‹Discount Factor @{term "QR_disc"}›
abbreviation "QR_disc ≡ (⨆d ∈ D⇩D. norm (inv⇩L (Q d) o⇩L R d))"
lemma QR_le_QR_disc: "d ∈ D⇩D ⟹ norm (inv⇩L (Q d) o⇩L (R d)) ≤ QR_disc"
using QR_bdd
by (auto intro!: cSUP_upper)
lemma a_nonneg: "0 ≤ QR_disc"
using QR_contraction norm_ge_zero ex_dec_det QR_bdd
by (fastforce intro!: cSUP_upper2)
subsection ‹Bellman-Operator›
abbreviation "L_split d v ≡ inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d v)"
definition "ℒ_split v s = (⨆d ∈ D⇩D. L_split d v s)"
lemma ℒ_split_bfun_aux:
assumes "d ∈ D⇩D"
shows "norm (L_split d v) ≤ (⨆d ∈ D⇩D. norm (inv⇩L (Q d))) * r⇩M + norm v"
proof -
have "norm (L_split d v) ≤ norm (inv⇩L (Q d) (r_dec⇩b (mk_dec_det d))) + norm (inv⇩L (Q d) (R d v))"
by (simp add: blinfun.add_right norm_triangle_ineq)
also have "… ≤ norm (inv⇩L (Q d) (r_dec⇩b (mk_dec_det d))) + norm (inv⇩L (Q d) o⇩L R d) * norm v"
by (auto simp: blinfun_apply_blinfun_compose[symmetric] norm_blinfun simp del: blinfun_apply_blinfun_compose)
also have "… ≤ norm (inv⇩L (Q d) (r_dec⇩b (mk_dec_det d))) + norm v"
using norm_QR_less_one assms
by (fastforce intro!: mult_left_le_one_le)
also have "… ≤ norm (inv⇩L (Q d)) * r⇩M + norm v"
by (auto intro!: order.trans[OF norm_blinfun] mult_left_mono simp: norm_r_dec_le)
also have "… ≤ (⨆d ∈ D⇩D. norm (inv⇩L (Q d))) * r⇩M + norm v"
using Q_bdd bounded_imp_bdd_above
by (auto intro!: mult_right_mono cSUP_upper assms simp: r⇩M_nonneg)
finally show ?thesis.
qed
lemma L_split_le: "d ∈ D⇩D ⟹ L_split d v s ≤ (⨆d ∈ D⇩D. norm (inv⇩L (Q d))) * r⇩M + norm v"
using le_norm_bfun order.trans[OF le_norm_bfun ℒ_split_bfun_aux]
by auto
lift_definition ℒ⇩b_split :: "('s ⇒⇩b real) ⇒ ('s ⇒⇩b real)" is ℒ_split
unfolding ℒ_split_def bfun_def
using order.trans[OF abs_le_norm_bfun ℒ_split_bfun_aux] ex_dec_det
by (fastforce intro!: boundedI cSup_abs_le)
lemma ℒ⇩b_split_def': "ℒ⇩b_split v s = (⨆d∈D⇩D. L_split d v s)"
unfolding ℒ⇩b_split.rep_eq ℒ_split_def
by auto
lemma ℒ⇩b_split_contraction: "dist (ℒ⇩b_split v) (ℒ⇩b_split u) ≤ QR_disc * dist v u"
proof -
have
"ℒ⇩b_split v s - ℒ⇩b_split u s ≤ QR_disc * norm (v - u)" if h: "ℒ⇩b_split u s ≤ ℒ⇩b_split v s" for u v s
proof -
obtain d where d: "is_arg_max (λd. inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d v) s) (λd. d ∈ D⇩D) d"
using arg_max_ex_split by blast
hence *: "inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d u) s ≤ ℒ⇩b_split u s"
by (fastforce simp: ℒ⇩b_split_def' is_arg_max_linorder intro!: cSUP_upper2 L_split_le)
have "inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d v) s = ℒ⇩b_split v s"
by (auto simp: ℒ⇩b_split_def' arg_max_SUP[OF d])
hence "ℒ⇩b_split v s - ℒ⇩b_split u s = inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d v) s - ℒ⇩b_split u s"
by auto
also have "… ≤ (inv⇩L (Q d) o⇩L R d) (v - u) s"
using * by (auto simp: blinfun.bilinear_simps)
also have "… ≤ norm ((inv⇩L (Q d) o⇩L R d)) * norm (v - u)"
by (fastforce intro: order.trans[OF le_norm_bfun norm_blinfun])
also have "… ≤ QR_disc * norm (v - u)"
using QR_contraction d QR_bdd
by (auto simp: is_arg_max_linorder intro!: mult_right_mono cSUP_upper2)
finally show ?thesis.
qed
hence "¦(ℒ⇩b_split v - ℒ⇩b_split u) s¦ ≤ QR_disc * dist v u" for s
by (cases "ℒ⇩b_split v s ≤ ℒ⇩b_split u s") (fastforce simp: dist_norm norm_minus_commute)+
thus ?thesis
by (auto intro!: cSUP_least simp: dist_bfun.rep_eq dist_real_def)
qed
lemma ℒ⇩b_lim:
"∃!v. ℒ⇩b_split v = v"
"(λn. (ℒ⇩b_split ^^ n) v) ⇢ (THE v. ℒ⇩b_split v = v)"
using banach'[of ℒ⇩b_split] a_nonneg QR_contraction ℒ⇩b_split_contraction
unfolding is_contraction_def
by auto
lemma ℒ⇩b_split_tendsto_opt: "(λn. (ℒ⇩b_split ^^ n) v) ⇢ ν⇩b_opt"
proof -
obtain L where l_fix: "ℒ⇩b_split L = L"
using ℒ⇩b_lim(1) by auto
have "ν⇩b (mk_stationary_det d) ≤ L" if d: "d ∈ D⇩D" for d
proof -
let ?QR = "inv⇩L (Q d) o⇩L R d"
have "inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d L) ≤ ℒ⇩b_split L"
unfolding less_eq_bfun_def ℒ⇩b_split_def'
using d L_split_le by (auto intro!: bdd_aboveI cSUP_upper2)
hence "inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d L) ≤ L"
using l_fix by auto
hence aux: "inv⇩L (Q d) (r_dec⇩b (mk_dec_det d)) ≤ (id_blinfun - ?QR) L"
using that by (auto simp: blinfun.bilinear_simps le_diff_eq)
have inv_eq: "inv⇩L (id_blinfun - ?QR) = (∑i. ?QR ^^ i)"
using QR_contraction d norm_QR_less_one
by (auto intro!: inv⇩L_inf_sum)
have summable_QR:"summable (λi. norm (?QR ^^ i))"
using QR_contraction QR_bdd d
by (auto simp: a_nonneg
intro!: summable_comparison_test'[of "λi. QR_disc^i" 0 "λn. norm ((inv⇩L (Q d) o⇩L R d) ^^n)"]
cSUP_upper2 power_mono order.trans[OF norm_blinfunpow_le])
have "summable (λi. (?QR ^^ i) v s)" for v s
by (rule summable_comparison_test'[where g = "λi. norm (?QR ^^ i) * norm v"])
(auto intro!: summable_QR summable_norm_cancel order.trans[OF abs_le_norm_bfun] order.trans[OF norm_blinfun] summable_mult2)
moreover have "0 ≤ v ⟹ 0 ≤ (∑i<n. (?QR ^^ i) v s)" for n v s
using blinfunpow_nonneg[OF QR_nonneg[OF d]]
by (induction n) (auto simp add: less_eq_bfun_def)
ultimately have "0 ≤ v ⟹ 0 ≤ (∑i. ((?QR ^^ i) v s)) " for v s
by (auto intro!: summable_LIMSEQ LIMSEQ_le)
hence "0 ≤ v ⟹ 0 ≤ (∑i. ((?QR ^^ i))) v s" for v s
using bounded_linear_apply_bfun summable_QR summable_comparison_test'
by (subst bounded_linear.suminf[where f = "(λi. apply_bfun (blinfun_apply i v) s)"])
(fastforce intro: bounded_linear_compose[of "λs. apply_bfun s _"])+
hence "0 ≤ v ⟹ 0 ≤ inv⇩L (id_blinfun - ?QR) v" for v
by (simp add: inv_eq less_eq_bfun_def)
hence "(inv⇩L (id_blinfun - ?QR)) ((inv⇩L (Q d)) (r_dec⇩b (mk_dec_det d)))
≤ (inv⇩L (id_blinfun - ?QR)) ((id_blinfun - ?QR) L)"
by (metis aux blinfun.diff_right diff_ge_0_iff_ge)
hence "(inv⇩L (id_blinfun - ?QR) o⇩L inv⇩L (Q d)) (r_dec⇩b (mk_dec_det d)) ≤ L"
using invertible⇩L_inf_sum[OF norm_QR_less_one[OF that]] by auto
hence "(inv⇩L (Q d o⇩L (id_blinfun - ?QR))) (r_dec⇩b (mk_dec_det d)) ≤ L"
using d norm_QR_less_one
by (auto simp: inv⇩L_compose[OF Q_invertible invertible⇩L_inf_sum])
hence "(inv⇩L (Q d - R d)) (r_dec⇩b (mk_dec_det d)) ≤ L"
using Q_invertible d
by (auto simp: blinfun_compose_diff_right blinfun_compose_assoc[symmetric])
thus "ν⇩b (mk_stationary_det d) ≤ L"
by (auto simp: ν_stationary splitting[OF that, symmetric] inv⇩L_inf_sum blincomp_scaleR_right)
qed
hence opt_le: "ν⇩b_opt ≤ L"
by (metis ν_conserving_def conserving_imp_opt' ex_improving_det)
obtain d where d: "is_arg_max (λd. inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d L) s) (λd. d ∈ D⇩D) d" for s
using arg_max_ex_split by blast
hence "d ∈ D⇩D"
unfolding is_arg_max_linorder by auto
have "L = inv⇩L (Q d) (r_dec⇩b (mk_dec_det d) + R d L)"
by (subst l_fix[symmetric]) (fastforce simp: ℒ⇩b_split_def' arg_max_SUP[OF d])
hence "Q d L = r_dec⇩b (mk_dec_det d) + R d L"
by (metis Q_invertible ‹d ∈ D⇩D› inv_app2')
hence "(id_blinfun - l *⇩R 𝒫⇩1 (mk_dec_det d)) L = r_dec⇩b (mk_dec_det d)"
using splitting[OF ‹d ∈ D⇩D›] by (simp add: blinfun.diff_left)
hence "L = inv⇩L ((id_blinfun - l *⇩R 𝒫⇩1 (mk_dec_det d))) (r_dec⇩b (mk_dec_det d))"
using invertible⇩L_inf_sum[OF norm_𝒫⇩1_l_less] inv_app1' by metis
hence "L = ν⇩b (mk_stationary_det d)"
by (auto simp: inv⇩L_inf_sum ν_stationary blincomp_scaleR_right)
hence "ν⇩b_opt = L"
using opt_le ‹d ∈ D⇩D› is_markovian_def
by (auto intro: order.antisym[OF _ ν⇩b_le_opt])
thus ?thesis
using ℒ⇩b_lim l_fix the1_equality[OF ℒ⇩b_lim(1)] by auto
qed
lemma ℒ⇩b_split_fix[simp]: "ℒ⇩b_split ν⇩b_opt = ν⇩b_opt"
using ℒ⇩b_lim ℒ⇩b_split_tendsto_opt the_equality limI
by (metis (mono_tags, lifting))
lemma dist_ℒ⇩b_split_opt_eps:
assumes "eps > 0" "2 * QR_disc * dist v (ℒ⇩b_split v) < eps * (1-QR_disc)"
shows "dist (ℒ⇩b_split v) ν⇩b_opt < eps / 2"
proof -
have "(1 - QR_disc) * dist v ν⇩b_opt ≤ dist v (ℒ⇩b_split v)"
using dist_triangle ℒ⇩b_split_contraction[of v "ν⇩b_opt"]
by (fastforce simp: algebra_simps intro: order.trans[OF _ add_left_mono[of "dist (ℒ⇩b_split v) ν⇩b_opt"]])
hence "dist v ν⇩b_opt ≤ dist v (ℒ⇩b_split v) / (1 - QR_disc)"
using QR_contraction
by (simp add: mult.commute pos_le_divide_eq)
hence "2 * QR_disc * dist v ν⇩b_opt ≤ 2 * QR_disc * (dist v (ℒ⇩b_split v) / (1 - QR_disc))"
using ℒ⇩b_split_contraction assms mult_le_cancel_left_pos[of "2 * QR_disc"] a_nonneg
by (fastforce intro!: mult_left_mono[of _ _ "2 * QR_disc"])
hence "2 * QR_disc * dist v ν⇩b_opt < eps"
using a_nonneg QR_contraction
by (auto simp: assms(2) pos_divide_less_eq intro: order.strict_trans1)
hence "dist v ν⇩b_opt * QR_disc < eps / 2"
by argo
thus "dist (ℒ⇩b_split v) ν⇩b_opt < eps / 2"
using ℒ⇩b_split_contraction[of v ν⇩b_opt]
by (auto simp: algebra_simps)
qed
lemma L_split_fix:
assumes "d ∈ D⇩D"
shows "L_split d (ν⇩b (mk_stationary_det d)) = ν⇩b (mk_stationary_det d)"
proof -
let ?d = "mk_dec_det d"
let ?p = "mk_stationary_det d"
have "(Q d - R d) (ν⇩b ?p) = r_dec⇩b ?d"
using L_ν_fix[of "mk_dec_det d"]
by (simp add: L_def splitting[OF assms, symmetric] blinfun.bilinear_simps diff_eq_eq)
thus ?thesis
using assms
by (auto simp: blinfun.bilinear_simps diff_eq_eq inv⇩L_cancel_iff[OF Q_invertible])
qed
lemma L_split_contraction:
assumes "d ∈ D⇩D"
shows "dist (L_split d v) (L_split d u) ≤ QR_disc * dist v u"
proof -
have aux: "L_split d v s - L_split d u s ≤ QR_disc * dist v u" if lea: "(L_split d u s) ≤ (L_split d v s)" for v s u
proof -
have "L_split d v s - L_split d u s = (inv⇩L (Q d) o⇩L (R d)) (v - u) s"
by (auto simp: blinfun.bilinear_simps)
also have "… ≤ norm ((inv⇩L (Q d) o⇩L (R d)) (v - u))"
by (simp add: le_norm_bfun)
also have "… ≤ norm ((inv⇩L (Q d) o⇩L (R d))) * dist v u"
by (auto simp only: dist_norm norm_blinfun)
also have "… ≤ QR_disc * dist v u"
using assms QR_le_QR_disc
by (auto intro!: mult_right_mono)
finally show ?thesis
by auto
qed
have "dist (L_split d v s) (L_split d u s) ≤ QR_disc * dist v u" for v s u
using aux aux[of v _ u]
by (cases "L_split d v s ≥ L_split d u s") (auto simp: dist_real_def dist_commute)
thus "dist (L_split d v) (L_split d u) ≤ QR_disc * dist v u"
by (simp add: dist_bound)
qed
lemma argmax_policy_error_bound:
assumes am: "⋀s. is_arg_max (λd. L (mk_dec_det d) (ℒ⇩b v) s) (λd. d ∈ D⇩D) d"
shows "(1 - l) * dist (ν⇩b (mk_stationary_det d)) (ℒ⇩b v) ≤ l * dist (ℒ⇩b v) v"
proof -
have "dist (ν⇩b (mk_stationary_det d)) (ℒ⇩b v) = dist (L (mk_dec_det d) (ν⇩b (mk_stationary_det d))) (ℒ⇩b v)"
using L_ν_fix by presburger
also have "… ≤ dist (L (mk_dec_det d) (ν⇩b (mk_stationary_det d))) (ℒ⇩b (ℒ⇩b v)) + dist (ℒ⇩b (ℒ⇩b v)) (ℒ⇩b v)"
using dist_triangle by blast
also have "… = dist (L (mk_dec_det d) (ν⇩b (mk_stationary_det d))) (L (mk_dec_det d) (ℒ⇩b v)) + dist (ℒ⇩b (ℒ⇩b v)) (ℒ⇩b v)"
using ℒ⇩b_eq_SUP_det using arg_max_SUP[OF assms, symmetric]
by (auto simp: dist_bfun_def)
also have "… ≤ l * dist (ν⇩b (mk_stationary_det d)) (ℒ⇩b v) + l * dist (ℒ⇩b v) v"
by (meson add_mono contraction_L contraction_ℒ)
finally show ?thesis
by (auto simp: algebra_simps)
qed
lemma find_policy_QR_error_bound:
assumes "eps > 0" "2 * QR_disc * dist v (ℒ⇩b_split v) < eps * (1-QR_disc)"
assumes am: "⋀s. is_arg_max (λd. L_split d (ℒ⇩b_split v) s) (λd. d ∈ D⇩D) d"
shows "dist (ν⇩b (mk_stationary_det d)) ν⇩b_opt < eps"
proof -
let ?p = "mk_stationary_det d"
have L_eq_ℒ⇩b: "L_split d (ℒ⇩b_split v) = ℒ⇩b_split (ℒ⇩b_split v)"
by (auto simp: ℒ⇩b_split_def' arg_max_SUP[OF am])
have "dist (ν⇩b ?p) (ℒ⇩b_split v) = dist (L_split d (ν⇩b ?p)) (ℒ⇩b_split v)"
using am
by (auto simp: is_arg_max_linorder L_split_fix)
also have "… ≤ dist (L_split d (ν⇩b ?p)) (ℒ⇩b_split (ℒ⇩b_split v)) + dist (ℒ⇩b_split (ℒ⇩b_split v)) (ℒ⇩b_split v)"
by (auto intro: dist_triangle)
also have "… = dist (L_split d (ν⇩b ?p)) (L_split d (ℒ⇩b_split v)) + dist (ℒ⇩b_split (ℒ⇩b_split v)) (ℒ⇩b_split v)"
by (auto simp: L_eq_ℒ⇩b)
also have "… ≤ QR_disc * dist (ν⇩b ?p) (ℒ⇩b_split v) + QR_disc * dist (ℒ⇩b_split v) v"
using ℒ⇩b_split_contraction L_split_contraction am unfolding is_arg_max_def
by (auto intro!: add_mono)
finally have aux: "dist (ν⇩b ?p) (ℒ⇩b_split v) ≤ QR_disc * dist (ν⇩b ?p) (ℒ⇩b_split v) + QR_disc * dist (ℒ⇩b_split v) v" .
hence "dist (ν⇩b ?p) (ℒ⇩b_split v) - QR_disc * dist (ν⇩b ?p) (ℒ⇩b_split v) ≤ QR_disc * dist (ℒ⇩b_split v) v"
by auto
hence "dist (ν⇩b ?p) (ℒ⇩b_split v) * (1 - QR_disc) ≤ QR_disc * dist (ℒ⇩b_split v) v"
by argo
hence "2 * dist (ν⇩b ?p) (ℒ⇩b_split v) * (1-QR_disc) ≤ 2 * (QR_disc * dist (ℒ⇩b_split v) v)"
using mult_left_mono
by auto
hence "2 * dist (ν⇩b ?p) (ℒ⇩b_split v) * (1 - QR_disc) ≤ eps * (1 - QR_disc)"
using assms
by (auto intro!: mult_left_mono simp: dist_commute pos_divide_le_eq)
hence "2 * dist (ν⇩b ?p) (ℒ⇩b_split v) ≤ eps"
using QR_contraction mult_right_le_imp_le
by auto
moreover have "2 * dist (ℒ⇩b_split v) ν⇩b_opt < eps"
using dist_ℒ⇩b_split_opt_eps assms
by fastforce
ultimately show ?thesis
using dist_triangle[of "ν⇩b ?p" ν⇩b_opt "ℒ⇩b_split v"]
by auto
qed
end
context MDP_att_ℒ
begin
lemma inv_one_sub_Q':
fixes f :: "'c :: banach ⇒⇩L 'c"
assumes onorm_le: "norm (id_blinfun - f) < 1"
shows "inv⇩L f = (∑i. (id_blinfun - f)^^i)"
by (metis inv⇩L_I inv_one_sub_Q assms)
lemma blinfun_le_trans: "blinfun_le X Y ⟹ blinfun_le Y Z ⟹ blinfun_le X Z"
unfolding blinfun_le_def nonneg_blinfun_def
by (fastforce simp: blinfun.diff_left)
lemma blinfun_leI[intro]: "(⋀v. v ≥ 0 ⟹ blinfun_apply C v ≤ blinfun_apply D v) ⟹ blinfun_le C D"
unfolding blinfun_le_def nonneg_blinfun_def
by (auto simp: algebra_simps blinfun.diff_left)
lemma blinfun_pow_mono: "nonneg_blinfun (C :: ('c ⇒⇩b real) ⇒⇩L ('c ⇒⇩b real)) ⟹ blinfun_le C D ⟹ blinfun_le (C ^^ n) (D ^^ n)"
proof (induction n)
case 0
then show ?case by (simp add: blinfun_le_def nonneg_blinfun_def)
next
case (Suc n)
have *: "⋀v. 0 ≤ v ⟹ blinfun_apply (D ^^ n) (blinfun_apply C v) ≤ blinfun_apply (D ^^ n) (blinfun_apply D v)"
by (metis (no_types, opaque_lifting) Suc.prems(1) Suc.prems(2) blinfun_apply_mono blinfunpow_nonneg le_left_mono nonneg_blinfun_def nonneg_blinfun_mono)
thus ?case
using blinfun_apply_mono Suc
by (intro blinfun_leI) (auto simp: blinfunpow_assoc blinfunpow_nonneg nonneg_blinfun_def simp del: blinfunpow.simps intro!: blinfun_apply_mono order.trans[OF _ *])
qed
lemma blinfun_le_iff: "blinfun_le X Y ⟷ (∀v ≥ 0. X v ≤ Y v)"
unfolding blinfun_le_def nonneg_blinfun_def
by (auto simp: blinfun.diff_left)
text ‹An important theorem: allows to compare the rate of convergence for different splittings›
lemma norm_splitting_le:
assumes "is_splitting_blin (id_blinfun - l *⇩R 𝒫⇩1 d) Q1 R1"
and "is_splitting_blin (id_blinfun - l *⇩R 𝒫⇩1 d) Q2 R2"
and "blinfun_le R2 R1"
and "blinfun_le R1 (l *⇩R 𝒫⇩1 d)"
shows "norm (inv⇩L Q2 o⇩L R2) ≤ norm (inv⇩L Q1 o⇩L R1)"
proof -
have
inv_Q: "inv⇩L Q = (∑i. (id_blinfun - Q)^^i)" "norm (id_blinfun - Q) < 1" and
splitting_eq: "id_blinfun - Q = l *⇩R 𝒫⇩1 d - R" and
nonneg_Q: "nonneg_blinfun (id_blinfun - Q)"
if "blinfun_le R (l *⇩R 𝒫⇩1 d)"
and "is_splitting_blin (id_blinfun - l *⇩R 𝒫⇩1 d) Q R" for Q R
proof -
show splitting_eq: "id_blinfun - Q = l *⇩R 𝒫⇩1 d - R"
using that unfolding is_splitting_blin_def
by (auto simp: algebra_simps)
have R_nonneg: "nonneg_blinfun R"
using that by blast
show nonneg_Q: "nonneg_blinfun (id_blinfun - Q)"
using that by (simp add: blinfun_le_def splitting_eq)
moreover have "blinfun_le (id_blinfun - Q) (l *⇩R 𝒫⇩1 d)"
using R_nonneg by (simp add: splitting_eq blinfun_le_def)
ultimately have "norm (id_blinfun - Q) ≤ norm (l *⇩R 𝒫⇩1 d)"
using blinfun_le_def matrix_le_norm_mono by fast
thus "norm (id_blinfun - Q) < 1"
using norm_𝒫⇩1_l_less by (simp add: order.strict_trans1)
thus "inv⇩L Q = (∑i. (id_blinfun - Q) ^^ i)"
using inv⇩L_inf_sum by fastforce
qed
have i1: "inv⇩L Q1 = (∑i. (id_blinfun - Q1) ^^ i)" "norm (id_blinfun - Q1) < 1"
and i2: "inv⇩L Q2 = (∑i. (id_blinfun - Q2) ^^ i)" "norm (id_blinfun - Q2) < 1"
using assms by (auto intro: blinfun_le_trans inv_Q[of R2 Q2] inv_Q[of R1 Q1])
have Q1_le_Q2: "blinfun_le (id_blinfun - Q1) (id_blinfun - Q2)"
using assms unfolding is_splitting_blin_def blinfun_le_def eq_diff_eq
by fastforce
have "(inv⇩L Q1) = ((∑i. (id_blinfun - Q1) ^^ i))"
using i1 by auto
also have "… = ((∑i. ((id_blinfun - Q1) ^^ i)))"
using summable_inv_Q i1(2)
by auto
have "blinfun_le ((∑i. ((id_blinfun - Q1) ^^ i))) (∑i. ((id_blinfun - Q2) ^^ i))"
proof -
have le_n: "⋀n v. 0 ≤ v ⟹ (∑i<n. ((id_blinfun - Q1) ^^ i) v) ≤ (∑i<n. ((id_blinfun - Q2) ^^ i) v)"
using nonneg_Q blinfun_pow_mono[OF _ Q1_le_Q2] assms
by (auto intro!: sum_mono simp: blinfun_le_iff)
hence le_n_elem: "⋀n v. 0 ≤ v ⟹ (∑i<n. ((id_blinfun - Q1) ^^ i) v s) ≤ (∑i<n. ((id_blinfun - Q2) ^^ i) v s)" for s
unfolding less_eq_bfun_def
by (simp add: sum_apply_bfun)
have tt: "(λn. (∑i<n. ((id_blinfun - Q1) ^^ i) v s)) ⇢ (∑i. ((id_blinfun - Q1) ^^ i)) v s"
"(λn. (∑i<n. ((id_blinfun - Q2) ^^ i) v s)) ⇢ (∑i. ((id_blinfun - Q2) ^^ i)) v s" for v s
unfolding blinfun.sum_left[symmetric] sum_apply_bfun[symmetric]
using summable_inv_Q[OF i1(2)] summable_inv_Q[OF i2(2)]
by (fastforce intro: bfun_tendsto_apply_bfun tendsto_blinfun_apply summable_LIMSEQ)+
show ?thesis
unfolding blinfun_le_iff less_eq_bfun_def
using le_n_elem
by (auto simp add: less_eq_bfunI intro: Topological_Spaces.lim_mono[OF _ tt(1) tt(2)])
qed
also have "… = (inv⇩L Q2)"
using summable_inv_Q i2(2) i2 by auto
finally have Q1_le_Q2: "blinfun_le (inv⇩L Q1) (inv⇩L Q2)".
have *: "nonneg_blinfun ((inv⇩L Q1) o⇩L R1)" "nonneg_blinfun ((inv⇩L Q2) o⇩L R2)"
using assms is_splitting_blin_def
by (metis blinfun_apply_blinfun_compose nonneg_blinfun_def)+
have "0 ≤ (id_blinfun - l *⇩R 𝒫⇩1 d) 1"
using less_imp_le[OF disc_lt_one]
by (auto simp: blinfun.diff_left less_eq_bfun_def blinfun.scaleR_left)
hence "(inv⇩L Q1) ((id_blinfun - l *⇩R 𝒫⇩1 d) 1) ≤ (inv⇩L Q2) ((id_blinfun - l *⇩R 𝒫⇩1 d) 1)"
using Q1_le_Q2
by (simp add: blinfun_le_iff)
hence "(inv⇩L Q1) ((Q1 - R1) 1) ≤ (inv⇩L Q2) ((Q2 - R2) 1)"
by (metis (no_types, opaque_lifting) assms(1) assms(2) is_splitting_blin_def)
hence "(inv⇩L Q1 o⇩L Q1) 1 - (inv⇩L Q1 o⇩L R1) 1 ≤ (inv⇩L Q2 o⇩L Q2) 1 - (inv⇩L Q2 o⇩L R2) 1"
by (auto simp: blinfun.add_left blinfun.diff_right blinfun.diff_left)
hence "(inv⇩L Q2 o⇩L R2) 1 ≤ (inv⇩L Q1 o⇩L R1) 1"
using assms unfolding is_splitting_blin_def by auto
moreover have "0 ≤ (inv⇩L Q2 o⇩L R2) 1"
using * assms(2) by (fastforce simp: less_eq_bfunI intro!: nonneg_blinfun_nonneg)
ultimately have "norm ((inv⇩L Q2 o⇩L R2) 1) ≤ norm ((inv⇩L Q1 o⇩L R1) 1)"
by (auto simp: less_eq_bfun_def norm_bfun_def' intro!: abs_le_norm_bfun abs_ge_self cSUP_mono bdd_above.I2 intro: order.trans)
thus "norm ((inv⇩L Q2 o⇩L R2)) ≤ norm ((inv⇩L Q1 o⇩L R1))"
by (simp add: * norm_nonneg_blinfun_one)
qed
end
end