Theory MTX_Norms
section ‹ Matrix norms ›
text ‹ Here, we explore some properties about the operator and the maximum norms for matrices. ›
theory MTX_Norms
imports MTX_Preliminaries
begin
subsection‹ Matrix operator norm ›
abbreviation op_norm :: "('a::real_normed_algebra_1)^'n^'m ⇒ real" ("(1∥_∥⇩o⇩p)" [65] 61)
where "∥A∥⇩o⇩p ≡ onorm (λx. A *v x)"
lemma norm_matrix_bound:
fixes A :: "('a::real_normed_algebra_1)^'n^'m"
shows "∥x∥ = 1 ⟹ ∥A *v x∥ ≤ ∥(χ i j. ∥A $ i $ j∥) *v 1∥"
proof-
fix x :: "('a, 'n) vec" assume "∥x∥ = 1"
hence xi_le1:"⋀i. ∥x $ i∥ ≤ 1"
by (metis Finite_Cartesian_Product.norm_nth_le)
{fix j::'m
have "∥(∑i∈UNIV. A $ j $ i * x $ i)∥ ≤ (∑i∈UNIV. ∥A $ j $ i * x $ i∥)"
using norm_sum by blast
also have "... ≤ (∑i∈UNIV. (∥A $ j $ i∥) * (∥x $ i∥))"
by (simp add: norm_mult_ineq sum_mono)
also have "... ≤ (∑i∈UNIV. (∥A $ j $ i∥) * 1)"
using xi_le1 by (simp add: sum_mono mult_left_le)
finally have "∥(∑i∈UNIV. A $ j $ i * x $ i)∥ ≤ (∑i∈UNIV. (∥A $ j $ i∥) * 1)" by simp}
hence "⋀j. ∥(A *v x) $ j∥ ≤ ((χ i1 i2. ∥A $ i1 $ i2∥) *v 1) $ j"
unfolding matrix_vector_mult_def by simp
hence "(∑j∈UNIV. (∥(A *v x) $ j∥)⇧2) ≤ (∑j∈UNIV. (∥((χ i1 i2. ∥A $ i1 $ i2∥) *v 1) $ j∥)⇧2)"
by (metis (mono_tags, lifting) norm_ge_zero power2_abs power_mono real_norm_def sum_mono)
thus "∥A *v x∥ ≤ ∥(χ i j. ∥A $ i $ j∥) *v 1∥"
unfolding norm_vec_def L2_set_def by simp
qed
lemma onorm_set_proptys:
fixes A :: "('a::real_normed_algebra_1)^'n^'m"
shows "bounded (range (λx. (∥A *v x∥) / (∥x∥)))"
and "bdd_above (range (λx. (∥A *v x∥) / (∥x∥)))"
and "(range (λx. (∥A *v x∥) / (∥x∥))) ≠ {}"
unfolding bounded_def bdd_above_def image_def dist_real_def
apply(rule_tac x=0 in exI)
by (rule_tac x="∥(χ i j. ∥A $ i $ j∥) *v 1∥" in exI, clarsimp,
subst mult_norm_matrix_sgn_eq[symmetric], clarsimp,
rule_tac x="sgn _" in norm_matrix_bound, simp add: norm_sgn)+ force
lemma op_norm_set_proptys:
fixes A :: "('a::real_normed_algebra_1)^'n^'m"
shows "bounded {∥A *v x∥ | x. ∥x∥ = 1}"
and "bdd_above {∥A *v x∥ | x. ∥x∥ = 1}"
and "{∥A *v x∥ | x. ∥x∥ = 1} ≠ {}"
unfolding bounded_def bdd_above_def apply safe
apply(rule_tac x=0 in exI, rule_tac x="∥(χ i j. ∥A $ i $ j∥) *v 1∥" in exI)
apply(force simp: norm_matrix_bound dist_real_def)
apply(rule_tac x="∥(χ i j. ∥A $ i $ j∥) *v 1∥" in exI, force simp: norm_matrix_bound)
using ex_norm_eq_1 by blast
lemma op_norm_def: "∥A∥⇩o⇩p = Sup {∥A *v x∥ | x. ∥x∥ = 1}"
apply(rule antisym[OF onorm_le cSup_least[OF op_norm_set_proptys(3)]])
apply(case_tac "x = 0", simp)
apply(subst mult_norm_matrix_sgn_eq[symmetric], simp)
apply(rule cSup_upper[OF _ op_norm_set_proptys(2)])
apply(force simp: norm_sgn)
unfolding onorm_def
apply(rule cSup_upper[OF _ onorm_set_proptys(2)])
by (simp add: image_def, clarsimp) (metis div_by_1)
lemma norm_matrix_le_op_norm: "∥x∥ = 1 ⟹ ∥A *v x∥ ≤ ∥A∥⇩o⇩p"
apply(unfold onorm_def, rule cSup_upper[OF _ onorm_set_proptys(2)])
unfolding image_def by (clarsimp, rule_tac x=x in exI) simp
lemma op_norm_ge_0: "0 ≤ ∥A∥⇩o⇩p"
using ex_norm_eq_1 norm_ge_zero norm_matrix_le_op_norm basic_trans_rules(23) by blast
lemma norm_sgn_le_op_norm: "∥A *v sgn x∥ ≤ ∥A∥⇩o⇩p"
by (cases "x=0", simp_all add: norm_sgn norm_matrix_le_op_norm op_norm_ge_0)
lemma norm_matrix_le_mult_op_norm: "∥A *v x∥ ≤ (∥A∥⇩o⇩p) * (∥x∥)"
proof-
have "∥A *v x∥ = (∥A *v sgn x∥) * (∥x∥)"
by(simp add: mult_norm_matrix_sgn_eq)
also have "... ≤ (∥A∥⇩o⇩p) * (∥x∥)"
using norm_sgn_le_op_norm[of A] by (simp add: mult_mono')
finally show ?thesis by simp
qed
lemma blin_matrix_vector_mult: "bounded_linear ((*v) A)" for A :: "('a::real_normed_algebra_1)^'n^'m"
by (unfold_locales) (auto intro: norm_matrix_le_mult_op_norm simp:
mult.commute matrix_vector_right_distrib vector_scaleR_commute)
lemma op_norm_eq_0: "(∥A∥⇩o⇩p = 0) = (A = 0)" for A :: "('a::real_normed_field)^'n^'m"
unfolding onorm_eq_0[OF blin_matrix_vector_mult] using matrix_axis_0[of 1 A] by fastforce
lemma op_norm0: "∥(0::('a::real_normed_field)^'n^'m)∥⇩o⇩p = 0"
using op_norm_eq_0[of 0] by simp
lemma op_norm_triangle: "∥A + B∥⇩o⇩p ≤ (∥A∥⇩o⇩p) + (∥B∥⇩o⇩p)"
using onorm_triangle[OF blin_matrix_vector_mult[of A] blin_matrix_vector_mult[of B]]
matrix_vector_mult_add_rdistrib[symmetric, of A _ B] by simp
lemma op_norm_scaleR: "∥c *⇩R A∥⇩o⇩p = ¦c¦ * (∥A∥⇩o⇩p)"
unfolding onorm_scaleR[OF blin_matrix_vector_mult, symmetric] scaleR_vector_assoc ..
lemma op_norm_matrix_matrix_mult_le: "∥A ** B∥⇩o⇩p ≤ (∥A∥⇩o⇩p) * (∥B∥⇩o⇩p)"
proof(rule onorm_le)
have "0 ≤ (∥A∥⇩o⇩p)"
by(rule onorm_pos_le[OF blin_matrix_vector_mult])
fix x have "∥A ** B *v x∥ = ∥A *v (B *v x)∥"
by (simp add: matrix_vector_mul_assoc)
also have "... ≤ (∥A∥⇩o⇩p) * (∥B *v x∥)"
by (simp add: norm_matrix_le_mult_op_norm[of _ "B *v x"])
also have "... ≤ (∥A∥⇩o⇩p) * ((∥B∥⇩o⇩p) * (∥x∥))"
using norm_matrix_le_mult_op_norm[of B x] ‹0 ≤ (∥A∥⇩o⇩p)› mult_left_mono by blast
finally show "∥A ** B *v x∥ ≤ (∥A∥⇩o⇩p) * (∥B∥⇩o⇩p) * (∥x∥)"
by simp
qed
lemma norm_matrix_vec_mult_le_transpose:
"∥x∥ = 1 ⟹ (∥A *v x∥) ≤ sqrt (∥transpose A ** A∥⇩o⇩p) * (∥x∥)" for A :: "real^'n^'n"
proof-
assume "∥x∥ = 1"
have "(∥A *v x∥)⇧2 = (A *v x) ∙ (A *v x)"
using dot_square_norm[of "(A *v x)"] by simp
also have "... = x ∙ (transpose A *v (A *v x))"
using vec_mult_inner by blast
also have "... ≤ (∥x∥) * (∥transpose A *v (A *v x)∥)"
using norm_cauchy_schwarz by blast
also have "... ≤ (∥transpose A ** A∥⇩o⇩p) * (∥x∥)^2"
apply(subst matrix_vector_mul_assoc)
using norm_matrix_le_mult_op_norm[of "transpose A ** A" x]
by (simp add: ‹∥x∥ = 1›)
finally have "((∥A *v x∥))^2 ≤ (∥transpose A ** A∥⇩o⇩p) * (∥x∥)^2"
by linarith
thus "(∥A *v x∥) ≤ sqrt ((∥transpose A ** A∥⇩o⇩p)) * (∥x∥)"
by (simp add: ‹∥x∥ = 1› real_le_rsqrt)
qed
lemma op_norm_le_sum_column: "∥A∥⇩o⇩p ≤ (∑i∈UNIV. ∥column i A∥)" for A :: "real^'n^'m"
proof(unfold op_norm_def, rule cSup_least[OF op_norm_set_proptys(3)], clarsimp)
fix x :: "real^'n" assume x_def:"∥x∥ = 1"
hence x_hyp:"⋀i. ∥x $ i∥ ≤ 1"
by (simp add: norm_bound_component_le_cart)
have "(∥A *v x∥) = ∥(∑i∈UNIV. x $ i *s column i A)∥"
by(subst matrix_mult_sum[of A], simp)
also have "... ≤ (∑i∈UNIV. ∥x $ i *s column i A∥)"
by (simp add: sum_norm_le)
also have "... = (∑i∈UNIV. (∥x $ i∥) * (∥column i A∥))"
by (simp add: mult_norm_matrix_sgn_eq)
also have "... ≤ (∑i∈UNIV. ∥column i A∥)"
using x_hyp by (simp add: mult_left_le_one_le sum_mono)
finally show "∥A *v x∥ ≤ (∑i∈UNIV. ∥column i A∥)" .
qed
lemma op_norm_le_transpose: "∥A∥⇩o⇩p ≤ ∥transpose A∥⇩o⇩p" for A :: "real^'n^'n"
proof-
have obs:"∀x. ∥x∥ = 1 ⟶ (∥A *v x∥) ≤ sqrt ((∥transpose A ** A∥⇩o⇩p)) * (∥x∥)"
using norm_matrix_vec_mult_le_transpose by blast
have "(∥A∥⇩o⇩p) ≤ sqrt ((∥transpose A ** A∥⇩o⇩p))"
using obs apply(unfold op_norm_def)
by (rule cSup_least[OF op_norm_set_proptys(3)]) clarsimp
hence "((∥A∥⇩o⇩p))⇧2 ≤ (∥transpose A ** A∥⇩o⇩p)"
using power_mono[of "(∥A∥⇩o⇩p)" _ 2] op_norm_ge_0
by (metis not_le real_less_lsqrt)
also have "... ≤ (∥transpose A∥⇩o⇩p) * (∥A∥⇩o⇩p)"
using op_norm_matrix_matrix_mult_le by blast
finally have "((∥A∥⇩o⇩p))⇧2 ≤ (∥transpose A∥⇩o⇩p) * (∥A∥⇩o⇩p)"
by linarith
thus "(∥A∥⇩o⇩p) ≤ (∥transpose A∥⇩o⇩p)"
using sq_le_cancel[of "(∥A∥⇩o⇩p)"] op_norm_ge_0 by metis
qed
subsection‹ Matrix maximum norm ›
abbreviation max_norm :: "real^'n^'m ⇒ real" ("(1∥_∥⇩m⇩a⇩x)" [65] 61)
where "∥A∥⇩m⇩a⇩x ≡ Max (abs ` (entries A))"
lemma max_norm_def: "∥A∥⇩m⇩a⇩x = Max {¦A $ i $ j¦|i j. i∈UNIV ∧ j∈UNIV}"
by (simp add: image_def, rule arg_cong[of _ _ Max], blast)
lemma max_norm_set_proptys: "finite {¦A $ i $ j¦ |i j. i ∈ UNIV ∧ j ∈ UNIV}" (is "finite ?X")
proof-
have "⋀i. finite {¦A $ i $ j¦ | j. j ∈ UNIV}"
using finite_Atleast_Atmost_nat by fastforce
hence "finite (⋃i∈UNIV. {¦A $ i $ j¦ | j. j ∈ UNIV})" (is "finite ?Y")
using finite_class.finite_UNIV by blast
also have "?X ⊆ ?Y"
by auto
ultimately show ?thesis
using finite_subset by blast
qed
lemma max_norm_ge_0: "0 ≤ ∥A∥⇩m⇩a⇩x"
unfolding max_norm_def
apply(rule order.trans[OF abs_ge_zero[of "A $ _ $ _"] Max_ge])
using max_norm_set_proptys by auto
lemma op_norm_le_max_norm:
fixes A :: "real^('n::finite)^('m::finite)"
shows "∥A∥⇩o⇩p ≤ real CARD('m) * real CARD('n) * (∥A∥⇩m⇩a⇩x)"
apply(rule onorm_le_matrix_component)
unfolding max_norm_def by(rule Max_ge[OF max_norm_set_proptys]) force
lemma sqrt_Sup_power2_eq_Sup_abs:
"finite A ⟹ A ≠ {} ⟹ sqrt (Sup {(f i)⇧2 |i. i ∈ A}) = Sup {¦f i¦ |i. i ∈ A}"
proof(rule sym)
assume assms: "finite A" "A ≠ {}"
then obtain i where i_def: "i ∈ A ∧ Sup {(f i)⇧2|i. i ∈ A} = (f i)^2"
using cSup_finite_ex[of "{(f i)⇧2|i. i ∈ A}"] by auto
hence lhs: "sqrt (Sup {(f i)⇧2 |i. i ∈ A}) = ¦f i¦"
by simp
have "finite {(f i)⇧2|i. i ∈ A}"
using assms by simp
hence "∀j∈A. (f j)⇧2 ≤ (f i)⇧2"
using i_def cSup_upper[of _ "{(f i)⇧2 |i. i ∈ A}"] by force
hence "∀j∈A. ¦f j¦ ≤ ¦f i¦"
using abs_le_square_iff by blast
also have "¦f i¦ ∈ {¦f i¦ |i. i ∈ A}"
using i_def by auto
ultimately show "Sup {¦f i¦ |i. i ∈ A} = sqrt (Sup {(f i)⇧2 |i. i ∈ A})"
using cSup_mem_eq[of "¦f i¦" "{¦f i¦ |i. i ∈ A}"] lhs by auto
qed
lemma sqrt_Max_power2_eq_max_abs:
"finite A ⟹ A ≠ {} ⟹ sqrt (Max {(f i)⇧2|i. i ∈ A}) = Max {¦f i¦ |i. i ∈ A}"
apply(subst cSup_eq_Max[symmetric], simp_all)+
using sqrt_Sup_power2_eq_Sup_abs .
lemma op_norm_diag_mat_eq: "∥diag_mat f∥⇩o⇩p = Max {¦f i¦ |i. i ∈ UNIV}" (is "_ = Max ?A")
proof(unfold op_norm_def)
have obs: "⋀x i. (f i)⇧2 * (x $ i)⇧2 ≤ Max {(f i)⇧2|i. i ∈ UNIV} * (x $ i)⇧2"
apply(rule mult_right_mono[OF _ zero_le_power2])
using le_max_image_of_finite[of "λi. (f i)^2"] by simp
{fix r assume "r ∈ {∥diag_mat f *v x∥ |x. ∥x∥ = 1}"
then obtain x where x_def: "∥diag_mat f *v x∥ = r ∧ ∥x∥ = 1"
by blast
hence "r⇧2 = (∑i∈UNIV. (f i)⇧2 * (x $ i)⇧2)"
unfolding norm_vec_def L2_set_def matrix_vector_mul_diag_mat
apply (simp add: power_mult_distrib)
by (metis (no_types, lifting) x_def norm_ge_zero real_sqrt_ge_0_iff real_sqrt_pow2)
also have "... ≤ (Max {(f i)⇧2|i. i ∈ UNIV}) * (∑i∈UNIV. (x $ i)⇧2)"
using obs[of _ x] by (simp add: sum_mono sum_distrib_left)
also have "... = Max {(f i)⇧2|i. i ∈ UNIV}"
using x_def by (simp add: norm_vec_def L2_set_def)
finally have "r ≤ sqrt (Max {(f i)⇧2|i. i ∈ UNIV})"
using x_def real_le_rsqrt by blast
hence "r ≤ Max ?A"
by (subst (asm) sqrt_Max_power2_eq_max_abs[of UNIV f], simp_all)}
hence 1: "∀x∈{∥diag_mat f *v x∥ |x. ∥x∥ = 1}. x ≤ Max ?A"
unfolding diag_mat_def by blast
obtain i where i_def: "Max ?A = ∥diag_mat f *v 𝖾 i∥"
using cMax_finite_ex[of ?A] by force
hence 2: "∃x∈{∥diag_mat f *v x∥ |x. ∥x∥ = 1}. Max ?A ≤ x"
by (metis (mono_tags, lifting) abs_1 mem_Collect_eq norm_axis_eq order_refl real_norm_def)
show "Sup {∥diag_mat f *v x∥ |x. ∥x∥ = 1} = Max ?A"
by (rule cSup_eq[OF 1 2])
qed
lemma op_max_norms_eq_at_diag: "∥diag_mat f∥⇩o⇩p = ∥diag_mat f∥⇩m⇩a⇩x"
proof(rule antisym)
have "{¦f i¦ |i. i ∈ UNIV} ⊆ {¦diag_mat f $ i $ j¦ |i j. i ∈ UNIV ∧ j ∈ UNIV}"
by (smt Collect_mono diag_mat_vec_nth_simps(1))
thus "∥diag_mat f∥⇩o⇩p ≤ ∥diag_mat f∥⇩m⇩a⇩x"
unfolding op_norm_diag_mat_eq max_norm_def
by (rule Max.subset_imp) (blast, simp only: finite_image_of_finite2)
next
have "Sup {¦diag_mat f $ i $ j¦ |i j. i ∈ UNIV ∧ j ∈ UNIV} ≤ Sup {¦f i¦ |i. i ∈ UNIV}"
apply(rule cSup_least, blast, clarify, case_tac "i = j", simp)
by (rule cSup_upper, blast, simp_all) (rule cSup_upper2, auto)
thus "∥diag_mat f∥⇩m⇩a⇩x ≤ ∥diag_mat f∥⇩o⇩p"
unfolding op_norm_diag_mat_eq max_norm_def
apply (subst cSup_eq_Max[symmetric], simp only: finite_image_of_finite2, blast)
by (subst cSup_eq_Max[symmetric], simp, blast)
qed
end