Theory Blinfun_Util
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 o⇩L f = f"
"f o⇩L id_blinfun = f"
by (auto intro!: blinfun_eqI)
lemma blinfun_compose_assoc: "F o⇩L G o⇩L H = F o⇩L (G o⇩L H)"
using blinfun_apply_inject by fastforce
lemma blinfun_compose_diff_right: "f o⇩L (g - h) = (f o⇩L g) - (f o⇩L 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 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
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 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)"
by (simp add: bounded_bilinear.add_left bounded_bilinear_blinfun_compose)
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›
definition "is_inverse⇩L X Y ⟷ X o⇩L Y = id_blinfun ∧ Y o⇩L X = id_blinfun"
abbreviation "invertible⇩L X ≡ ∃X'. is_inverse⇩L X X'"
lemma is_inverse⇩L_I[intro]:
assumes "X o⇩L Y = id_blinfun" "Y o⇩L X = id_blinfun"
shows "is_inverse⇩L X Y"
using assms
unfolding is_inverse⇩L_def
by auto
lemma is_inverse⇩L_D[dest]:
assumes "is_inverse⇩L X Y"
shows "X o⇩L Y = id_blinfun" "Y o⇩L X = id_blinfun"
using assms
unfolding is_inverse⇩L_def
by auto
lemma invertible⇩L_D[dest]:
assumes "invertible⇩L f"
obtains g where "f o⇩L g = id_blinfun" "g o⇩L f = id_blinfun"
using assms
by auto
lemma invertible⇩L_I[intro]:
assumes "f o⇩L g = id_blinfun" "g o⇩L f = id_blinfun"
shows "invertible⇩L f"
using assms
by auto
lemma is_inverse⇩L_comm: "is_inverse⇩L X Y ⟷ is_inverse⇩L Y X"
by auto
lemma is_inverse⇩L_unique: "is_inverse⇩L f g ⟹ is_inverse⇩L f h ⟹ g = h"
unfolding is_inverse⇩L_def
using blinfun_compose_assoc blinfun_compose_id(1)
by metis
lemma is_inverse⇩L_ex1: "is_inverse⇩L f g ⟹ ∃!h. is_inverse⇩L f h"
using is_inverse⇩L_unique
by auto
lemma is_inverse⇩L_ex1': "∃x. is_inverse⇩L f x ⟹ ∃!x. is_inverse⇩L f x"
using is_inverse⇩L_ex1
by auto
definition "inv⇩L f = (THE g. is_inverse⇩L f g)"
lemma inv⇩L_eq:
assumes "is_inverse⇩L f g"
shows "inv⇩L f = g"
unfolding inv⇩L_def
using assms is_inverse⇩L_ex1
by (auto intro!: the_equality)
lemma inv⇩L_I:
assumes "f o⇩L g = id_blinfun" "g o⇩L f = id_blinfun"
shows "g = inv⇩L f"
using assms inv⇩L_eq
unfolding is_inverse⇩L_def
by auto
lemma inv_app1 [simp]: "invertible⇩L X ⟹ (inv⇩L X) o⇩L X = id_blinfun"
using is_inverse⇩L_ex1' inv⇩L_eq
by blast
lemma inv_app2[simp]: "invertible⇩L X ⟹ X o⇩L (inv⇩L X) = id_blinfun"
using is_inverse⇩L_ex1' inv⇩L_eq
by blast
lemma inv_app1'[simp]: "invertible⇩L X ⟹ inv⇩L X (X v) = v"
using inv_app1 blinfun_apply_blinfun_compose id_blinfun.rep_eq
by metis
lemma inv_app2'[simp]: "invertible⇩L X ⟹ X (inv⇩L X v) = v"
using inv_app2 blinfun_apply_blinfun_compose id_blinfun.rep_eq
by metis
lemma inv⇩L_inv⇩L[simp]: "invertible⇩L X ⟹ inv⇩L (inv⇩L X) = X"
by (metis inv⇩L_eq is_inverse⇩L_comm)
lemma inv⇩L_cancel_iff:
assumes "invertible⇩L f"
shows "f x = y ⟷ x = inv⇩L f y"
by (auto simp add: assms)
lemma invertible⇩L_inf_sum:
assumes "norm (X :: 'b :: banach ⇒⇩L 'b) < 1"
shows "invertible⇩L (id_blinfun - X)"
using Blinfun_Util.inv_norm_le[OF assms] assms
by blast
lemma inv⇩L_inf_sum:
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
by (auto simp: inv⇩L_I[symmetric])
lemma is_inverse⇩L_compose:
assumes "invertible⇩L f" "invertible⇩L g"
shows "is_inverse⇩L (f o⇩L g) (inv⇩L g o⇩L inv⇩L f)"
by (auto intro!: blinfun_eqI is_inverse⇩L_I[of _ "inv⇩L g o⇩L inv⇩L f"]
simp: inv_app2'[OF assms(1)] inv_app2'[OF assms(2)] inv_app1'[OF assms(1)] inv_app1'[OF assms(2)])
lemma invertible⇩L_compose: "invertible⇩L f ⟹ invertible⇩L g ⟹ invertible⇩L (f o⇩L g)"
using is_inverse⇩L_compose
by blast
lemma inv⇩L_compose:
assumes "invertible⇩L f" "invertible⇩L g"
shows"inv⇩L (f o⇩L g) = (inv⇩L g) o⇩L (inv⇩L f)"
using assms inv⇩L_eq is_inverse⇩L_compose
by blast
lemma inv⇩L_id_blinfun[simp]: "inv⇩L id_blinfun = id_blinfun"
by (metis blinfun_compose_id(2) inv⇩L_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
lemma tendsto_blinfun_apply: "(λn. X n) ⇢ L ⟹ (λn. blinfun_apply (X n) u) ⇢ L u"
using blinfun.bounded_bilinear_axioms
by (auto simp: convergent_LIMSEQ_iff intro: Limits.bounded_bilinear.tendsto)
definition "nonneg_blinfun (Q :: _::{ordered_real_normed_vector} ⇒⇩L _::{ordered_ab_group_add, ordered_real_normed_vector}) ≡ (∀v≥0. blinfun_apply Q v ≥ 0)"
definition "blinfun_le Q R = nonneg_blinfun (R - Q)"
lemma nonneg_blinfun_nonneg[dest]: "nonneg_blinfun Q ⟹ 0 ≤ v ⟹ 0 ≤ Q v"
unfolding nonneg_blinfun_def
by auto
lemma nonneg_blinfun_mono[dest]: "nonneg_blinfun Q ⟹ u ≤ v ⟹ Q u ≤ Q v"
using nonneg_blinfun_nonneg[of Q "v - u", unfolded blinfun.diff_right]
by auto
lemma nonneg_id_blinfun: "nonneg_blinfun id_blinfun"
by (auto simp: nonneg_blinfun_def)
lemma blinfun_nonneg_eq:
assumes "∀v ≥ 0. blinfun_apply (f::('c ⇒⇩b real) ⇒⇩L ('c ⇒⇩b real)) v = blinfun_apply g v"
shows "f = g"
proof (rule blinfun_eqI)
fix v :: "'c ⇒⇩b real"
define v1 where "v1 = Bfun (λx. max (v x) 0)"
define v2 where "v2 = Bfun (λx. - min (v x) 0)"
have in_bfun[simp]: "(λx. max (v x) 0) ∈ bfun" "(λx. - min (v x) 0) ∈ bfun"
by (auto simp: le_norm_bfun minus_min_eq_max abs_le_norm_bfun abs_le_D2 intro!: boundedI[of _ "norm v"])
have eq_v: "v = v1 - v2"
unfolding v1_def v2_def
by (auto simp: Bfun_inverse)
have nonneg: "0 ≤ v1" "0 ≤ v2"
unfolding less_eq_bfun_def
by (auto simp: v1_def v2_def Bfun_inverse)
show " blinfun_apply f v = blinfun_apply g v"
unfolding eq_v
using nonneg assms
by (auto simp: blinfun.diff_right)
qed
lemma bfun_zero_le_one: "0 ≤ (1 :: 'c ⇒⇩b real)"
by (simp add: less_eq_bfunI)
lemma norm_nonneg_blinfun_one:
assumes "nonneg_blinfun (X :: ('c ⇒⇩b real) ⇒⇩L ('c ⇒⇩b real))"
shows "norm X = norm (blinfun_apply X 1)"
using assms unfolding nonneg_blinfun_def
by (auto simp: norm_blinfun_mono_eq_one)
lemma blinfun_apply_mono: "nonneg_blinfun X ⟹ 0 ≤ v ⟹ blinfun_le X Y ⟹ X v ≤ Y v"
by (simp add: blinfun.diff_left blinfun_le_def nonneg_blinfun_def)
lemma nonneg_blinfun_scaleR[intro]: "nonneg_blinfun B ⟹ 0 ≤ c ⟹ nonneg_blinfun (c *⇩R B)"
by (simp add: nonneg_blinfun_def scaleR_blinfun.rep_eq scaleR_nonneg_nonneg)
lemma nonneg_blinfun_compose[intro]: "nonneg_blinfun B ⟹ nonneg_blinfun C ⟹ nonneg_blinfun (C o⇩L B)"
by (simp add: nonneg_blinfun_def)
lemma matrix_le_norm_mono:
assumes "nonneg_blinfun (C :: ('c ⇒⇩b real) ⇒⇩L ('c ⇒⇩b real))"
and "nonneg_blinfun (D - C)"
shows "norm C ≤ norm D"
proof -
have "nonneg_blinfun D"
using assms
by (metis add_nonneg_nonneg diff_add_cancel nonneg_blinfun_def plus_blinfun.rep_eq)
have zero_le: "0 ≤ C 1" "0 ≤ D 1"
using assms zero_le_one ‹nonneg_blinfun D›
by (auto simp add: less_eq_bfunI nonneg_blinfun_nonneg)
hence "C 1 ≤ D 1"
using assms(2) unfolding nonneg_blinfun_def blinfun.diff_left
by (simp add: less_eq_bfun_def)
thus ?thesis
using assms ‹nonneg_blinfun D› zero_le le_norm_bfun
by (fastforce simp: norm_nonneg_blinfun_one norm_bfun_def' less_eq_bfun_def intro!: bdd_above.I2 cSUP_mono)
qed
lemma bounded_subset: "Y ⊆ X ⟹ bounded (f ` X) ⟹ bounded (f ` Y)"
by (auto simp: bounded_def)
lemma bounded_subset_range: "bounded (range f) ⟹ bounded (f ` Y)"
using bounded_subset subset_UNIV by metis
lift_definition bfun_if :: "('b ⇒ bool) ⇒ ('b ⇒⇩b 'c::metric_space) ⇒ ('b ⇒⇩b 'c) ⇒ ('b ⇒⇩b 'c)" is "λb u v s. if b s then u s else v s"
using bounded_subset_range
by (auto simp: bfun_def)
lemma bfun_if_add: "bfun_if b (w + z) (u + v) = bfun_if b w u + bfun_if b z v"
by (auto simp: bfun_if.rep_eq)
lemma bfun_if_zero_add: "bfun_if b 0 (u + v) = bfun_if b 0 u + bfun_if b 0 v"
by (auto simp: bfun_if.rep_eq)
lemma bfun_if_zero_le: "0 ≤ v ⟹ bfun_if b 0 v ≤ v"
by (metis (no_types, lifting) bfun_if.rep_eq le_less less_eq_bfun_def)
lemma bfun_if_eq: "(⋀i. P i ⟹ apply_bfun v i = apply_bfun u i) ⟹ (⋀i. ¬P i ⟹ v i = apply_bfun w i) ⟹ bfun_if P u w = v"
by (auto simp: bfun_if.rep_eq)
lemma bfun_if_scaleR: "c *⇩R bfun_if b v1 v2 = bfun_if b (c *⇩R v1) (c *⇩R v2)"
by (auto simp: bfun_if.rep_eq)
lemma summable_blinfun_apply:
assumes "summable (f :: nat ⇒ 'a::real_normed_vector ⇒⇩L 'a)"
shows "summable (λn. f n v)"
using assms tendsto_blinfun_apply
unfolding summable_def sums_def blinfun.sum_left[symmetric]
by auto
lemma blinfun_apply_suminf:
assumes "summable (f :: nat ⇒ 'a::real_normed_vector ⇒⇩L 'a)"
shows "(∑k. blinfun_apply (f k) v) = (∑k. f k) v"
using bounded_linear.suminf[OF blinfun.bounded_linear_left assms]
by auto
end