Theory NN_Lipschitz_Continuous
subsection‹Neural Network Lipschitz Continuity›
theory
NN_Lipschitz_Continuous
imports
NN_Layers
"HOL-Library.Numeral_Type"
Activation_Functions
Matrix_Utils
"HOL-Analysis.Analysis"
begin
subsubsection "Lipschitz Continuity of Functions (real)"
paragraph ‹Splitting Function›
paragraph ‹Neural Network: Activations›
lemma relu_lipschitz: "1-lipschitz_on (X::real set) (relu)"
unfolding lipschitz_on_def relu_def dist_real_def
by auto
lemma identity_lipschitz: "1-lipschitz_on (X::real set) (identity)"
unfolding lipschitz_on_def identity_def dist_real_def
by auto
paragraph ‹Neural Network: Layers›
lemma input_output_lipschitz_continuous:
‹1-lipschitz_on (U::real set) (λ i. i)›
using lipschitz_intros by simp
lemma activation_lipschitz_continuous:
assumes ‹C-lipschitz_on U f›
shows ‹C-lipschitz_on U (λ i . f i)›
using assms by simp
lemma lipschitz_on_add_const:
shows "(1::real)-lipschitz_on (U::real set) (λx. x + c)"
unfolding lipschitz_on_def by simp
lemma lipschitz_on_fold_add:
shows "1-lipschitz_on (U::real set) (fold (+) xs)"
unfolding lipschitz_on_def
by (simp add: fold_plus_sum_list_rev)
lemma lipschitz_on_fold_add_zero:
shows "1-lipschitz_on (U::real set) (λ x . fold (+) [x] (0::real))"
unfolding lipschitz_on_def
by (simp add: fold_plus_sum_list_rev foldr_conv_fold)
lemma lipschitz_on_foldr_add:
shows "1-lipschitz_on (U::real set) (λ s. foldr (+) xs s)"
unfolding lipschitz_on_def
by (simp add: fold_plus_sum_list_rev foldr_conv_fold)
lemma lipschitz_on_sumlist_rev:
shows "1-lipschitz_on (U::real set) ((+) (sum_list (rev xs)))"
using fold_plus_sum_list_rev lipschitz_on_fold_add by metis
lemma lipschitz_on_sumlist:
shows "1-lipschitz_on (U::real set) ((+) (sum_list xs))"
using fold_plus_sum_list_rev lipschitz_on_fold_add
by (metis sum_list_rev)
lemma lipschitz_on_mult_const:
shows "¦c¦-lipschitz_on (U::real set) (λ x . x * c)"
unfolding lipschitz_on_def dist_real_def using abs_mult
by (metis (no_types, opaque_lifting) Orderings.order_eq_iff abs_ge_zero mult.commute
real_scaleR_def scaleR_right_diff_distrib)
lemma lipschitz_on_weighted_sum_single:
"¦w¦-lipschitz_on (U::real set) (λ x . x * w + b)"
unfolding lipschitz_on_def dist_real_def using abs_mult
by (metis Groups.mult_ac(2) abs_ge_zero add_diff_cancel_right left_diff_distrib order.refl)
lemma lipschitz_on_fold_add_zero':
shows "2-lipschitz_on (U::real set) (λ x . (fold (+) [x,x] (0::real)) + w)"
unfolding lipschitz_on_def
by (metis (no_types, lifting) ext List.fold_simps(1,2) add.commute dist_add_cancel dist_triangle_add mult.commute mult_2_right zero_le_numeral)
lemma lipschitz_on_mult_const':
shows ‹∀ x ∈ set xs . ¦c¦-lipschitz_on (set xs) (λ y . c * y)›
using lipschitz_on_mult_const
by (metis mult_commute_abs)
typedef ('a, 'nr::finite, 'nc::finite) fixed_mat =
"carrier_mat (CARD('nr)) (CARD('nc)) :: 'a mat set"
morphisms Rep_fixed_mat Abs_fixed_mat by blast
setup_lifting type_definition_fixed_mat
typedef ('a, 'n::finite) fixed_vec =
"carrier_vec (CARD('n)) :: 'a vec set"
morphisms Rep_fixed_vec Abs_fixed_vec
using vec_carrier by blast
setup_lifting type_definition_fixed_vec
definition dim_vecf :: "('a, 'n::finite) fixed_vec ⇒ nat" where
"dim_vecf v = CARD('n)"
definition dim_colf :: "('a, 'nc::finite, 'nr::finite) fixed_mat ⇒ nat" where
"dim_colf m = CARD('nc)"
definition dim_rowf :: "('a, 'nc::finite, 'nr::finite) fixed_mat ⇒ nat" where
"dim_rowf m = CARD('nr)"
definition fixed_mat_zero :: "('a::zero, 'nr::finite, 'nc::finite) fixed_mat" where
"fixed_mat_zero = Abs_fixed_mat (0⇩m (CARD('nr)) (CARD('nc)))"
definition fixed_mat_add :: "('a::plus, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat" where
"fixed_mat_add A B = Abs_fixed_mat (Rep_fixed_mat A + Rep_fixed_mat B)"
definition fixed_vec_zero :: "('a::zero, 'nr::finite ) fixed_vec" where
"fixed_vec_zero = Abs_fixed_vec (0⇩v (CARD('nr)))"
definition fixed_vec_add :: "('a::plus, 'nr::finite) fixed_vec ⇒ ('a, 'nr) fixed_vec ⇒ ('a, 'nr) fixed_vec" where
"fixed_vec_add A B = Abs_fixed_vec (Rep_fixed_vec A + Rep_fixed_vec B)"
lift_definition fixed_mat_smult :: "'a::times ⇒ ('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat"
is "λc A. c ⋅⇩m A"
using smult_carrier_mat .
lift_definition fixed_mat_index :: "('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ nat ⇒ nat ⇒ 'a"
is "λA i j. A $$ (i, j)" .
lift_definition fixed_vec_index :: "('a, 'nr::finite) fixed_vec ⇒ nat ⇒ 'a"
is "vec_index" .
lift_definition fixed_vec_smult :: "'a::times ⇒ ('a, 'nr::finite) fixed_vec ⇒ ('a, 'nr) fixed_vec"
is "λc A. c ⋅⇩v A"
using smult_carrier_mat by simp
lift_definition mult_vec_fixed_mat ::
"('a::semiring_0, 'nr::finite) fixed_vec ⇒ ('a, 'nr, 'nc::finite) fixed_mat ⇒ ('a, 'nc) fixed_vec"
(infixl "⇩f⇩v*" 70)
is "λv A. vec (dim_col A) (λi. col A i ∙ v)"
by simp
lift_definition map_fixed_vec :: "('a ⇒ 'b) ⇒ ('a, 'n::finite) fixed_vec ⇒ ('b, 'n::finite) fixed_vec"
is "map_vec :: ('a ⇒ 'b) ⇒ 'a vec ⇒ 'b vec"
by simp
lemma zero_in_carrier:
"0⇩m (CARD('nr)) (CARD('nc)) ∈ carrier_mat (CARD('nr)) (CARD('nc))"
using zero_carrier_mat by simp
lemma Rep_fixed_mat_zero [simp]:
"Rep_fixed_mat (fixed_mat_zero :: ('a::zero, 'nr::finite, 'nc::finite) fixed_mat) = 0⇩m (CARD('nr)) (CARD('nc))"
unfolding fixed_mat_zero_def
using zero_in_carrier
by (simp add: Abs_fixed_mat_inverse)
lemma Rep_fixed_mat_add [simp]:
"Rep_fixed_mat (fixed_mat_add A B) = Rep_fixed_mat A + Rep_fixed_mat B"
unfolding fixed_mat_add_def
apply (subst Abs_fixed_mat_inverse)
using Rep_fixed_mat
apply fastforce by auto
lemma Rep_fixed_vec_zero [simp]:
"Rep_fixed_vec (fixed_vec_zero :: ('a::zero, 'n::finite) fixed_vec) = 0⇩v (CARD('n))"
unfolding fixed_vec_zero_def
using zero_in_carrier
by (simp add: Abs_fixed_vec_inverse)
lemma Rep_fixed_vec_add [simp]:
"Rep_fixed_vec (fixed_vec_add A B) = Rep_fixed_vec A + Rep_fixed_vec B"
unfolding fixed_vec_add_def
apply (subst Abs_fixed_vec_inverse)
subgoal using Rep_fixed_vec
using add_carrier_vec by blast
subgoal by blast
done
lemma Rep_fixed_mat_inject: "Rep_fixed_mat A = Rep_fixed_mat B ⟹ A = B"
by (simp add: Rep_fixed_mat_inject)
lemma Rep_fixed_vec_inject: "Rep_fixed_vec A = Rep_fixed_vec B ⟹ A = B"
by (simp add: Rep_fixed_vec_inject)
lift_definition row_fixed :: "('a, 'n::finite, 'm::finite) fixed_mat ⇒ nat ⇒ ('a, 'm) fixed_vec" is
"λA i. vec (CARD('m)) (λj. A $$ (i, j))"
by simp
lift_definition col_fixed :: "('a, 'n::finite, 'm::finite) fixed_mat ⇒ nat ⇒ ('a, 'n) fixed_vec" is
"λA j. vec (CARD('n)) (λi. A $$ (i, j))"
by simp
lemma "CARD(285) = 285" by auto
instantiation fixed_mat :: (semiring_1, finite, finite) times
begin
lift_definition mat_mult :: "('a::semiring_1, 'n::finite, 'm::finite) fixed_mat ⇒
('a, 'm, 'k::finite) fixed_mat ⇒
('a, 'n, 'k) fixed_mat" is
"λA B. mat (CARD('n)) (CARD('k)) (λ(i,j).
sum_list (map (λl. A $$ (i,l) * B $$ (l,j)) [0..<CARD('m)]))"
using mat_carrier by blast
instance ..
end
instantiation fixed_mat :: ("{real_normed_vector, times, one, real_algebra_1}", finite, finite) real_normed_vector
begin
definition zero_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat" where
"zero_fixed_mat = fixed_mat_zero"
definition plus_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat" where
"plus_fixed_mat = fixed_mat_add"
definition minus_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat" where
"minus_fixed_mat A B = fixed_mat_add A (fixed_mat_smult (-1) B)"
definition uminus_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat" where
"uminus_fixed_mat A = fixed_mat_smult (-1) A"
definition scaleR_fixed_mat :: "real ⇒ ('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat" where
"scaleR_fixed_mat r A = fixed_mat_smult (of_real r) A"
definition norm_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ real" where
"norm_fixed_mat A = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index A i j))^2)"
definition dist_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat ⇒ real" where
"dist_fixed_mat A B = norm (A - B)"
definition uniformity_fixed_mat :: "(('a::{real_algebra_1,real_normed_vector}, 'nr::finite, 'nc::finite) fixed_mat × ('a, 'nr, 'nc) fixed_mat) filter" where
"uniformity_fixed_mat = (INF e∈{0<..}. principal {(x, y). dist x y < e})"
definition open_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat set ⇒ bool" where
"open_fixed_mat S = (∀x∈S. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ S)"
definition sgn_fixed_mat :: "('a, 'nr::finite, 'nc::finite) fixed_mat ⇒ ('a, 'nr, 'nc) fixed_mat" where
"sgn_fixed_mat A = (if A = 0 then 0
else scaleR (1 / norm A) A)"
lemma uminus_add: "- (A :: ('a, 'nr::finite, 'nc::finite) fixed_mat) + A = 0"
proof -
have a0: "Rep_fixed_mat A ∈ carrier_mat CARD('nr) CARD('nc)"
using Rep_fixed_mat by blast
have a1: "- (Rep_fixed_mat A) + (Rep_fixed_mat A) = 0⇩m CARD('nr) CARD('nc)"
using uminus_l_inv_mat[of "Rep_fixed_mat A" "CARD('nr)" "CARD('nc)"] a0 by simp
have a2: "- A + A = Abs_fixed_mat (Rep_fixed_mat (- A + A))"
by (simp add: Rep_fixed_mat_inverse)
have a3: "Rep_fixed_mat (- A + A) = Rep_fixed_mat (- A) + Rep_fixed_mat A"
using Rep_fixed_mat_add[of "-A" A] unfolding fixed_mat_add_def
by (simp add: plus_fixed_mat_def)
have a4: "Rep_fixed_mat (- A) = - Rep_fixed_mat A"
using fixed_mat_smult.rep_eq[of "-1" A]
unfolding uminus_fixed_mat_def fixed_mat_smult_def by auto
have a5: "Abs_fixed_mat (0⇩m CARD('nr) CARD('nc)) = Abs_fixed_mat (Rep_fixed_mat (fixed_mat_zero:: ('a, 'nr::finite, 'nc::finite) fixed_mat))"
using Rep_fixed_mat_zero unfolding fixed_mat_zero_def
by metis
have a6: "Abs_fixed_mat (Rep_fixed_mat (fixed_mat_zero:: ('a, 'nr::finite, 'nc::finite) fixed_mat)) =
( fixed_mat_zero::('a, 'nr::finite, 'nc::finite) fixed_mat)"
using Rep_fixed_mat_inverse[of "( fixed_mat_zero::('a, 'nr::finite, 'nc::finite) fixed_mat)"] by simp
have a7: "( fixed_mat_zero::('a, 'nr::finite, 'nc::finite) fixed_mat) = 0"
unfolding zero_fixed_mat_def
by simp
show ?thesis using a0 a1 a2 a3 a4 a5 a6 a7
by (smt (verit, best))
qed
lemma smult: "a *⇩R b *⇩R x = (a * b) *⇩R (x:: ('a, 'nr::finite, 'nc::finite) fixed_mat)"
proof -
have b8: "a *⇩R b *⇩R x = scaleR a (scaleR b x)"
by (simp add: scaleR_fixed_mat_def)
also have b7: "... = fixed_mat_smult (of_real a) (fixed_mat_smult (of_real b) x)"
by (simp add: scaleR_fixed_mat_def)
also have b6: "... = Abs_fixed_mat (of_real a ⋅⇩m Rep_fixed_mat (fixed_mat_smult (of_real b) x))"
by (simp add: fixed_mat_smult.rep_eq fixed_mat_smult_def)
also have b5: "... = Abs_fixed_mat (of_real a ⋅⇩m (of_real b ⋅⇩m Rep_fixed_mat x))"
by (simp add: fixed_mat_smult.rep_eq)
also have b4: "... = Abs_fixed_mat ((of_real a * of_real b) ⋅⇩m Rep_fixed_mat x)"
using mult_smult_assoc_mat Rep_fixed_mat
proof -
have "∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶
(of_real a ⋅⇩m (of_real b ⋅⇩m Rep_fixed_mat x)) $$ (i, j) =
((of_real a * of_real b) ⋅⇩m Rep_fixed_mat x) $$ (i, j)"
proof -
have a0: "∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶
(of_real a ⋅⇩m (of_real b ⋅⇩m Rep_fixed_mat x)) $$ (i, j) =
of_real a * ((of_real b ⋅⇩m Rep_fixed_mat x) $$ (i, j))"
unfolding smult_mat_def
by (metis Rep_fixed_mat carrier_matD(1) carrier_matD(2) fixed_mat_smult.rep_eq index_smult_mat(1) smult_mat_def)
have a1: "∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶
of_real a * ((of_real b ⋅⇩m Rep_fixed_mat x) $$ (i, j)) =
of_real a * (of_real b * (Rep_fixed_mat x $$ (i, j)))"
unfolding smult_mat_def index_mat_def using index_smult_mat(1)
by (metis Rep_fixed_mat carrier_matD(1) carrier_matD(2) index_mat_def smult_mat_def)
have a2: "∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶
of_real a * (of_real b * (Rep_fixed_mat x $$ (i, j)))
= (of_real a * of_real b) * (Rep_fixed_mat x $$ (i, j))"
by (simp add: mult.assoc)
have a3: " ∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶
(of_real a * of_real b) * (Rep_fixed_mat x $$ (i, j))
= ((of_real a * of_real b) ⋅⇩m Rep_fixed_mat x) $$ (i, j)"
unfolding smult_mat_def index_mat_def using index_smult_mat(1)
by (metis Rep_fixed_mat carrier_matD(1) carrier_matD(2) index_mat_def smult_mat_def)
show ?thesis using a0 a1 a2 a3 by presburger
qed
hence "of_real a ⋅⇩m (of_real b ⋅⇩m Rep_fixed_mat x) =
(of_real a * of_real b) ⋅⇩m Rep_fixed_mat x"
using mat_eq_iff Rep_fixed_mat unfolding carrier_mat_def
by (smt (verit, best) Rep_fixed_mat carrier_matD(1) carrier_matD(2) index_smult_mat(2) index_smult_mat(3))
thus ?thesis by simp
qed
also have b1: "... = Abs_fixed_mat (of_real (a * b) ⋅⇩m Rep_fixed_mat x)"
by simp
also have b0: "... = fixed_mat_smult (of_real (a * b)) x"
by (simp add: fixed_mat_smult.rep_eq fixed_mat_smult_def)
also have b3: "... = scaleR(a * b) x"
by (simp add: scaleR_fixed_mat_def)
also have b2: "... = (a * b) *⇩R x"
by (simp add: scaleR_fixed_mat_def)
show ?thesis
using b0 b1 b2 b3 b4 b5 b6 b7 b8
by argo
qed
lemma scaleR: " 1 *⇩R x =( x:: ('a, 'nr::finite, 'nc::finite) fixed_mat)"
proof -
have a0: "1 *⇩R x = scaleR 1 x"
by (simp add: scaleR_fixed_mat_def)
have a1: "... = fixed_mat_smult (of_real 1) x"
by (simp add: scaleR_fixed_mat_def)
have a2: "... = fixed_mat_smult 1 x"
by simp
have a3: "... = x"
proof -
have "fixed_mat_smult 1 x = Abs_fixed_mat (smult_mat 1 (Rep_fixed_mat x))"
by (simp add: fixed_mat_smult_def)
also have "smult_mat 1 (Rep_fixed_mat x) = Rep_fixed_mat x"
proof -
have "∀i j. i < dim_row (Rep_fixed_mat x) ∧ j < dim_col (Rep_fixed_mat x) ⟶
(smult_mat 1 (Rep_fixed_mat x)) $$ (i, j) = Rep_fixed_mat x $$ (i, j)"
by (auto simp add: smult_mat_def)
thus ?thesis by auto
qed
hence "Abs_fixed_mat (smult_mat 1 (Rep_fixed_mat x)) = Abs_fixed_mat (Rep_fixed_mat x)" by simp
also have "... = x" by (rule Rep_fixed_mat_inverse)
finally show "fixed_mat_smult 1 x = x" .
qed
show "1 *⇩R x = x"
using a0 a1 a2 a3 by simp
qed
lemma scaleR_0: " 0 *⇩R x =( 0:: ('a, 'nr::finite, 'nc::finite) fixed_mat)"
proof -
have a0: "0 *⇩R x = scaleR 0 x"
by (simp add: scaleR_fixed_mat_def)
have a1: "... = fixed_mat_smult (of_real 0) x"
by (simp add: scaleR_fixed_mat_def)
have a2: "... = fixed_mat_smult 0 x"
by simp
have a3: "... = 0"
proof -
have "fixed_mat_smult 0 x = Abs_fixed_mat (smult_mat 0 (Rep_fixed_mat x))"
by (simp add: fixed_mat_smult_def)
also have "smult_mat 0 (Rep_fixed_mat x) = (Rep_fixed_mat ( 0:: ('a, 'nr::finite, 'nc::finite) fixed_mat))"
proof -
have "0 ⋅⇩m Rep_fixed_mat x = 0⇩m (CARD('nr)) (CARD('nc))"
proof -
have "∀i j. i < dim_row (Rep_fixed_mat x) ∧ j < dim_col (Rep_fixed_mat x) ⟶
(0 ⋅⇩m Rep_fixed_mat x) $$ (i,j) = 0"
unfolding smult_mat_def by auto
then have "0 ⋅⇩m Rep_fixed_mat x = Matrix.mat CARD('nr) CARD('nc) (λij. 0)"
using Rep_fixed_mat[of x] by auto
moreover have "Matrix.mat CARD('nr) CARD('nc) (λij. 0) = 0⇩m (CARD('nr)) (CARD('nc))"
by (simp add: zero_mat_def)
ultimately show ?thesis by simp
qed
also have "... = Rep_fixed_mat (fixed_mat_zero:: ('a, 'nr::finite, 'nc::finite) fixed_mat)"
apply(subst fixed_mat_zero_def)
by (metis Rep_fixed_mat_inverse Rep_fixed_mat_zero)
finally show ?thesis unfolding zero_fixed_mat_def by blast
qed
hence "Abs_fixed_mat (smult_mat 0 (Rep_fixed_mat x)) = Abs_fixed_mat (Rep_fixed_mat ( 0:: ('a, 'nr::finite, 'nc::finite) fixed_mat))" by simp
also have "... = ( 0:: ('a, 'nr::finite, 'nc::finite) fixed_mat)"
using Rep_fixed_mat_inverse by auto
finally show "fixed_mat_smult 0 x = ( 0:: ('a, 'nr::finite, 'nc::finite) fixed_mat)" .
qed
show "0 *⇩R x = 0"
using a0 a1 a2 a3 by simp
qed
lemma norm_0: "norm (0::('a, 'nr::finite, 'nc::finite) fixed_mat) = 0"
proof -
have a0: "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}.
fixed_mat_index (0::('a, 'nr, 'nc) fixed_mat) i j = 0"
unfolding zero_fixed_mat_def fixed_mat_zero_def zero_mat_def fixed_mat_index_def
by (simp add: Abs_fixed_mat_inverse)
have "norm (0::('a, 'nr, 'nc) fixed_mat) =
sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}.
(norm (fixed_mat_index (0::('a, 'nr, 'nc) fixed_mat) i j))^2)"
by (simp add: norm_fixed_mat_def)
also have "... = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. 0^2)"
using a0 by simp
also have "... = sqrt 0" by simp
finally show ?thesis by simp
qed
lemma sgn: "sgn x = inverse (norm x) *⇩R (x::('a, 'nr::finite, 'nc::finite) fixed_mat)"
proof -
have "sgn x = (if x = 0 then 0 else scaleR (1 / norm x) x)"
by (simp add: sgn_fixed_mat_def)
show "sgn x = inverse (norm x) *⇩R x"
proof (cases "x = 0")
case True
have "inverse (norm x) *⇩R x = inverse (norm (0::('a, 'nr::finite, 'nc::finite) fixed_mat)) *⇩R 0"
using True by simp
also have "... = inverse 0 *⇩R 0"
using norm_0 using arg_cong by fast
also have "... = 0"
using scaleR_0 by simp
finally have "inverse (norm x) *⇩R x = 0" .
with True show ?thesis
by (simp add: sgn_fixed_mat_def)
next
case False
have b0: "sgn x = scaleR (1 / norm x) x"
using False by (simp add: sgn_fixed_mat_def)
have b1: "... = scaleR (inverse (norm x)) x"
by (simp add: divide_inverse)
have b2: "... = inverse (norm x) *⇩R x"
by (simp add: scaleR_fixed_mat_def)
show ?thesis using b0 b1 b2 by simp
qed
qed
lemma norm_eq_zero_iff: "(norm x = (0::real)) = (x = (0::('a, 'nr::finite, 'nc::finite) fixed_mat))"
proof
assume "norm x = 0"
have norm_def: "norm x = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2)"
by (simp add: norm_fixed_mat_def)
with ‹norm x = 0› have b0: "sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) = 0"
by simp
then have b1: "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) = 0"
by simp
then have b2: "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2 = 0"
proof -
have non_neg: "⋀i j. (norm (fixed_mat_index x i j))⇧2 ≥ 0"
by (simp add: power2_eq_square)
{
fix i j
assume i_range: "i ∈ {0..<CARD('nr)}"
assume j_range: "j ∈ {0..<CARD('nc)}"
have "(norm (fixed_mat_index x i j))⇧2 ≤ (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index x i j))⇧2)"
proof -
have a0: "(norm (fixed_mat_index x i j))⇧2 = (∑j' = 0..<CARD('nc). if j' = j then (norm (fixed_mat_index x i j))⇧2 else 0)"
using j_range by (simp add: sum.delta)
also have "... ≤ (∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i j'))⇧2)"
proof (rule sum_mono)
fix j'
assume "j' ∈ {0..<CARD('nc)}"
show "(if j' = j then (norm (fixed_mat_index x i j))⇧2 else 0) ≤ (norm (fixed_mat_index x i j'))⇧2"
proof (cases "j' = j")
case True
then show ?thesis by simp
next
case False
have "0 ≤ (norm (fixed_mat_index x i j'))⇧2" by (simp add: non_neg)
show ?thesis by simp
qed
qed
have a1: "... = (∑i' = 0..<CARD('nr). ∑j' = 0..<CARD('nc).
if i' = i then (norm (fixed_mat_index x i j'))⇧2 else 0)"
using i_range sum.delta[of "{0..<CARD('nr)}" i "λ j' . (norm (fixed_mat_index x i j'))⇧2" ]
proof -
have "(∑i' = 0..<CARD('nr). ∑j' = 0..<CARD('nc). if i' = i then (norm (fixed_mat_index x i j'))⇧2 else 0) =
(∑i' = 0..<CARD('nr). if i' = i then (∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i j'))⇧2) else 0)"
by (simp add: sum.swap)
also have "... = (if i ∈ {0..<CARD('nr)} then (∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i j'))⇧2) else 0)"
by simp
also have "... = (∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i j'))⇧2)"
using i_range by simp
finally show "(∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i j'))⇧2) =
(∑i' = 0..<CARD('nr). ∑j' = 0..<CARD('nc). if i' = i then (norm (fixed_mat_index x i j'))⇧2 else 0)"
by simp
qed
have a2: "... ≤ (∑i' = 0..<CARD('nr). ∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i' j'))⇧2)"
proof (rule sum_mono)
fix i'
assume "i' ∈ {0..<CARD('nr)}"
show "(∑j' = 0..<CARD('nc). if i' = i then (norm (fixed_mat_index x i j'))⇧2 else 0) ≤
(∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i' j'))⇧2)"
proof (cases "i' = i")
case True
then show ?thesis by simp
next
case False
have c0: "(∑j' = 0..<CARD('nc). if i' = i then (norm (fixed_mat_index x i j'))⇧2 else 0) = 0"
using False by simp
have c1: "... ≤ (∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i' j'))⇧2)"
by (simp add: sum_nonneg non_neg)
show ?thesis using c0 c1 by simp
qed
qed
show ?thesis using a0 a1 a2
using ‹(∑j' = 0..<CARD('nc). if j' = j then (norm (fixed_mat_index x i j))⇧2 else 0) ≤ (∑j' = 0..<CARD('nc). (norm (fixed_mat_index x i j'))⇧2)› by linarith
qed
with non_neg[of i j] have "(norm (fixed_mat_index x i j))⇧2 = 0"
using ‹(∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index x i j))⇧2) = 0› by linarith
}
thus b3: "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))⇧2 = 0"
by blast
qed
then have b4: "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. norm (fixed_mat_index x i j) = 0"
by (simp add: power2_eq_iff)
then have b5: "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. fixed_mat_index x i j = 0"
by simp
then have "x = 0"
proof -
have "∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶ fixed_mat_index x i j = 0"
using ‹∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. fixed_mat_index x i j = 0›
by auto
have "x = Abs_fixed_mat (Rep_fixed_mat x)"
by (simp add: Rep_fixed_mat_inverse)
also have "Rep_fixed_mat x = Matrix.mat CARD('nr) CARD('nc) (λ(i,j). fixed_mat_index x i j)"
using Rep_fixed_mat unfolding fixed_mat_index_def carrier_mat_def
by force
also have "... = Matrix.mat CARD('nr) CARD('nc) (λ(i,j). 0)"
using ‹∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶ fixed_mat_index x i j = 0›
by (simp add: mat_eq_iff)
also have "... = 0⇩m CARD('nr) CARD('nc)"
unfolding zero_mat_def by auto
also have "Abs_fixed_mat (0⇩m CARD('nr) CARD('nc)) = (fixed_mat_zero::('a, 'nr::finite, 'nc::finite) fixed_mat)"
unfolding fixed_mat_zero_def by simp
also have "fixed_mat_zero = 0"
using zero_fixed_mat_def by metis
show "x = 0"
by (simp add: calculation zero_fixed_mat_def)
qed
thus "x = 0" by simp
next
assume "x = 0"
have norm_def: "norm x = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2)"
by (simp add: norm_fixed_mat_def)
from ‹x = 0› have "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. fixed_mat_index x i j = 0"
proof -
have "∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶ fixed_mat_index x i j = 0"
by (simp add: NN_Lipschitz_Continuous.zero_fixed_mat_def ‹(x::('a, 'nr, 'nc) fixed_mat) = (0::('a, 'nr, 'nc) fixed_mat)› fixed_mat_index.rep_eq)
have "x = Abs_fixed_mat (Rep_fixed_mat x)"
by (simp add: Rep_fixed_mat_inverse)
also have "Rep_fixed_mat x = Matrix.mat CARD('nr) CARD('nc) (λ(i,j). fixed_mat_index x i j)"
using Rep_fixed_mat unfolding fixed_mat_index_def carrier_mat_def
by force
also have "... = Matrix.mat CARD('nr) CARD('nc) (λ(i,j). 0)"
using ‹∀i j. i < CARD('nr) ∧ j < CARD('nc) ⟶ fixed_mat_index x i j = 0›
by (simp add: mat_eq_iff)
also have "... = 0⇩m CARD('nr) CARD('nc)"
unfolding zero_mat_def by auto
also have "Abs_fixed_mat (0⇩m CARD('nr) CARD('nc)) = (fixed_mat_zero::('a, 'nr::finite, 'nc::finite) fixed_mat)"
unfolding fixed_mat_zero_def by simp
also have "fixed_mat_zero = 0"
using zero_fixed_mat_def by metis
show "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. fixed_mat_index x i j = 0"
using ‹∀(i::nat) j::nat. i < CARD('nr) ∧ j < CARD('nc) ⟶ fixed_mat_index (x::('a, 'nr, 'nc) fixed_mat) i j = (0::'a)› atLeast0LessThan by blast
qed
then have "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. norm (fixed_mat_index x i j) = 0"
by simp
then have "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2 = 0"
by simp
then have "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) = 0"
by simp
then have "sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) = 0"
by simp
with norm_def show "norm x = 0"
by simp
qed
lemma sum_tuple: ‹(∑ i < n. ∑ j < m . P i j) = (∑p∈ {(i,j). i < n ∧ j < m}. P (fst p) (snd p))›
apply(subst prod.split_sel, simp)
apply(subst sum.cartesian_product')
by(simp, metis lessThan_def)
lemma triangle_inequality: "norm ((x::('a, 'nr::finite, 'nc::finite) fixed_mat) + y::('a, 'nr::finite, 'nc::finite) fixed_mat) ≤ norm x + norm y"
proof -
have norm_def: "norm z = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index z i j))^2)"
for z :: "('a, 'nr::finite, 'nc::finite) fixed_mat"
by (simp add: norm_fixed_mat_def)
have component_add: "fixed_mat_index (x + y) i j = fixed_mat_index x i j + fixed_mat_index y i j"
if "i ∈ {0..<CARD('nr)}" "j ∈ {0..<CARD('nc)}" for i j
proof -
have "fixed_mat_index (x + y) i j = Rep_fixed_mat (x + y) $$ (i, j)"
by (simp add: fixed_mat_index_def)
also have "Rep_fixed_mat (x + y) $$ (i, j) = Rep_fixed_mat ((Abs_fixed_mat (Rep_fixed_mat x + Rep_fixed_mat y)::('a, 'nr::finite, 'nc::finite) fixed_mat)) $$ (i::nat, j)"
unfolding plus_fixed_mat_def fixed_mat_add_def plus_mat_def by blast
have "Rep_fixed_mat x ∈ carrier_mat CARD('nr) CARD('nc)"
by (simp add: Rep_fixed_mat)
moreover have "Rep_fixed_mat y ∈ carrier_mat CARD('nr) CARD('nc)"
by (simp add: Rep_fixed_mat)
ultimately have a0: "Rep_fixed_mat x + Rep_fixed_mat y ∈ carrier_mat CARD('nr) CARD('nc)"
by auto
hence "Rep_fixed_mat (Abs_fixed_mat (Rep_fixed_mat x + Rep_fixed_mat y)::('a, 'nr::finite, 'nc::finite) fixed_mat) = Rep_fixed_mat x + Rep_fixed_mat y"
using Abs_fixed_mat_inverse[of "Rep_fixed_mat x + Rep_fixed_mat y"] by blast
hence "Rep_fixed_mat ((Abs_fixed_mat (Rep_fixed_mat x + Rep_fixed_mat y)::('a, 'nr::finite, 'nc::finite) fixed_mat)) $$ (i, j) =
(Rep_fixed_mat x + Rep_fixed_mat y) $$ (i, j)"
by metis
also have "... = Rep_fixed_mat x $$ (i, j) + Rep_fixed_mat y $$ (i, j)"
proof -
have add_def:
"Rep_fixed_mat (fixed_mat_add x y) = Rep_fixed_mat x + Rep_fixed_mat y"
using fixed_mat_add_def Abs_fixed_mat_inverse by auto
have index_def:
"(Rep_fixed_mat x + Rep_fixed_mat y) $$ (i, j) = (Rep_fixed_mat x) $$ (i, j) + (Rep_fixed_mat y) $$ (i, j)"
proof -
have carrier_x: "Rep_fixed_mat x ∈ carrier_mat CARD('nr) CARD('nc)"
by (simp add: Rep_fixed_mat)
have carrier_y: "Rep_fixed_mat y ∈ carrier_mat CARD('nr) CARD('nc)"
by (simp add: Rep_fixed_mat)
have add_def: "Rep_fixed_mat x + Rep_fixed_mat y =
mat CARD('nr) CARD('nc) (λ(i', j'). Rep_fixed_mat x $$ (i', j') + Rep_fixed_mat y $$ (i', j'))"
using carrier_x carrier_y unfolding plus_mat_def mat_def carrier_mat_def
by (simp add: cond_case_prod_eta)
have "(Rep_fixed_mat x + Rep_fixed_mat y) $$ (i, j) =
mat CARD('nr) CARD('nc) (λ(i', j'). Rep_fixed_mat x $$ (i', j') + Rep_fixed_mat y $$ (i', j')) $$ (i, j)"
by (simp add: add_def)
moreover have "mat CARD('nr) CARD('nc) (λ(i', j'). Rep_fixed_mat x $$ (i', j') + Rep_fixed_mat y $$ (i', j')) $$ (i, j) =
(λ(i', j'). Rep_fixed_mat x $$ (i', j') + Rep_fixed_mat y $$ (i', j')) (i, j)"
using Rep_fixed_mat[of x] Rep_fixed_mat[of y] unfolding index_mat_def carrier_mat_def
by (metis (no_types, lifting) atLeastLessThan_iff index_mat(1) index_mat_def that(1) that(2))
moreover have "(λ(i', j'). Rep_fixed_mat x $$ (i', j') + Rep_fixed_mat y $$ (i', j')) (i, j) =
Rep_fixed_mat x $$ (i, j) + Rep_fixed_mat y $$ (i, j)"
by simp
show ?thesis
by (simp add: calculation(2) local.add_def)
qed
show ?thesis
using add_def index_def
by simp
qed
also have "... = fixed_mat_index x i j + fixed_mat_index y i j"
by (simp add: fixed_mat_index_def)
finally show "fixed_mat_index (x + y) i j = fixed_mat_index x i j + fixed_mat_index y i j"
by (simp add: fixed_mat_add_def fixed_mat_index.rep_eq plus_fixed_mat_def)
qed
have "norm (fixed_mat_index (x + y) i j) ≤ norm (fixed_mat_index x i j) + norm (fixed_mat_index y i j)"
if "i ∈ {0..<CARD('nr)}" "j ∈ {0..<CARD('nc)}" for i j
using component_add norm_triangle_ineq that by auto
then have component_ineq: "(norm (fixed_mat_index (x + y) i j))^2 ≤
(norm (fixed_mat_index x i j) + norm (fixed_mat_index y i j))^2"
if "i ∈ {0..<CARD('nr)}" "j ∈ {0..<CARD('nc)}" for i j
using that by simp
have expand_square: "(a + b)^2 = a^2 + 2*a*b + b^2" for a b :: real
by (simp add: power2_eq_square algebra_simps)
have component_ineq2: "(norm (fixed_mat_index (x + y) i j))^2 ≤
(norm (fixed_mat_index x i j))^2 + 2*(norm (fixed_mat_index x i j))*(norm (fixed_mat_index y i j)) +
(norm (fixed_mat_index y i j))^2"
if "i ∈ {0..<CARD('nr)}" "j ∈ {0..<CARD('nc)}" for i j
using component_ineq expand_square that by simp
have sum_ineq: "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. ((norm (fixed_mat_index x i j))^2) +
2*(norm (fixed_mat_index x i j))*(norm (fixed_mat_index y i j)) +
(norm (fixed_mat_index y i j))^2)"
proof -
have "∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}.
(norm (fixed_mat_index (x + y) i j))^2 ≤
(norm (fixed_mat_index x i j))^2 + 2*(norm (fixed_mat_index x i j))*(norm (fixed_mat_index y i j)) +
(norm (fixed_mat_index y i j))^2"
using component_ineq2 by blast
have inner_sum_mono: "∀i∈{0..<CARD('nr)}.
(∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤
(∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2 +
2 * norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j) +
(norm (fixed_mat_index y i j))^2)"
proof
fix i
assume "i ∈ {0..<CARD('nr)}"
have "∀j∈{0..<CARD('nc)}.
(norm (fixed_mat_index (x + y) i j))^2 ≤
(norm (fixed_mat_index x i j))^2 +
2 * norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j) +
(norm (fixed_mat_index y i j))^2"
using `i ∈ {0..<CARD('nr)}` component_ineq
using component_ineq2 by blast
thus "(∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤
(∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2 +
2 * norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j) +
(norm (fixed_mat_index y i j))^2)"
using sum_mono by fast
qed
have "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2 +
2 * norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j) +
(norm (fixed_mat_index y i j))^2)"
using inner_sum_mono sum_mono by fast
thus ?thesis .
qed
have sum_distribute: "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2 +
2*(norm (fixed_mat_index x i j))*(norm (fixed_mat_index y i j)) +
(norm (fixed_mat_index y i j))^2) =
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) +
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. 2*(norm (fixed_mat_index x i j))*(norm (fixed_mat_index y i j))) +
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index y i j))^2)"
by (simp add: sum.distrib)
have cs: "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. 2*(norm (fixed_mat_index x i j))*(norm (fixed_mat_index y i j))) ≤
2 * sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) *
sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index y i j))^2)"
proof -
let ?x_norm_ij = "λi j. norm (fixed_mat_index x i j)"
let ?y_norm_ij = "λi j. norm (fixed_mat_index y i j)"
let ?sum_xy = "∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). ?x_norm_ij i j * ?y_norm_ij i j"
let ?sum_x2 = "∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (?x_norm_ij i j)^2"
let ?sum_y2 = "∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (?y_norm_ij i j)^2"
have step1: "(∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). 2 * ?x_norm_ij i j * ?y_norm_ij i j) =
2 * (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). ?x_norm_ij i j * ?y_norm_ij i j)"
using sum_distrib_left[of 2 _ "{0..<CARD('nr)}" ]
proof -
let ?g = "λi. ∑j = 0..<CARD('nc). norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j)"
have "2 * (∑i = 0..<CARD('nr). ?g i) = (∑i = 0..<CARD('nr). 2 * ?g i)"
using sum_distrib_left[of 2 ?g "{0..<CARD('nr)}"] by blast
have "(∑i = 0..<CARD('nr). 2 * (∑j = 0..<CARD('nc). norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j))) =
(∑i = 0..<CARD('nr). (∑j = 0..<CARD('nc). 2 * norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j)))"
proof -
have "⋀i. 2 * (∑j = 0..<CARD('nc). norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j)) =
(∑j = 0..<CARD('nc). 2 * norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j))"
using sum_distrib_left[of 2 _ "{0..<CARD('nc)}"]
by (metis (mono_tags, lifting) Finite_Cartesian_Product.sum_cong_aux more_arith_simps(11))
thus ?thesis by simp
qed
show ?thesis using ‹2 * (∑i = 0..<CARD('nr). ?g i) = (∑i = 0..<CARD('nr). 2 * ?g i)›
and ‹(∑i = 0..<CARD('nr). 2 * (∑j = 0..<CARD('nc). norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j))) =
(∑i = 0..<CARD('nr). (∑j = 0..<CARD('nc). 2 * norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j)))›
by simp
qed
have cs_ineq: "?sum_xy^2 ≤ ?sum_x2 * ?sum_y2"
proof -
let ?all_indices = "{(i, j). i < CARD('nr) ∧ j < CARD('nc)}"
let ?x_vec = "λ(i, j). ?x_norm_ij i j"
let ?y_vec = "λ(i, j). ?y_norm_ij i j"
have rewrite_sum_xy: "?sum_xy = (∑p ∈ ?all_indices. ?x_vec p * ?y_vec p)"
apply (subst case_prod_beta)+
apply(subst sum_tuple[of "λ i j . norm (fixed_mat_index x i j) * norm (fixed_mat_index y i j)" "CARD('nc)" "CARD('nr)", symmetric])
using atLeast0LessThan by presburger
have rewrite_sum_x2: "?sum_x2 = (∑p ∈ ?all_indices. (?x_vec p)^2)"
apply (subst case_prod_beta)
apply(subst sum_tuple[of "λ i j . (norm (fixed_mat_index x i j))⇧2" "CARD('nc)" "CARD('nr)", symmetric])
using atLeast0LessThan by presburger
have rewrite_sum_y2: "?sum_y2 = (∑p ∈ ?all_indices. (?y_vec p)^2)"
apply (subst case_prod_beta)
using sum_tuple[of "λ i j . (norm (fixed_mat_index y i j))⇧2" "CARD('nc)" "CARD('nr)", symmetric]
using atLeast0LessThan by presburger
have "(∑p ∈ ?all_indices. ?x_vec p * ?y_vec p)^2 ≤
(∑p ∈ ?all_indices. (?x_vec p)^2) * (∑p ∈ ?all_indices. (?y_vec p)^2)"
using Cauchy_Schwarz_ineq_sum by blast
with rewrite_sum_xy rewrite_sum_x2 rewrite_sum_y2 show ?thesis by simp
qed
have "?sum_xy ≤ sqrt (?sum_x2 * ?sum_y2)"
using real_le_rsqrt cs_ineq by blast
also have "sqrt (?sum_x2 * ?sum_y2) = sqrt ?sum_x2 * sqrt ?sum_y2"
by (rule real_sqrt_mult)
finally have "2 * ?sum_xy ≤ 2 * sqrt ?sum_x2 * sqrt ?sum_y2"
using mult_right_mono by argo
with step1 show ?thesis by simp
qed
have norm_square_ineq: "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) +
2 * sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) *
sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index y i j))^2) +
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index y i j))^2)"
using sum_ineq sum_distribute cs by argo
have norm_square_ineq2: "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤
(norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2"
proof -
have d0: "(sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index x i j))⇧2))⇧2 =
(∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index x i j))⇧2) "
by (meson real_sqrt_pow2 sum_nonneg zero_le_power2)
have d1: "(sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index y i j))⇧2))⇧2 =
(∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index y i j))⇧2) "
by (meson real_sqrt_pow2 sum_nonneg zero_le_power2)
have "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) +
2 * sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2) *
sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index y i j))^2) +
(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index y i j))^2)"
by (rule norm_square_ineq)
also have "... = (norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2"
apply(subst norm_def[of x])+
apply(subst d0)
apply(subst norm_def[of y])+
apply(subst d1)
using power2_eq_square d0
by blast
finally show ?thesis .
qed
have "(norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2 = (norm x + norm y)^2"
by (simp add: algebra_simps power2_sum)
have "(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤ (norm x + norm y)^2"
using norm_square_ineq2 `(norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2 = (norm x + norm y)^2` by simp
have "sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤ sqrt((norm x + norm y)^2)"
using `(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤ (norm x + norm y)^2`
using real_sqrt_le_mono by blast
have "sqrt((norm x + norm y)^2) = abs (norm x + norm y)"
by (simp add: power2_eq_square)
have "sqrt((norm x + norm y)^2) = norm x + norm y"
proof -
have "norm x ≥ 0"
unfolding norm_def
by (meson norm_ge_zero real_sqrt_ge_zero sum_nonneg zero_le_power)
moreover have "norm y ≥ 0"
unfolding norm_def
by (meson norm_ge_zero real_sqrt_ge_zero sum_nonneg zero_le_power)
ultimately have "norm x + norm y ≥ 0" by simp
hence "abs (norm x + norm y) = norm x + norm y" by simp
thus ?thesis using `sqrt((norm x + norm y)^2) = abs (norm x + norm y)` by simp
qed
have "sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤ norm x + norm y"
using `sqrt(∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (x + y) i j))^2) ≤ sqrt((norm x + norm y)^2)`
`sqrt((norm x + norm y)^2) = norm x + norm y` by simp
thus "norm (x + y) ≤ norm x + norm y"
using norm_def by simp
qed
lemma norm_scaleR: "norm (a *⇩R x) = ¦a¦ * norm (x::('a, 'nr::finite, 'nc::finite) fixed_mat)"
proof -
have a0: "norm (a *⇩R x) = norm (scaleR a x)"
by (simp add: scaleR_fixed_mat_def)
have a1: "... = norm (fixed_mat_smult (of_real a) x)"
by (simp add: scaleR_fixed_mat_def)
have a2: "... = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index (fixed_mat_smult (of_real a) x) i j))^2)"
by (simp add: norm_fixed_mat_def)
have a3: "... = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm ((of_real a) * (fixed_mat_index x i j)))^2)"
proof -
have element_equality: "⋀i j. i ∈ {0..<CARD('nr)} ⟹ j ∈ {0..<CARD('nc)} ⟹
map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) (fixed_mat_smult (of_real a) x) i j =
of_real a * map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) x i j"
proof -
fix i j
assume i_range: "i ∈ {0..<CARD('nr)}"
assume j_range: "j ∈ {0..<CARD('nc)}"
have b0: "map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) (fixed_mat_smult (of_real a) x) i j =
(λA i j. A $$ (i, j)) (Rep_fixed_mat (fixed_mat_smult (of_real a) x)) i j"
by (simp add: map_fun_def)
have b1: "... = Rep_fixed_mat (fixed_mat_smult (of_real a) x) $$ (i, j)"
by simp
have b2: "... = fixed_mat_index (fixed_mat_smult (of_real a) x) i j"
using i_range j_range by (simp add: fixed_mat_index_def)
have b3: "... = of_real a * fixed_mat_index x i j"
using i_range j_range Rep_fixed_mat
unfolding fixed_mat_smult_def smult_mat_def fixed_mat_index_def map_mat_def
proof -
have f1: "∀a f. Rep_fixed_mat (fixed_mat_smult a (f::('a, 'nr, 'nc) fixed_mat)) = a ⋅⇩m Rep_fixed_mat f"
using fixed_mat_smult.rep_eq by blast
have f2: "j < card (UNIV::'nc set)"
using atLeastLessThan_iff j_range by blast
have f3: "i < card (UNIV::'nr set)"
using atLeastLessThan_iff i_range by blast
have f4: "∀f a. Abs_fixed_mat (a ⋅⇩m Rep_fixed_mat (f::('a, 'nr, 'nc) fixed_mat)) = fixed_mat_smult a f"
using f1 by (metis (no_types) Rep_fixed_mat_inverse)
have f5: "∀f. dim_col (Rep_fixed_mat (0::('a, 'nr, 'nc) fixed_mat)) = dim_col (Rep_fixed_mat (f::('a, 'nr, 'nc) fixed_mat))"
using f1 by (smt (z3) NN_Lipschitz_Continuous.scaleR_fixed_mat_def index_smult_mat(3) scaleR_0)
then have f6: "dim_col (Rep_fixed_mat (0::('a, 'nr, 'nc) fixed_mat)) = card (UNIV::'nc set)"
by (smt (z3) Rep_fixed_mat_zero dim_col_mat(1) zero_mat_def)
have "∀f. card (UNIV::'nr set) = dim_row (Rep_fixed_mat (f::('a, 'nr, 'nc) fixed_mat))"
using f1 by (smt (z3) NN_Lipschitz_Continuous.scaleR_fixed_mat_def Rep_fixed_mat_zero dim_row_mat(1) index_smult_mat(2) scaleR_0 zero_mat_def)
then show "map_fun Rep_fixed_mat id (λm n na. m $$ (n, na)) (map_fun id (map_fun Rep_fixed_mat Abs_fixed_mat) (λa m. Matrix.mat (dim_row m) (dim_col m) (λp. a * m $$ p)) (of_real a) x::('a, 'nr, 'nc) fixed_mat) i j = of_real a * map_fun Rep_fixed_mat id (λm n na. m $$ (n, na)) x i j"
using f6 f5 f4 f3 f2 f1 by (simp add: map_mat_def smult_mat_def)
qed
have b4: "... = of_real a * Rep_fixed_mat x $$ (i, j)"
using i_range j_range by (simp add: fixed_mat_index_def)
have b5: "... = of_real a * (λA i j. A $$ (i, j)) (Rep_fixed_mat x) i j"
by simp
have b6:"... = of_real a * map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) x i j"
by (simp add: map_fun_def)
show "map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) (fixed_mat_smult (of_real a) x) i j =
of_real a * map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) x i j"
using b0 b1 b2 b3 b4 b5 b6 by argo
qed
have c0: "(∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) (fixed_mat_smult (of_real a) x) i j))⇧2) =
(∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (of_real a * map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) x i j))⇧2)"
proof -
have "(∀i∈{0..<CARD('nr)}. ∀j∈{0..<CARD('nc)}.
(norm (map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) (fixed_mat_smult (of_real a) x) i j))⇧2 =
(norm (of_real a * map_fun Rep_fixed_mat id (λA i j. A $$ (i, j)) x i j))⇧2)"
using element_equality by auto
then show ?thesis by simp
qed
show ?thesis using c0
by (simp add: fixed_mat_index_def)
qed
have a4: "... = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (¦of_real a¦ * norm (fixed_mat_index x i j))^2)"
by (simp add: of_real_def)
have a5: "... = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (¦a¦ * norm (fixed_mat_index x i j))^2)"
by simp
have a6: "... = sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (¦a¦)^2 * (norm (fixed_mat_index x i j))^2)"
by (simp add: power_mult_distrib)
have a7: "... = sqrt ((¦a¦)^2 * (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2))"
by (simp add: sum_distrib_left)
have a8: "... = ¦a¦ * sqrt (∑i∈{0..<CARD('nr)}. ∑j∈{0..<CARD('nc)}. (norm (fixed_mat_index x i j))^2)"
by (simp add: real_sqrt_mult)
have a9: "... = ¦a¦ * norm x"
by (simp add: norm_fixed_mat_def)
have a10: "... = ¦a¦ * norm x"
by simp
show ?thesis using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
by linarith
qed
instance
apply standard
subgoal
using dist_fixed_mat_def by blast
subgoal
unfolding plus_fixed_mat_def fixed_mat_add_def
using Rep_fixed_mat Rep_fixed_mat_inject
by (smt (verit, del_insts) Abs_fixed_mat_inverse add_carrier_mat assoc_add_mat)
subgoal
unfolding plus_fixed_mat_def fixed_mat_add_def
by (metis Rep_fixed_mat comm_add_mat)
subgoal
unfolding zero_fixed_mat_def fixed_mat_zero_def plus_fixed_mat_def fixed_mat_add_def
using Rep_fixed_mat
by (metis Abs_fixed_mat_inverse Rep_fixed_mat_inverse left_add_zero_mat zero_carrier_mat)
subgoal using uminus_add by blast
subgoal unfolding minus_fixed_mat_def uminus_fixed_mat_def plus_fixed_mat_def
by simp
subgoal unfolding scaleR_fixed_mat_def fixed_mat_smult_def smult_mat_def using Rep_fixed_mat
by (smt (z3) Rep_fixed_mat_add Rep_fixed_mat_inverse add_smult_distrib_left_mat
fixed_mat_smult.rep_eq map_fun_apply plus_fixed_mat_def smult_mat_def)
subgoal unfolding scaleR_fixed_mat_def fixed_mat_smult_def smult_mat_def using Rep_fixed_mat
by (smt (z3) Rep_fixed_mat_add Rep_fixed_mat_inverse add_smult_distrib_right_mat eq_id_iff
fixed_mat_smult.rep_eq map_fun_apply of_real_hom.hom_add plus_fixed_mat_def smult_mat_def)
subgoal using smult by blast
subgoal using scaleR by blast
subgoal using sgn by blast
subgoal unfolding uniformity_fixed_mat_def by simp
subgoal unfolding open_fixed_mat_def by simp
subgoal using norm_eq_zero_iff by blast
subgoal using triangle_inequality by blast
subgoal using norm_scaleR by blast
done
end
instantiation fixed_vec :: ("{real_normed_vector, times, one, real_algebra_1}", finite) real_normed_vector
begin
lift_definition zero_fixed_vec :: "('a, 'b) fixed_vec" is
"zero_vec (CARD('b))"
by (simp add: carrier_vecI)
lift_definition plus_fixed_vec :: "('a, 'b) fixed_vec ⇒ ('a, 'b) fixed_vec ⇒ ('a, 'b) fixed_vec" is
"fixed_vec_add" .
definition scaleR_fixed_vec :: "real ⇒ ('a, 'b) fixed_vec ⇒ ('a, 'b) fixed_vec" where
"scaleR_fixed_vec r A = fixed_vec_smult (of_real r) A"
lift_definition uminus_fixed_vec :: "('a, 'b) fixed_vec ⇒ ('a, 'b) fixed_vec" is
"λ v. smult_vec (-1) v"
unfolding smult_vec_def by auto
lift_definition minus_fixed_vec :: "('a, 'b) fixed_vec ⇒ ('a, 'b) fixed_vec ⇒ ('a, 'b) fixed_vec" is
"λ v w. v + (smult_vec (-1) w)"
by auto
definition norm_fixed_vec :: "('a, 'b::finite) fixed_vec ⇒ real" where
"norm_fixed_vec A = sqrt (∑i∈{0..<CARD('b)} . (norm (fixed_vec_index A i))^2)"
definition sgn_fixed_vec :: "('a, 'b::finite) fixed_vec ⇒ ('a, 'b) fixed_vec" where
"sgn_fixed_vec v = (if v = 0 then 0 else scaleR (1 / norm v) v)"
definition dist_fixed_vec :: "('a, 'b) fixed_vec ⇒ ('a, 'b) fixed_vec ⇒ real" where
"dist_fixed_vec v w = norm (v - w)"
definition uniformity_fixed_vec :: "( ('a, 'b) fixed_vec × ('a, 'b) fixed_vec) filter"
where "uniformity_fixed_vec = (INF e∈{0<..}. principal {(x, y). dist x y < e})"
definition open_fixed_vec :: "('a, 'b) fixed_vec set ⇒ bool" where
"open_fixed_vec U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)"
lemma uminus_add_vec: "- (A :: ('a, 'n::finite) fixed_vec) + A = 0"
proof -
have a0: "Rep_fixed_vec A ∈ carrier_vec CARD('n)"
using Rep_fixed_vec by blast
have a1: "- (Rep_fixed_vec A) + (Rep_fixed_vec A) = 0⇩v CARD('n) "
using uminus_l_inv_vec[of "Rep_fixed_vec A" "CARD('n)" ] a0 by simp
have a2: "- A + A = Abs_fixed_vec (Rep_fixed_vec (- A + A))"
by (simp add: Rep_fixed_vec_inverse)
have a3: "Rep_fixed_vec (- A + A) = Rep_fixed_vec (- A) + Rep_fixed_vec A"
using Rep_fixed_vec_add[of "-A" A] unfolding fixed_vec_add_def
by (simp add: NN_Lipschitz_Continuous.plus_fixed_vec.rep_eq)
have a4: "Rep_fixed_vec (- A) = - Rep_fixed_vec A"
using fixed_vec_smult.rep_eq[of "-1" A]
unfolding uminus_fixed_vec_def fixed_vec_smult_def smult_vec_def
by (simp add: Matrix.uminus_vec_def NN_Lipschitz_Continuous.uminus_fixed_vec.rep_eq smult_vec_def)
have a5: "Abs_fixed_vec (0⇩v CARD('n)) = Abs_fixed_vec (Rep_fixed_vec (fixed_vec_zero:: ('a, 'n) fixed_vec))"
using Rep_fixed_vec_zero unfolding fixed_vec_zero_def
by metis
have a6: "Abs_fixed_vec (Rep_fixed_vec (fixed_vec_zero:: ('a, 'n::finite) fixed_vec)) =
( fixed_vec_zero::('a, 'n::finite) fixed_vec)"
using Rep_fixed_vec_inverse[of "( fixed_vec_zero::('a, 'n::finite) fixed_vec)"] by simp
have a7: "( fixed_vec_zero::('a, 'n::finite) fixed_vec) = 0"
unfolding zero_fixed_vec_def fixed_vec_zero_def zero_vec_def
by (simp add: Matrix.zero_vec_def NN_Lipschitz_Continuous.zero_fixed_vec_def)
show ?thesis using a0 a1 a2 a3 a4 a5 a6 a7
by (smt (verit, best))
qed
lemma smult_vec: "a *⇩R b *⇩R x = (a * b) *⇩R (x:: ('a, 'n::finite) fixed_vec)"
proof -
have b8: "a *⇩R b *⇩R x = scaleR a (scaleR b x)"
by (simp add: scaleR_fixed_vec_def)
also have b7: "... = fixed_vec_smult (of_real a) (fixed_vec_smult (of_real b) x)"
by (simp add: NN_Lipschitz_Continuous.scaleR_fixed_vec_def)
also have b6: "... = Abs_fixed_vec (of_real a ⋅⇩v Rep_fixed_vec (fixed_vec_smult (of_real b) x))"
by (simp add: fixed_vec_smult.rep_eq fixed_vec_smult_def)
also have b5: "... = Abs_fixed_vec (of_real a ⋅⇩v (of_real b ⋅⇩v Rep_fixed_vec x))"
by (simp add: fixed_vec_smult.rep_eq)
also have b4: "... = Abs_fixed_vec((of_real a * of_real b) ⋅⇩v Rep_fixed_vec x)"
using Rep_fixed_vec
by (simp add: smult_smult_assoc)
also have b1: "... = Abs_fixed_vec (of_real (a * b) ⋅⇩v Rep_fixed_vec x)"
by simp
also have b0: "... = fixed_vec_smult (of_real (a * b)) x"
by (simp add: fixed_vec_smult.rep_eq fixed_vec_smult_def)
also have b3: "... = scaleR(a * b) x"
by (simp add: NN_Lipschitz_Continuous.scaleR_fixed_vec_def)
also have b2: "... = (a * b) *⇩R x"
by (simp add: scaleR_fixed_vec_def)
show ?thesis
using b0 b1 b2 b3 b4 b5 b6 b7 b8
by argo
qed
lemma scaleR_vec: " 1 *⇩R x =( x:: ('a, 'n::finite) fixed_vec)"
proof -
have a0: "1 *⇩R x = scaleR 1 x"
by (simp add: scaleR_fixed_vec_def)
have a1: "... = fixed_vec_smult (of_real 1) x"
by (metis NN_Lipschitz_Continuous.scaleR_fixed_vec_def)
have a2: "... = fixed_vec_smult 1 x"
by simp
have a3: "... = x"
proof -
have "fixed_vec_smult 1 x = Abs_fixed_vec (smult_vec 1 (Rep_fixed_vec x))"
by (simp add: fixed_vec_smult_def)
also have "smult_vec 1 (Rep_fixed_vec x) = Rep_fixed_vec x"
by auto
hence "Abs_fixed_vec (smult_vec 1 (Rep_fixed_vec x)) = Abs_fixed_vec (Rep_fixed_vec x)" by simp
also have "... = x" by (rule Rep_fixed_vec_inverse)
finally show "fixed_vec_smult 1 x = x" .
qed
show "1 *⇩R x = x"
using a0 a1 a2 a3 by simp
qed
lemma norm_0_vec: "norm (0::('a, 'n::finite) fixed_vec) = 0"
proof -
have a0: "∀i∈{0..<CARD('n)}.
fixed_vec_index (0::('a, 'n) fixed_vec) i = 0"
unfolding fixed_vec_index_def
by (simp add: NN_Lipschitz_Continuous.zero_fixed_vec.rep_eq)
have "norm (0::('a, 'n) fixed_vec) =
sqrt (∑i∈{0..<CARD('n)}.
(norm (fixed_vec_index (0::('a, 'n) fixed_vec) i ))^2)"
by (simp add: NN_Lipschitz_Continuous.norm_fixed_vec_def a0)
also have "... = sqrt (∑i∈{0..<CARD('n)}. 0^2)"
using a0 by simp
also have "... = sqrt 0" by simp
finally show ?thesis by simp
qed
lemma scaleR_0_vec: " 0 *⇩R x =( 0:: ('a, 'n::finite) fixed_vec)"
proof -
have a0: "0 *⇩R x = scaleR 0 x"
by (simp add: scaleR_fixed_vec_def)
have a1: "... = fixed_vec_smult (of_real 0) x"
by (simp add: NN_Lipschitz_Continuous.scaleR_fixed_vec_def)
have a2: "... = fixed_vec_smult 0 x"
by simp
have a3: "... = 0"
proof -
have "fixed_vec_smult 0 x = Abs_fixed_vec (smult_vec 0 (Rep_fixed_vec x))"
by (simp add: fixed_vec_smult_def)
also have "smult_vec 0 (Rep_fixed_vec x) = (Rep_fixed_vec ( 0:: ('a, 'n::finite) fixed_vec))"
proof -
have "0 ⋅⇩v Rep_fixed_vec x = 0⇩v (CARD('n))"
proof -
have "∀i . ((i < (dim_vec (Rep_fixed_vec x))) ⟶
(((0 ⋅⇩v Rep_fixed_vec x) $ i) = 0))"
unfolding smult_mat_def by auto
then have "0 ⋅⇩v Rep_fixed_vec x = Matrix.vec CARD('n) (λij. 0)"
using Rep_fixed_vec[of x] by auto
moreover have "Matrix.vec CARD('n) (λij. 0) = 0⇩v (CARD('n))"
by (simp add: zero_vec_def)
ultimately show ?thesis by simp
qed
also have "... = Rep_fixed_vec (fixed_vec_zero:: ('a, 'n::finite) fixed_vec)"
apply(subst fixed_vec_zero_def)
by (metis Rep_fixed_vec_inverse Rep_fixed_vec_zero)
finally show ?thesis unfolding zero_fixed_vec_def
by (simp add: NN_Lipschitz_Continuous.zero_fixed_vec.rep_eq)
qed
hence "Abs_fixed_vec (smult_vec 0 (Rep_fixed_vec x)) = Abs_fixed_vec (Rep_fixed_vec ( 0:: ('a, 'n::finite) fixed_vec))" by simp
also have "... = ( 0:: ('a, 'n::finite) fixed_vec)"
using Rep_fixed_vec_inverse by auto
finally show "fixed_vec_smult 0 x = ( 0:: ('a, 'n::finite) fixed_vec)" .
qed
show "0 *⇩R x = 0"
using a0 a1 a2 a3 by simp
qed
lemma sgn_vec: "sgn x = inverse (norm x) *⇩R (x::('a, 'n::finite) fixed_vec)"
proof -
have "sgn x = (if x = 0 then 0 else scaleR (1 / norm x) x)"
by (simp add: NN_Lipschitz_Continuous.sgn_fixed_vec_def)
show "sgn x = inverse (norm x) *⇩R x"
proof (cases "x = 0")
case True
have "inverse (norm x) *⇩R x = inverse (norm (0::('a, 'n::finite) fixed_vec)) *⇩R 0"
using True by simp
also have "... = inverse 0 *⇩R 0"
using norm_0_vec
by (metis (mono_tags, lifting))
also have "... = 0"
using scaleR_0_vec by simp
finally have "inverse (norm x) *⇩R x = 0" .
with True show ?thesis
by (simp add: NN_Lipschitz_Continuous.sgn_fixed_vec_def)
next
case False
have b0: "sgn x = scaleR (1 / norm x) x"
using False by (simp add: NN_Lipschitz_Continuous.sgn_fixed_vec_def)
have b1: "... = scaleR (inverse (norm x)) x"
by (simp add: divide_inverse)
have b2: "... = inverse (norm x) *⇩R x"
by (simp add: scaleR_fixed_mat_def)
show ?thesis using b0 b1 b2 by simp
qed
qed
lemma norm_eq_zero_iff_vec: "(norm x = (0::real)) = (x = (0::('a, 'n::finite) fixed_vec))"
proof
assume "norm x = 0"
have norm_def: "norm x = sqrt (∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i))^2)"
by (simp add: NN_Lipschitz_Continuous.norm_fixed_vec_def)
with ‹norm x = 0› have b0: "sqrt (∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) = 0"
by simp
then have b1: "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i))^2) = 0"
by simp
then have b2: "∀i∈{0..<CARD('n)}. (norm (fixed_vec_index x i))^2 = 0"
proof -
have non_neg: "⋀i . (norm (fixed_vec_index x i ))⇧2 ≥ 0"
by (simp add: power2_eq_square)
thus b3: "∀i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))⇧2 = 0"
by (smt (verit, best) b1 finite_atLeastLessThan sum_nonneg_eq_0_iff)
qed
then have b4: "∀i∈{0..<CARD('n)}. norm (fixed_vec_index x i ) = 0"
by (simp add: power2_eq_iff)
then have b5: "∀i∈{0..<CARD('n)}. fixed_vec_index x i = 0"
by simp
then have "x = 0"
proof -
have "∀i . i < CARD('n) ⟶ fixed_vec_index x i = 0"
using ‹∀i∈{0..<CARD('n)}. fixed_vec_index x i = 0›
by auto
have "x = Abs_fixed_vec (Rep_fixed_vec x)"
by (simp add: Rep_fixed_vec_inverse)
also have "Rep_fixed_vec x = Matrix.vec CARD('n) (λ i. fixed_vec_index x i )"
using Rep_fixed_vec unfolding fixed_vec_index_def carrier_vec_def
by force
also have "... = Matrix.vec CARD('n) (λ i. 0)"
using ‹∀i . i < CARD('n) ⟶ fixed_vec_index x i = 0›
by (simp add: vec_eq_iff)
also have "... = 0⇩v CARD('n)"
unfolding zero_vec_def by auto
also have "Abs_fixed_vec (0⇩v CARD('n)) = (fixed_vec_zero::('a, 'n::finite) fixed_vec)"
unfolding fixed_vec_zero_def by simp
also have "fixed_vec_zero = 0"
using zero_fixed_vec_def
by (simp add: fixed_vec_zero_def)
show "x = 0"
by (simp add: calculation NN_Lipschitz_Continuous.zero_fixed_vec_def fixed_vec_zero_def)
qed
thus "x = 0" by simp
next
assume "x = 0"
have norm_def: "norm x = sqrt (∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2)"
by (simp add: NN_Lipschitz_Continuous.norm_fixed_vec_def)
from ‹x = 0› have "∀i∈{0..<CARD('n)}. fixed_vec_index x i = 0"
proof -
have "∀i . i < CARD('n) ⟶ fixed_vec_index x i = 0"
using ‹(x::('a, 'n) fixed_vec) = (0::('a, 'n) fixed_vec)›
fixed_vec_index.rep_eq
by (smt (verit) NN_Lipschitz_Continuous.zero_fixed_vec.rep_eq index_zero_vec(1))
have "x = Abs_fixed_vec (Rep_fixed_vec x)"
by (simp add: Rep_fixed_vec_inverse)
also have "Rep_fixed_vec x = Matrix.vec CARD('n) (λi. fixed_vec_index x i )"
using Rep_fixed_vec unfolding fixed_vec_index_def carrier_vec_def
by force
also have "... = Matrix.vec CARD('n) (λ i. 0)"
using ‹∀i . i < CARD('n) ⟶ fixed_vec_index x i = 0›
by (simp add: vec_eq_iff)
also have "... = 0⇩v CARD('n) "
by auto
also have "Abs_fixed_vec (0⇩v CARD('n) ) = (fixed_vec_zero::('a, 'n::finite) fixed_vec)"
unfolding fixed_vec_zero_def by simp
also have "fixed_vec_zero = 0"
using zero_fixed_vec_def
by (simp add: fixed_vec_zero_def)
show "∀i∈{0..<CARD('n)}. fixed_vec_index x i = 0"
using ‹∀(i::nat). i < CARD('n) ⟶ fixed_vec_index (x::('a, 'n) fixed_vec) i = (0::'a)› atLeast0LessThan by blast
qed
then have "∀i∈{0..<CARD('n)} . norm (fixed_vec_index x i ) = 0"
by simp
then have "∀i∈{0..<CARD('n)} . (norm (fixed_vec_index x i ))^2 = 0"
by simp
then have "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) = 0"
by simp
then have "sqrt (∑i∈{0..<CARD('n)} . (norm (fixed_vec_index x i ))^2) = 0"
by simp
with norm_def show "norm x = 0"
by simp
qed
lemma triangle_inequality_vec: "norm ((x::('a, 'n::finite) fixed_vec) + y::('a, 'n::finite) fixed_vec) ≤ norm x + norm y"
proof -
have norm_def: "norm z = sqrt (∑i∈{0..<CARD('n)}. (norm (fixed_vec_index z i ))^2)"
for z :: "('a, 'n::finite) fixed_vec"
by (simp add: NN_Lipschitz_Continuous.norm_fixed_vec_def)
have component_add: "fixed_vec_index (x + y) i = fixed_vec_index x i + fixed_vec_index y i "
if "i ∈ {0..<CARD('n)}" for i
proof -
have "fixed_vec_index (x + y) i = Rep_fixed_vec (x + y) $ i"
by (simp add: fixed_vec_index_def)
also have "Rep_fixed_vec (x + y) $ i = Rep_fixed_vec ((Abs_fixed_vec (Rep_fixed_vec x + Rep_fixed_vec y)::('a, 'n::finite) fixed_vec)) $ (i::nat)"
by (simp add: Matrix.plus_vec_def NN_Lipschitz_Continuous.plus_fixed_vec.rep_eq fixed_vec_add_def)
have "Rep_fixed_vec x ∈ carrier_vec CARD('n)"
by (simp add: Rep_fixed_vec)
moreover have "Rep_fixed_vec y ∈ carrier_vec CARD('n)"
by (simp add: Rep_fixed_vec)
ultimately have a0: "Rep_fixed_vec x + Rep_fixed_vec y ∈ carrier_vec CARD('n) "
by auto
hence "Rep_fixed_vec (Abs_fixed_vec (Rep_fixed_vec x + Rep_fixed_vec y)::('a, 'n::finite) fixed_vec) = Rep_fixed_vec x + Rep_fixed_vec y"
using Abs_fixed_vec_inverse[of "Rep_fixed_vec x + Rep_fixed_vec y"] by blast
hence "Rep_fixed_vec ((Abs_fixed_vec (Rep_fixed_vec x + Rep_fixed_vec y)::('a, 'n::finite) fixed_vec)) $ i =
(Rep_fixed_vec x + Rep_fixed_vec y) $ i"
by metis
also have "... = Rep_fixed_vec x $ i + Rep_fixed_vec y $ i"
proof -
have add_def:
"Rep_fixed_vec (fixed_vec_add x y) = Rep_fixed_vec x + Rep_fixed_vec y"
by auto
have index_def:
"(Rep_fixed_vec x + Rep_fixed_vec y) $ i = (Rep_fixed_vec x) $ i + (Rep_fixed_vec y) $ i"
proof -
have carrier_x: "Rep_fixed_vec x ∈ carrier_vec CARD('n)"
by (simp add: Rep_fixed_vec)
have carrier_y: "Rep_fixed_vec y ∈ carrier_vec CARD('n)"
by (simp add: Rep_fixed_vec)
have add_def: "Rep_fixed_vec x + Rep_fixed_vec y =
vec CARD('n) (λ i'. Rep_fixed_vec x $ i' + Rep_fixed_vec y $ i')"
using carrier_x carrier_y unfolding plus_vec_def vec_def carrier_vec_def
by (simp add: cond_case_prod_eta)
have "(Rep_fixed_vec x + Rep_fixed_vec y) $ i =
vec CARD('n) (λ i' . Rep_fixed_vec x $ i' + Rep_fixed_vec y $ i') $ i"
by (simp add: add_def)
moreover have "vec CARD('n) (λ i'. Rep_fixed_vec x $ i' + Rep_fixed_vec y $ i') $ i =
(λ i'. Rep_fixed_vec x $ i' + Rep_fixed_vec y $ i') i"
using Rep_fixed_vec[of x] Rep_fixed_vec[of y] unfolding vec_index_def carrier_vec_def
by (metis (no_types, lifting) atLeastLessThan_iff index_vec(1) vec_index_def that(1))
moreover have "(λ i' . Rep_fixed_vec x $ i' + Rep_fixed_vec y $ i') i =
Rep_fixed_vec x $ i + Rep_fixed_vec y $ i"
by simp
show ?thesis
by (simp add: calculation(2) local.add_def)
qed
show ?thesis
using add_def index_def
by simp
qed
also have "... = fixed_vec_index x i + fixed_vec_index y i "
by (simp add: fixed_vec_index_def)
finally show "fixed_vec_index (x + y) i = fixed_vec_index x i + fixed_vec_index y i "
apply (simp add: fixed_vec_add_def fixed_vec_index.rep_eq plus_fixed_vec_def)
using ‹Rep_fixed_vec (x + y) $ i = Rep_fixed_vec (Abs_fixed_vec (Rep_fixed_vec x + Rep_fixed_vec y)) $ i› by argo
qed
have "norm (fixed_vec_index (x + y) i) ≤ norm (fixed_vec_index x i ) + norm (fixed_vec_index y i )"
if "i ∈ {0..<CARD('n)}" for i
using component_add norm_triangle_ineq that by auto
then have component_ineq: "(norm (fixed_vec_index (x + y) i ))^2 ≤
(norm (fixed_vec_index x i ) + norm (fixed_vec_index y i ))^2"
if "i ∈ {0..<CARD('n)}"for i
using that by simp
have expand_square: "(a + b)^2 = a^2 + 2*a*b + b^2" for a b :: real
by (simp add: power2_eq_square algebra_simps)
have component_ineq2: "(norm (fixed_vec_index (x + y) i ))^2 ≤
(norm (fixed_vec_index x i ))^2 + 2*(norm (fixed_vec_index x i ))*(norm (fixed_vec_index y i )) +
(norm (fixed_vec_index y i ))^2"
if "i ∈ {0..<CARD('n)}" for i
using component_ineq expand_square that by simp
have sum_ineq: "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤
(∑i∈{0..<CARD('n)}. ((norm (fixed_vec_index x i ))^2) +
2*(norm (fixed_vec_index x i ))*(norm (fixed_vec_index y i )) +
(norm (fixed_vec_index y i ))^2)"
proof -
have "∀i∈{0..<CARD('n)}.
(norm (fixed_vec_index (x + y) i ))^2 ≤
(norm (fixed_vec_index x i ))^2 + 2*(norm (fixed_vec_index x i ))*(norm (fixed_vec_index y i )) +
(norm (fixed_vec_index y i ))^2"
using component_ineq2 by blast
have inner_sum_mono: "∀i∈{0..<CARD('n)}.
( (norm (fixed_vec_index (x + y) i ))^2) ≤
((norm (fixed_vec_index x i ))^2 +
2 * norm (fixed_vec_index x i ) * norm (fixed_vec_index y i ) +
(norm (fixed_vec_index y i ))^2)"
using component_ineq2 by blast
have "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤
(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2 +
2 * norm (fixed_vec_index x i ) * norm (fixed_vec_index y i ) +
(norm (fixed_vec_index y i ))^2)"
using inner_sum_mono sum_mono by fast
thus ?thesis .
qed
have sum_distribute: "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2 +
2*(norm (fixed_vec_index x i ))*(norm (fixed_vec_index y i )) +
(norm (fixed_vec_index y i ))^2) =
(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) +
(∑i∈{0..<CARD('n)}. 2*(norm (fixed_vec_index x i ))*(norm (fixed_vec_index y i ))) +
(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index y i ))^2)"
by (simp add: sum.distrib)
have cs: "(∑i∈{0..<CARD('n)}. 2*(norm (fixed_vec_index x i ))*(norm (fixed_vec_index y i ))) ≤
2 * sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) *
sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index y i))^2)"
proof -
let ?x_norm_i = "λi . norm (fixed_vec_index x i )"
let ?y_norm_i = "λi . norm (fixed_vec_index y i )"
let ?sum_xy = "∑i = 0..<CARD('n). ?x_norm_i i * ?y_norm_i i "
let ?sum_x2 = "∑i = 0..<CARD('n). (?x_norm_i i )^2"
let ?sum_y2 = "∑i = 0..<CARD('n). (?y_norm_i i )^2"
have step1: "(∑i = 0..<CARD('n). 2 * ?x_norm_i i * ?y_norm_i i ) =
2 * (∑i = 0..<CARD('n). ?x_norm_i i * ?y_norm_i i )"
using sum_distrib_left[of 2 _ "{0..<CARD('nr)}" ]
proof -
let ?g = "λi. norm (fixed_vec_index x i ) * norm (fixed_vec_index y i )"
have "2 * (∑i = 0..<CARD('n). ?g i) = (∑i = 0..<CARD('n). 2 * ?g i)"
using sum_distrib_left[of 2 ?g "{0..<CARD('nr)}"] by blast
have "(∑i = 0..<CARD('n). 2 * ( norm (fixed_vec_index x i ) * norm (fixed_vec_index y i ))) =
(∑i = 0..<CARD('n). ( 2 * norm (fixed_vec_index x i ) * norm (fixed_vec_index y i )))"
by (meson vector_space_over_itself.vector_space_assms(3))
show ?thesis using ‹2 * (∑i = 0..<CARD('n). ?g i) = (∑i = 0..<CARD('n). 2 * ?g i)›
and ‹(∑i = 0..<CARD('n). 2 * ( norm (fixed_vec_index x i ) * norm (fixed_vec_index y i ))) =
(∑i = 0..<CARD('n). ( 2 * norm (fixed_vec_index x i ) * norm (fixed_vec_index y i )))›
by simp
qed
have cs_ineq: "?sum_xy^2 ≤ ?sum_x2 * ?sum_y2"
by (simp add: Cauchy_Schwarz_ineq_sum)
have "?sum_xy ≤ sqrt (?sum_x2 * ?sum_y2)"
using real_le_rsqrt cs_ineq by blast
also have "sqrt (?sum_x2 * ?sum_y2) = sqrt ?sum_x2 * sqrt ?sum_y2"
by (rule real_sqrt_mult)
finally have "2 * ?sum_xy ≤ 2 * sqrt ?sum_x2 * sqrt ?sum_y2"
using mult_right_mono by argo
with step1 show ?thesis by simp
qed
have norm_square_ineq: "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤
(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) +
2 * sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) *
sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index y i ))^2) +
(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index y i ))^2)"
using sum_ineq sum_distribute cs by argo
have norm_square_ineq2: "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤
(norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2"
proof -
have d0: "(sqrt (∑i = 0..<CARD('n). (norm (fixed_vec_index x i ))⇧2))⇧2 =
(∑i = 0..<CARD('n). (norm (fixed_vec_index x i ))⇧2) "
by (meson real_sqrt_pow2 sum_nonneg zero_le_power2)
have d1: "(sqrt (∑i = 0..<CARD('n). (norm (fixed_vec_index y i ))⇧2))⇧2 =
(∑i = 0..<CARD('n). (norm (fixed_vec_index y i ))⇧2) "
by (meson real_sqrt_pow2 sum_nonneg zero_le_power2)
have "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤
(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) +
2 * sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2) *
sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index y i ))^2) +
(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index y i ))^2)"
by (rule norm_square_ineq)
also have "... = (norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2"
apply(subst norm_def[of x])+
apply(subst d0)
apply(subst norm_def[of y])+
apply(subst d1)
using power2_eq_square d0
by blast
finally show ?thesis .
qed
have "(norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2 = (norm x + norm y)^2"
by (simp add: algebra_simps power2_sum)
have "(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i))^2) ≤ (norm x + norm y)^2"
using norm_square_ineq2 `(norm x)^2 + 2 * (norm x) * (norm y) + (norm y)^2 = (norm x + norm y)^2` by simp
have "sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤ sqrt((norm x + norm y)^2)"
using `(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤ (norm x + norm y)^2`
using real_sqrt_le_mono by blast
have "sqrt((norm x + norm y)^2) = abs (norm x + norm y)"
by (simp add: power2_eq_square)
have "sqrt((norm x + norm y)^2) = norm x + norm y"
proof -
have "norm x ≥ 0"
unfolding norm_def
by (meson norm_ge_zero real_sqrt_ge_zero sum_nonneg zero_le_power)
moreover have "norm y ≥ 0"
unfolding norm_def
by (meson norm_ge_zero real_sqrt_ge_zero sum_nonneg zero_le_power)
ultimately have "norm x + norm y ≥ 0" by simp
hence "abs (norm x + norm y) = norm x + norm y" by simp
thus ?thesis using `sqrt((norm x + norm y)^2) = abs (norm x + norm y)` by simp
qed
have "sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤ norm x + norm y"
using `sqrt(∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (x + y) i ))^2) ≤ sqrt((norm x + norm y)^2)`
`sqrt((norm x + norm y)^2) = norm x + norm y` by simp
thus "norm (x + y) ≤ norm x + norm y"
using norm_def by simp
qed
lemma norm_scaleR_vec: "norm (a *⇩R x) = ¦a¦ * norm (x::('a, 'n::finite) fixed_vec)"
proof -
have a0: "norm (a *⇩R x) = norm (scaleR a x)"
by simp
have a1: "... = norm (fixed_vec_smult (of_real a) x)"
by (simp add: NN_Lipschitz_Continuous.scaleR_fixed_vec_def)
have a2: "... = sqrt (∑i∈{0..<CARD('n)}. (norm (fixed_vec_index (fixed_vec_smult (of_real a) x) i ))^2)"
by (simp add: NN_Lipschitz_Continuous.norm_fixed_vec_def)
have a3: "... = sqrt (∑i∈{0..<CARD('n)}. (norm ((of_real a) * (fixed_vec_index x i )))^2)"
proof -
have element_equality: "⋀i . i ∈ {0..<CARD('n)} ⟹
map_fun Rep_fixed_vec id (λA i . A $ i) (fixed_vec_smult (of_real a) x) i =
of_real a * map_fun Rep_fixed_vec id (λA i . A $ i) x i "
proof -
fix i
assume i_range: "i ∈ {0..<CARD('n)}"
have b0: "map_fun Rep_fixed_vec id (λA i . A $ i) (fixed_vec_smult (of_real a) x) i =
(λA i . A $ i ) (Rep_fixed_vec (fixed_vec_smult (of_real a) x)) i "
by (simp add: map_fun_def)
have b1: "... = Rep_fixed_vec (fixed_vec_smult (of_real a) x) $ i"
by simp
have b2: "... = fixed_vec_index (fixed_vec_smult (of_real a) x) i "
using i_range by (simp add: fixed_vec_index_def)
have b3: "... = of_real a * fixed_vec_index x i "
using i_range Rep_fixed_vec
unfolding fixed_vec_smult_def smult_vec_def fixed_vec_index_def map_vec_def
proof -
have f1: "∀a f. Rep_fixed_vec (fixed_vec_smult a (f::('a, 'n) fixed_vec)) = a ⋅⇩v Rep_fixed_vec f"
using fixed_vec_smult.rep_eq by blast
have f3: "i < card (UNIV::'n set)"
using atLeastLessThan_iff i_range by blast
have f4: "∀f a. Abs_fixed_vec (a ⋅⇩v Rep_fixed_vec (f::('a, 'n) fixed_vec)) = fixed_vec_smult a f"
using f1 by (metis (no_types) Rep_fixed_vec_inverse)
have f5: "∀f. dim_vec (Rep_fixed_vec (0::('a, 'n) fixed_vec)) = dim_vec (Rep_fixed_vec (f::('a, 'n) fixed_vec))"
using f1 by (smt (z3) NN_Lipschitz_Continuous.scaleR_fixed_vec_def index_smult_vec scaleR_0_vec)
then have f6: "dim_vec (Rep_fixed_vec (0::('a, 'n) fixed_vec)) = card (UNIV::'n set)"
by (smt (z3) Rep_fixed_vec_zero dim_vec zero_vec_def)
have "∀f. card (UNIV::'n set) = dim_vec (Rep_fixed_vec (f::('a, 'n) fixed_vec))"
using f5 f6 by force
then show "map_fun Rep_fixed_vec id (λm n. m $ n ) (map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λa m. Matrix.vec (dim_vec m) (λp. a * m $ p)) (of_real a) x::('a, 'n) fixed_vec) i
= of_real a * map_fun Rep_fixed_vec id (λm n. m $ n ) x i "
using f6 f5 f4 f3 f1 by (simp add: map_vec_def smult_vec_def)
qed
have b4: "... = of_real a * Rep_fixed_vec x $ i"
using i_range by (simp add: fixed_vec_index_def)
have b5: "... = of_real a * (λA i. A $ i) (Rep_fixed_vec x) i "
by simp
have b6:"... = of_real a * map_fun Rep_fixed_vec id (λA i . A $ i) x i "
by (simp add: map_fun_def)
show "map_fun Rep_fixed_vec id (λA i . A $ i) (fixed_vec_smult (of_real a) x) i =
of_real a * map_fun Rep_fixed_vec id (λA i . A $ i) x i "
using b0 b1 b2 b3 b4 b5 b6 by argo
qed
have c0: "(∑i = 0..<CARD('n). (norm (map_fun Rep_fixed_vec id (λA i. A $ i) (fixed_vec_smult (of_real a) x) i ))⇧2) =
(∑i = 0..<CARD('n). (norm (of_real a * map_fun Rep_fixed_vec id (λA i . A $ i) x i ))⇧2)"
using element_equality by force
show ?thesis using c0
by (simp add: fixed_vec_index_def)
qed
have a4: "... = sqrt (∑i∈{0..<CARD('n)}. (¦of_real a¦ * norm (fixed_vec_index x i ))^2)"
by (simp add: of_real_def)
have a5: "... = sqrt (∑i∈{0..<CARD('n)}. (¦a¦ * norm (fixed_vec_index x i ))^2)"
by simp
have a6: "... = sqrt (∑i∈{0..<CARD('n)}. (¦a¦)^2 * (norm (fixed_vec_index x i ))^2)"
by (simp add: power_mult_distrib)
have a7: "... = sqrt ((¦a¦)^2 * (∑i∈{0..<CARD('n)}. (norm (fixed_vec_index x i ))^2))"
by (simp add: sum_distrib_left)
have a8: "... = ¦a¦ * sqrt (∑i∈{0..<CARD('n)}.(norm (fixed_vec_index x i ))^2)"
by (simp add: real_sqrt_mult)
have a9: "... = ¦a¦ * norm x"
by (simp add: NN_Lipschitz_Continuous.norm_fixed_vec_def)
have a10: "... = ¦a¦ * norm x"
by simp
show ?thesis using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
by linarith
qed
instance
apply standard
subgoal using dist_fixed_vec_def by simp
subgoal unfolding plus_fixed_vec_def fixed_vec_add_def
using add_carrier_vec assoc_add_vec
by (smt (verit, del_insts) Abs_fixed_vec_inverse Rep_fixed_vec carrier_vec_def id_apply)
subgoal unfolding plus_fixed_vec_def fixed_vec_add_def
using Rep_fixed_vec comm_add_vec
by (metis id_def)
subgoal unfolding zero_fixed_vec_def plus_fixed_vec_def fixed_vec_add_def id_def
using Rep_fixed_vec Abs_fixed_vec_inverse Rep_fixed_vec_inverse zero_carrier_vec
by (metis left_zero_vec)
subgoal using uminus_add_vec by blast
subgoal
by (metis (mono_tags, lifting) NN_Lipschitz_Continuous.minus_fixed_vec.rep_eq
NN_Lipschitz_Continuous.plus_fixed_vec.transfer Rep_fixed_vec_inverse
fixed_vec_add_def uminus_fixed_vec.rep_eq)
subgoal
by (smt (verit) NN_Lipschitz_Continuous.scaleR_fixed_vec_def Rep_fixed_vec
Rep_fixed_vec_add fixed_vec.Rep_fixed_vec_inject fixed_vec_smult.rep_eq
plus_fixed_vec.abs_eq smult_add_distrib_vec)
subgoal
by (metis (mono_tags, opaque_lifting) NN_Lipschitz_Continuous.plus_fixed_vec.rep_eq
Rep_fixed_vec_add add_smult_distrib_vec fixed_vec.Rep_fixed_vec_inject
fixed_vec_smult.rep_eq of_real_hom.hom_add scaleR_fixed_vec_def)
subgoal using smult_vec by blast
subgoal using scaleR_vec by blast
subgoal using sgn_vec by blast
subgoal unfolding uniformity_fixed_vec_def by blast
subgoal unfolding open_fixed_vec_def by blast
subgoal using norm_eq_zero_iff_vec by blast
subgoal using triangle_inequality_vec by blast
subgoal using norm_scaleR_vec by blast
done
end
lemma uminus_fixed_vec:
assumes "(v::'a::{real_algebra_1,real_normed_vector} Matrix.vec) ∈ carrier_vec (CARD('n::finite))"
shows "- Abs_fixed_vec v = (Abs_fixed_vec (- v):: ('a::{real_algebra_1,real_normed_vector}, 'n::finite) fixed_vec)"
proof -
have "Rep_fixed_vec ((Abs_fixed_vec v):: ('a::{real_algebra_1,real_normed_vector}, 'n::finite) fixed_vec) = v"
using assms Abs_fixed_vec_inverse[of v]
by blast
hence "Rep_fixed_vec (- (Abs_fixed_vec v):: ('a::{real_algebra_1,real_normed_vector}, 'n::finite) fixed_vec) = - v"
using uminus_fixed_vec.rep_eq
proof -
have f1: "Rep_fixed_vec (Abs_fixed_vec v::('a, 'n) fixed_vec) = v"
using ‹Rep_fixed_vec (Abs_fixed_vec (v::'a Matrix.vec)) = v› by blast
have "∀f. Rep_fixed_vec (- (f::('a, 'n) fixed_vec)) = - 1 ⋅⇩v Rep_fixed_vec f"
using uminus_fixed_vec.rep_eq by blast
then show ?thesis
using f1 by auto
qed
thus ?thesis
by (metis Rep_fixed_vec_inverse)
qed
lemma lipschitz_on_mat_add:
shows ‹(1::real)-lipschitz_on U (λ (A:: ('a::{real_algebra_1,real_normed_vector}, 'nr::finite, 'nc::finite) fixed_mat) . A + M)›
by (simp add: lipschitz_onI)
lemma vec_minus_element:
fixes v w :: "'a::{minus, zero} vec"
assumes "dim_vec v = dim_vec w" and "i < dim_vec v"
shows "vec_index (v - w) i = vec_index v i - vec_index w i"
proof -
from assms have dim_eq: "dim_vec (v - w) = dim_vec v"
by simp
have "vec_index (v - w) i = vec_index (vec (dim_vec v) (λj. vec_index v j - vec_index w j)) i"
using assms by simp
also have "... = (λj. vec_index v j - vec_index w j) i"
using assms dim_eq by simp
also have "... = vec_index v i - vec_index w i"
by simp
finally show ?thesis
by (metis assms(1) assms(2) index_minus_vec(1))
qed
lemma vec_minus:
fixes v w :: "'a::{minus, zero} vec"
assumes "dim_vec v = dim_vec w" and "i < dim_vec v"
shows "(v - w) = vec (dim_vec v) (λi. vec_index v i - vec_index w i)"
proof -
have "v - w = vec (dim_vec (v - w)) (λi. vec_index (v - w) i)"
by (simp add: vec_eq_iff)
also have "dim_vec (v - w) = dim_vec v"
using assms vec_minus_element
by (metis index_minus_vec(2))
also have "Matrix.vec (dim_vec v) (λi. (v - w) $ i) = Matrix.vec (dim_vec v) (λi. v $ i - w $ i)"
using assms(1) by fastforce
finally show ?thesis by simp
qed
lemma Rep_fixed_vec_plus:
"Rep_fixed_vec ((u:: ('a::{real_algebra_1,real_normed_vector}, 'n::finite) fixed_vec) +
(v:: ('a::{real_algebra_1,real_normed_vector}, 'n::finite) fixed_vec)) =
Rep_fixed_vec u + Rep_fixed_vec v"
proof -
have "u + v ∈ {v. Rep_fixed_vec v ∈ carrier_vec (CARD('n))}"
using Rep_fixed_vec unfolding carrier_vec_def
by blast
thus "Rep_fixed_vec (u + v) = Rep_fixed_vec u + Rep_fixed_vec v"
using Rep_fixed_vec unfolding plus_fixed_vec_def
by force
qed
lemma fixed_vec_add:
assumes "v1 ∈ carrier_vec (CARD('n::finite))"
and "v2 ∈ carrier_vec (CARD('n::finite))"
shows "Abs_fixed_vec v1 + Abs_fixed_vec v2 = (Abs_fixed_vec (v1 + v2)::('a::{real_algebra_1,real_normed_vector}, 'n) fixed_vec)"
proof -
have carrier_sum: "v1 + v2 ∈ carrier_vec (CARD('n))"
using assms add_carrier_vec by blast
have "Rep_fixed_vec ((Abs_fixed_vec v1 + Abs_fixed_vec v2)::('a, 'n) fixed_vec) =
Rep_fixed_vec ((Abs_fixed_vec v1)::('a, 'n) fixed_vec) +
Rep_fixed_vec ((Abs_fixed_vec v2)::('a, 'n) fixed_vec)"
using Rep_fixed_vec_plus[of "Abs_fixed_vec v1" "Abs_fixed_vec v2"]
by blast
also have "Rep_fixed_vec ((Abs_fixed_vec v1)::('a, 'n) fixed_vec) +
Rep_fixed_vec ((Abs_fixed_vec v2)::('a, 'n) fixed_vec) =
v1 + v2"
using assms Abs_fixed_vec_inverse[of v1]
Abs_fixed_vec_inverse[of v2]
by (metis calculation)
also have "... = Rep_fixed_vec ((Abs_fixed_vec (v1 + v2))::('a, 'n) fixed_vec)"
using carrier_sum assms
by (metis Rep_fixed_vec_inverse calculation)
finally have "Rep_fixed_vec ((Abs_fixed_vec v1 + Abs_fixed_vec v2)::('a, 'n) fixed_vec) =
Rep_fixed_vec ((Abs_fixed_vec (v1 + v2))::('a, 'n) fixed_vec)" .
thus "Abs_fixed_vec v1 + Abs_fixed_vec v2 = (Abs_fixed_vec (v1 + v2)::('a, 'n) fixed_vec)"
using Rep_fixed_vec_inject by blast
qed
lemma col_minus_mat:
fixes A B :: "'a::{minus, zero} mat"
assumes "dim_row A = dim_row B" and "dim_col A = dim_col B" and "i < dim_col A"
shows "col (A - B) i = col A i - col B i"
proof -
from assms have dim_col_eq: "dim_col (A - B) = dim_col A"
by (metis index_minus_mat(3))
from assms have dim_row_eq: "dim_row (A - B) = dim_row A"
by (metis index_minus_mat(2))
have "col (A - B) i = col A i - col B i"
proof -
have "col (A - B) i = vec (dim_row (A - B)) (λj. (A - B) $$ (j, i))"
by (simp add: col_def)
also have "... = vec (dim_row A) (λj. (A - B) $$ (j, i))"
using dim_row_eq assms(1) by presburger
also have "... = vec (dim_row A) (λj. A $$ (j, i) - B $$ (j, i))"
using assms ‹(i::nat) < dim_col (A::'a mat)› by fastforce
also have "... = vec (dim_row A) (λj. A $$ (j, i)) - vec (dim_row A) (λj. B $$ (j, i))"
by (simp add: Matrix.vec_eq_iff)
also have "... = col A i - col B i"
using assms(1) col_def by metis
finally show "col (A - B) i = col A i - col B i" .
qed
show "col (A - B) i = col A i -
col B i"
using assms by auto
qed
lemma index_vec_mat_mult:
assumes "v ∈ carrier_vec (dim_row A)"
and "A ∈ carrier_mat (dim_row A) (dim_col A)"
and "i < dim_col (A::'a::{semiring_0, ab_semigroup_mult} Matrix.mat)"
shows "(v ⇩v* A) $ i = (∑j = 0..<dim_row A. v $ j * A $$ (j, i))"
proof -
have a0: "(v ⇩v* A) $ i = (Matrix.vec (dim_col A) (λk. col A k ∙ v)) $ i"
using assms unfolding mult_vec_mat_def by blast
have a1: "(Matrix.vec (dim_col A) (λk. col A k ∙ v)) $ i = (λk. col A k ∙ v) i"
using assms index_vec by blast
have a2: "... = col A i ∙ v"
using assms by blast
have a3: "... = (∑j = 0..<dim_row A. col A i $ j * v $ j)"
using assms scalar_prod_def
by (metis carrier_vecD)
have a4: "(∑j = 0..<dim_row A. col A i $ j * v $ j) = (∑j = 0..<dim_row A. A $$ (j, i) * v $ j)"
using assms index_col
by (metis (no_types, lifting) sum.ivl_cong)
have a5: "... = (∑j = 0..<dim_row A. v $ j * A $$ (j, i))"
using mult.commute by metis
show "(v ⇩v* A) $ i = (∑j = 0..<dim_row A. v $ j * A $$ (j, i))"
using a0 a1 a2 a3 a4 a5 by argo
qed
lemma Rep_fixed_mat_minus:
"Rep_fixed_mat ((x - y)::('a, 'b, 'c) fixed_mat) = Rep_fixed_mat x - Rep_fixed_mat (y:: ('a:: {real_algebra_1,real_normed_vector}, 'b::finite, 'c::finite) fixed_mat)"
proof -
have "Rep_fixed_mat (x - y) = Rep_fixed_mat (Abs_fixed_mat (Rep_fixed_mat x - Rep_fixed_mat y)::('a, 'b, 'c) fixed_mat)"
proof -
have "x - y = Abs_fixed_mat (Rep_fixed_mat x - Rep_fixed_mat y)"
proof -
have "x - y = fixed_mat_add x (fixed_mat_smult (- 1) y::('a, 'b, 'c) fixed_mat)"
using minus_fixed_mat_def by blast
also have "... = Abs_fixed_mat (Rep_fixed_mat x + Rep_fixed_mat (fixed_mat_smult (- 1) y::('a, 'b, 'c) fixed_mat))"
by (simp add: fixed_mat_add_def)
also have "... = Abs_fixed_mat (Rep_fixed_mat x + (- 1) ⋅⇩m Rep_fixed_mat (y::('a, 'b, 'c) fixed_mat))"
by (simp add: fixed_mat_smult.rep_eq)
also have "... = Abs_fixed_mat (Rep_fixed_mat x + (- Rep_fixed_mat (y::('a, 'b, 'c) fixed_mat)))"
by (smt (verit, ccfv_SIG) Rep_fixed_mat Rep_fixed_mat_add
‹Abs_fixed_mat (Rep_fixed_mat (x::('a, 'b, 'c) fixed_mat) + Rep_fixed_mat (fixed_mat_smult (- (1::'a)) (y::('a, 'b, 'c) fixed_mat))) = Abs_fixed_mat (Rep_fixed_mat x + - (1::'a) ⋅⇩m Rep_fixed_mat y)›
‹fixed_mat_add (x::('a, 'b, 'c) fixed_mat) (fixed_mat_smult (- (1::'a)) (y::('a, 'b, 'c) fixed_mat)) = Abs_fixed_mat (Rep_fixed_mat x + Rep_fixed_mat (fixed_mat_smult (- (1::'a)) y))›
assoc_add_mat calculation comm_add_mat diff_add_cancel plus_fixed_mat_def
right_add_zero_mat uminus_carrier_iff_mat uminus_l_inv_mat)
also have "... = Abs_fixed_mat (Rep_fixed_mat x - Rep_fixed_mat y)"
by (metis Rep_fixed_mat add_uminus_minus_mat)
finally show "x - y = Abs_fixed_mat (Rep_fixed_mat x - Rep_fixed_mat y)" .
qed
thus "Rep_fixed_mat ((x - y)::('a, 'b, 'c) fixed_mat) = Rep_fixed_mat ((Abs_fixed_mat (Rep_fixed_mat x - Rep_fixed_mat y))::('a, 'b, 'c) fixed_mat)"
by argo
qed
also have " Rep_fixed_mat (Abs_fixed_mat (Rep_fixed_mat x - Rep_fixed_mat y)::('a, 'b, 'c) fixed_mat) = Rep_fixed_mat x - Rep_fixed_mat y"
proof -
have "Rep_fixed_mat x ∈ carrier_mat (CARD('b)) (CARD('c))"
using Rep_fixed_mat[of x] by blast
have "Rep_fixed_mat y ∈ carrier_mat (CARD('b)) (CARD('c))"
by (rule Rep_fixed_mat)
hence "Rep_fixed_mat x - Rep_fixed_mat y ∈ carrier_mat (CARD('b)) (CARD('c))"
using ‹Rep_fixed_mat x ∈ carrier_mat (CARD('b)) (CARD('c))›
using minus_carrier_mat by blast
thus ?thesis
by (metis Abs_fixed_mat_inverse calculation)
qed
finally show "Rep_fixed_mat (x - y) = Rep_fixed_mat x - Rep_fixed_mat y" .
qed
lemma vector_matrix_inequality:
fixes c :: "('a::{real_normed_field,real_inner}, 'nr::finite) fixed_vec"
and U :: "('a, 'nr, 'nc::finite) fixed_mat set"
and C :: real
assumes C_bound: "C ≥ norm c"
and C_nonneg: "C ≥ 0"
shows "⋀x y. x ∈ U ⟹ y ∈ U ⟹
sqrt (∑i = 0..<CARD('nc). (norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i))⇧2) ≤
C * sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)"
proof -
fix x y :: "('a, 'nr, 'nc) fixed_mat"
assume x_in_U: "x ∈ U" and y_in_U: "y ∈ U"
let ?x_rep = "Rep_fixed_mat x"
let ?y_rep = "Rep_fixed_mat y"
let ?c_rep = "Rep_fixed_vec c"
have c_mult_diff: "c ⇩f⇩v* x - c ⇩f⇩v* y = Abs_fixed_vec (?c_rep ⇩v* (?x_rep - ?y_rep))"
proof -
have dim_col_eq_x_y: "dim_col (Rep_fixed_mat x) = dim_col (Rep_fixed_mat y)"
by (metis Rep_fixed_mat carrier_matD(2))
have vec_mult_x: "c ⇩f⇩v* x = Abs_fixed_vec (?c_rep ⇩v* ?x_rep)"
by (simp add: mult_vec_fixed_mat_def mult_vec_mat_def)
have vec_mult_y: "c ⇩f⇩v* y = Abs_fixed_vec (?c_rep ⇩v* ?y_rep)"
by (simp add: mult_vec_fixed_mat_def mult_vec_mat_def)
have "c ⇩f⇩v* x - c ⇩f⇩v* y = Abs_fixed_vec (?c_rep ⇩v* ?x_rep) - Abs_fixed_vec (?c_rep ⇩v* ?y_rep)"
using vec_mult_x vec_mult_y by simp
also have "... = Abs_fixed_vec ((?c_rep ⇩v* ?x_rep) - (?c_rep ⇩v* ?y_rep))"
proof -
have carrier_vx: "(?c_rep ⇩v* ?x_rep) ∈ carrier_vec (CARD('nc))"
using Rep_fixed_vec
by (metis mult_vec_fixed_mat.rep_eq mult_vec_mat_def)
have carrier_vy: "(?c_rep ⇩v* ?y_rep) ∈ carrier_vec (CARD('nc))"
using Rep_fixed_vec
by (metis mult_vec_fixed_mat.rep_eq mult_vec_mat_def)
show ?thesis
using carrier_vx carrier_vy
by (simp add: fixed_vec_add minus_add_uminus_vec pth_2 uminus_fixed_vec)
qed
also have "... = Abs_fixed_vec (?c_rep ⇩v* (?x_rep - ?y_rep))"
proof -
have "(?c_rep ⇩v* ?x_rep) - (?c_rep ⇩v* ?y_rep) = ?c_rep ⇩v* (?x_rep - ?y_rep)"
using Rep_fixed_vec Rep_fixed_mat
by (smt (verit, del_insts) Matrix.vec_eq_iff carrier_matD(1) col_dim col_minus_mat
dim_col_eq_x_y dim_mult_vec_mat index_minus_mat(3) index_minus_vec(1)
index_minus_vec(2) index_mult_vec_mat minus_scalar_prod_distrib)
thus ?thesis by simp
qed
finally show ?thesis .
qed
have vec_index_eq: "∀i < CARD('nc).
fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i = (?c_rep ⇩v* (?x_rep - ?y_rep)) $ i"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
show "fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i = (?c_rep ⇩v* (?x_rep - ?y_rep)) $ i"
using c_mult_diff
by (metis (mono_tags, lifting) Abs_fixed_vec_inverse Rep_fixed_mat carrier_matD(2)
fixed_vec_index.rep_eq index_minus_mat(3) mult_vec_mat_def vec_carrier)
qed
have vec_mult_expand: "∀i < CARD('nc).
(?c_rep ⇩v* (?x_rep - ?y_rep)) $ i = (∑j = 0..<CARD('nr). ?c_rep $ j * (?x_rep - ?y_rep) $$ (j, i))"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
show "(?c_rep ⇩v* (?x_rep - ?y_rep)) $ i = (∑j = 0..<CARD('nr). ?c_rep $ j * (?x_rep - ?y_rep) $$ (j, i))"
proof -
have carrier_c: "?c_rep ∈ carrier_vec (CARD('nr))"
by (rule Rep_fixed_vec)
have carrier_diff: "(?x_rep - ?y_rep) ∈ carrier_mat (CARD('nr)) (CARD('nc))"
using Rep_fixed_mat minus_carrier_mat by blast
show ?thesis
using carrier_c carrier_diff ‹i < CARD('nc)›
by (metis (no_types, lifting) Finite_Cartesian_Product.sum_cong_aux carrier_matD(1)
carrier_matD(2) index_vec_mat_mult)
qed
qed
have triangle_step: "(∑i = 0..<CARD('nc). (norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i))⇧2) ≤
(∑i = 0..<CARD('nc). (∑j = 0..<CARD('nr). norm (?c_rep $ j) * norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2)"
proof -
have "∀i < CARD('nc).
norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i) ≤
(∑j = 0..<CARD('nr). norm (?c_rep $ j * (?x_rep - ?y_rep) $$ (j, i)))"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
have "norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i) =
norm ((?c_rep ⇩v* (?x_rep - ?y_rep)) $ i)"
using vec_index_eq ‹i < CARD('nc)› by simp
also have "... = norm (∑j = 0..<CARD('nr). ?c_rep $ j * (?x_rep - ?y_rep) $$ (j, i))"
using vec_mult_expand ‹i < CARD('nc)› by simp
also have "... ≤ (∑j = 0..<CARD('nr). norm (?c_rep $ j * (?x_rep - ?y_rep) $$ (j, i)))"
by (rule norm_sum)
finally show "norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i) ≤
(∑j = 0..<CARD('nr). norm (?c_rep $ j * (?x_rep - ?y_rep) $$ (j, i)))" .
qed
moreover have "∀i < CARD('nc). ∀j < CARD('nr).
norm (?c_rep $ j * (?x_rep - ?y_rep) $$ (j, i)) =
norm (?c_rep $ j) * norm ((?x_rep - ?y_rep) $$ (j, i))"
using norm_mult by blast
ultimately show ?thesis
proof -
have "∀i < CARD('nc).
(norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i))⇧2 ≤
(∑j = 0..<CARD('nr). norm (Rep_fixed_vec c $ j) * norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))⇧2"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
have "norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i) ≤
(∑j = 0..<CARD('nr). norm (Rep_fixed_vec c $ j * (Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))"
using ‹∀i<CARD('nc). norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i) ≤ (∑j = 0..<CARD('nr). norm (Rep_fixed_vec c $ j * (Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))›
using ‹i < CARD('nc)› by blast
also have "... = (∑j = 0..<CARD('nr). norm (Rep_fixed_vec c $ j) * norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))"
using ‹∀i<CARD('nc). ∀j<CARD('nr). norm (Rep_fixed_vec c $ j * (Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)) = norm (Rep_fixed_vec c $ j) * norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i))›
using ‹i < CARD('nc)› by simp
finally have "norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i) ≤
(∑j = 0..<CARD('nr). norm (Rep_fixed_vec c $ j) * norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))" .
thus "(norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i))⇧2 ≤
(∑j = 0..<CARD('nr). norm (Rep_fixed_vec c $ j) * norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))⇧2"
using norm_ge_zero power_mono by blast
qed
thus ?thesis
by (meson atLeastLessThan_iff sum_mono)
qed
qed
have cauchy_schwarz_step:
"(∑i = 0..<CARD('nc). (∑j = 0..<CARD('nr). norm (?c_rep $ j) * norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2) ≤
(∑i = 0..<CARD('nc).
(∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2) *
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2))"
proof -
have "∀i < CARD('nc).
(∑j = 0..<CARD('nr). norm (?c_rep $ j) * norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2 ≤
(∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2) *
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2)"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
let ?a = "λj. norm (?c_rep $ j)"
let ?b = "λj. norm ((?x_rep - ?y_rep) $$ (j, i))"
have nonneg_a: "∀j. ?a j ≥ 0" by simp
have nonneg_b: "∀j. ?b j ≥ 0" by simp
have "(∑j = 0..<CARD('nr). ?a j * ?b j)⇧2 ≤ (∑j = 0..<CARD('nr). (?a j)⇧2) * (∑j = 0..<CARD('nr). (?b j)⇧2)"
by (simp add: Cauchy_Schwarz_ineq_sum)
thus "(∑j = 0..<CARD('nr). norm (?c_rep $ j) * norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2 ≤
(∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2) * (∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2)"
by simp
qed
thus ?thesis
by (meson atLeastLessThan_iff sum_mono)
qed
have factor_step:
"(∑i = 0..<CARD('nc).
(∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2) *
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2)) =
(∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2) *
(∑i = 0..<CARD('nc). ∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2)"
by (simp add: sum_distrib_left)
have norm_c_eq: "(∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2) = (norm c)⇧2"
proof -
have "norm c = sqrt (∑j = 0..<CARD('nr). (norm (fixed_vec_index c j))⇧2)"
unfolding norm_fixed_vec_def by blast
also have "... = sqrt (∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2)"
by (simp add: fixed_vec_index_def)
finally have "norm c = sqrt (∑j = 0..<CARD('nr). (norm (?c_rep $ j))⇧2)" .
thus ?thesis
by (metis norm_ge_zero real_sqrt_ge_0_iff real_sqrt_pow2)
qed
have reorder_step:
"(∑i = 0..<CARD('nc). ∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2) =
(∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)"
proof -
have "(∑i = 0..<CARD('nc). ∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2) =
(∑j = 0..<CARD('nr). ∑i = 0..<CARD('nc). (norm ((?x_rep - ?y_rep) $$ (j, i)))⇧2)"
by (rule sum.swap)
also have "... = (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm ((?x_rep - ?y_rep) $$ (i, j)))⇧2)"
by simp
also have "... = (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)"
proof -
have "∀i < CARD('nr). ∀j < CARD('nc).
norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (i, j)) = norm (fixed_mat_index (x - y) i j)"
proof (intro allI impI)
fix i j
assume "i < CARD('nr)" and "j < CARD('nc)"
have "fixed_mat_index (x - y) i j = Rep_fixed_mat (x - y) $$ (i, j)"
by (simp add: fixed_mat_index_def)
also have "... = (Rep_fixed_mat x - Rep_fixed_mat y) $$ (i, j)"
using Rep_fixed_mat_minus by metis
finally have "fixed_mat_index (x - y) i j = (Rep_fixed_mat x - Rep_fixed_mat y) $$ (i, j)" .
thus "norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (i, j)) = norm (fixed_mat_index (x - y) i j)"
by simp
qed
thus ?thesis
by simp
qed
then show ?thesis
using ‹(∑i = 0..<CARD('nc). ∑j = 0..<CARD('nr).
(norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))⇧2) =
(∑j = 0..<CARD('nr). ∑i = 0..<CARD('nc).
(norm ((Rep_fixed_mat x - Rep_fixed_mat y) $$ (j, i)))⇧2)› by presburger
qed
have matrix_ineq: "(∑i = 0..<CARD('nc). (norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i))⇧2) ≤
(norm c)⇧2 * (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)"
using triangle_step cauchy_schwarz_step factor_step norm_c_eq reorder_step by simp
have "sqrt (∑i = 0..<CARD('nc). (norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i))⇧2) ≤
sqrt ((norm c)⇧2 * (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2))"
using matrix_ineq real_sqrt_le_iff by blast
also have "... = norm c * sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)"
proof -
have "sqrt ((norm c)⇧2 * (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)) =
sqrt ((norm c)⇧2) * sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)"
using real_sqrt_mult by blast
also have "sqrt ((norm c)⇧2) = norm c"
by simp
finally show ?thesis by simp
qed
also have "... ≤ C * sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)"
using C_bound C_nonneg
by (metis mult_right_mono norm_fixed_mat_def norm_ge_zero)
finally show "sqrt (∑i = 0..<CARD('nc). (norm (fixed_vec_index (c ⇩f⇩v* x - c ⇩f⇩v* y) i))⇧2) ≤
C * sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index (x - y) i j))⇧2)" .
qed
lemma lipschitz_on_mat_mult:
assumes ‹0 ≤ C › and "norm c ≤ C"
shows ‹C-lipschitz_on U (λ (y::('a:: {real_inner,real_normed_field}, 'nr::finite, 'nc::finite) fixed_mat) .
( c::('a, 'nr) fixed_vec) ⇩f⇩v* y)›
unfolding mult_vec_mat_def lipschitz_on_def
apply (intro conjI impI allI)
unfolding dist_fixed_vec_def dist_fixed_mat_def
unfolding norm_fixed_vec_def norm_fixed_mat_def
subgoal using assms by blast
subgoal using vector_matrix_inequality[of c C _ U ] assms by blast
done
lemma lipschitz_on_weighted_sum_bias:
assumes ‹0 ≤ C › and "norm c ≤ C"
shows ‹C-lipschitz_on U (λ (y::('a:: {real_inner,real_normed_field}, 'nr::finite, 'nc::finite) fixed_mat) . (c ⇩f⇩v* y) + b)›
using lipschitz_on_mat_mult
proof -
have "∀F. C-lipschitz_on (F::('a, 'nr, 'nc) fixed_mat set) ((⇩f⇩v*) c)"
by (meson assms(2) lipschitz_on_le lipschitz_on_mat_mult norm_imp_pos_and_ge)
then have "∀F f. (0 + C)-lipschitz_on F (λfa. (f::('a, 'nc) fixed_vec) + c ⇩f⇩v* fa)"
using Lipschitz.lipschitz_on_constant lipschitz_on_add by blast
then have "C-lipschitz_on U (λf. b + c ⇩f⇩v* f)"
by simp
then show ?thesis
by (meson Groups.add_ac(2) lipschitz_on_cong)
qed
lemma mult_vec_mat_distrib_left:
assumes "v1 ∈ carrier_vec n" and "v2 ∈ carrier_vec n" and "A ∈ carrier_mat n m"
shows "(v1 - v2) ⇩v* A = v1 ⇩v* A - v2 ⇩v* (A:: 'a::{real_normed_field,real_inner} mat)"
proof -
have carrier_diff: "v1 - v2 ∈ carrier_vec n"
using assms by simp
have carrier_mult1: "v1 ⇩v* A ∈ carrier_vec m"
using assms
by (simp add: mult_vec_mat_def)
have carrier_mult2: "v2 ⇩v* A ∈ carrier_vec m"
using assms
by (simp add: mult_vec_mat_def)
have carrier_mult_diff: "(v1 - v2) ⇩v* A ∈ carrier_vec m"
using carrier_diff assms
using carrier_dim_vec dim_mult_vec_mat by blast
have "dim_vec ((v1 - v2) ⇩v* A) = dim_vec (v1 ⇩v* A - v2 ⇩v* A)"
using carrier_mult_diff carrier_mult1 carrier_mult2 by simp
show ?thesis
proof
show "dim_vec ((v1 - v2) ⇩v* A) = dim_vec (v1 ⇩v* A - v2 ⇩v* A)"
by (simp add: mult_vec_mat_def)
next
fix i
assume i_bound: "i < dim_vec (v1 ⇩v* A - v2 ⇩v* A)"
have i_less_m: "i < m"
using i_bound carrier_mult1 carrier_mult2 by simp
have lhs_expand: "((v1 - v2) ⇩v* A) $ i = (∑j = 0..<n. (v1 - v2) $ j * A $$ (j, i))"
using carrier_diff assms i_less_m mult_vec_mat_def
by (metis (no_types, lifting) carrier_matD(1) carrier_matD(2) index_vec_mat_mult sum.cong)
have vec_sub_expand: "(∑j = 0..<n. (v1 - v2) $ j * A $$ (j, i)) = (∑j = 0..<n. (v1 $ j - v2 $ j) * A $$ (j, i))"
using assms by simp
have mult_distrib: "(∑j = 0..<n. (v1 $ j - v2 $ j) * A $$ (j, i)) = (∑j = 0..<n. v1 $ j * A $$ (j, i) - v2 $ j * A $$ (j, i))"
by (meson vector_space_over_itself.scale_left_diff_distrib)
have sum_distrib: "(∑j = 0..<n. v1 $ j * A $$ (j, i) - v2 $ j * A $$ (j, i)) = (∑j = 0..<n. v1 $ j * A $$ (j, i)) - (∑j = 0..<n. v2 $ j * A $$ (j, i))"
by (simp add: sum_subtractf)
have back_to_mult: "(∑j = 0..<n. v1 $ j * A $$ (j, i)) - (∑j = 0..<n. v2 $ j * A $$ (j, i)) = (v1 ⇩v* A) $ i - (v2 ⇩v* A) $ i"
by (metis (mono_tags, lifting) assms(1) assms(2) assms(3) carrier_matD(1) carrier_matD(2) i_less_m index_vec_mat_mult)
have to_vec_sub: "(v1 ⇩v* A) $ i - (v2 ⇩v* A) $ i = (v1 ⇩v* A - v2 ⇩v* A) $ i"
using carrier_mult1 carrier_mult2 i_less_m by simp
show "((v1 - v2) ⇩v* A) $ i = (v1 ⇩v* A - v2 ⇩v* A) $ i"
using lhs_expand vec_sub_expand mult_distrib sum_distrib back_to_mult to_vec_sub by simp
qed
qed
lemma matrix_vector_inequality:
fixes c :: "('a::{real_normed_field,real_inner}, 'nr::finite, 'nc::finite) fixed_mat"
and U :: "('a, 'nr) fixed_vec set"
and C :: real
assumes C_bound: "C ≥ norm c"
and C_nonneg: "C ≥ 0"
shows "⋀x y. x ∈ U ⟹ y ∈ U ⟹
sqrt (∑i = 0..<CARD('nc). (norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i))⇧2) ≤
C * sqrt (∑i = 0..<CARD('nr). (norm (fixed_vec_index (x - y) i))⇧2)"
proof -
fix x y :: "('a, 'nr) fixed_vec"
assume x_in_U: "x ∈ U" and y_in_U: "y ∈ U"
let ?x_rep = "Rep_fixed_vec x"
let ?y_rep = "Rep_fixed_vec y"
let ?c_rep = "Rep_fixed_mat c"
have vec_mat_mult_diff: "x ⇩f⇩v* c - y ⇩f⇩v* c = Abs_fixed_vec (?x_rep ⇩v* ?c_rep - ?y_rep ⇩v* ?c_rep)"
proof -
have vec_mat_mult_x: "x ⇩f⇩v* c = Abs_fixed_vec (?x_rep ⇩v* ?c_rep)"
by (simp add: mult_vec_fixed_mat_def mult_vec_mat_def)
have vec_mat_mult_y: "y ⇩f⇩v* c = Abs_fixed_vec (?y_rep ⇩v* ?c_rep)"
by (simp add: mult_vec_fixed_mat_def mult_vec_mat_def)
have "x ⇩f⇩v* c - y ⇩f⇩v* c = Abs_fixed_vec (?x_rep ⇩v* ?c_rep) - Abs_fixed_vec (?y_rep ⇩v* ?c_rep)"
using vec_mat_mult_x vec_mat_mult_y by simp
also have "... = Abs_fixed_vec ((?x_rep ⇩v* ?c_rep) - (?y_rep ⇩v* ?c_rep))"
proof -
have carrier_vx: "(?x_rep ⇩v* ?c_rep) ∈ carrier_vec (CARD('nc))"
using Rep_fixed_vec
by (metis mult_vec_fixed_mat.rep_eq mult_vec_mat_def)
have carrier_vy: "(?y_rep ⇩v* ?c_rep) ∈ carrier_vec (CARD('nc))"
using Rep_fixed_vec
by (metis mult_vec_fixed_mat.rep_eq mult_vec_mat_def)
show ?thesis
using carrier_vx carrier_vy
by (simp add: fixed_vec_add minus_add_uminus_vec pth_2 uminus_fixed_vec)
qed
finally show ?thesis by simp
qed
have vec_mat_mult_linear: "?x_rep ⇩v* ?c_rep - ?y_rep ⇩v* ?c_rep = (?x_rep - ?y_rep) ⇩v* ?c_rep"
proof -
have "?x_rep ⇩v* ?c_rep - ?y_rep ⇩v* ?c_rep = (?x_rep - ?y_rep) ⇩v* ?c_rep"
using Rep_fixed_vec Rep_fixed_mat
using mult_vec_mat_distrib_left
by metis
thus ?thesis by simp
qed
have c_mult_diff: "x ⇩f⇩v* c - y ⇩f⇩v* c = Abs_fixed_vec ((?x_rep - ?y_rep) ⇩v* ?c_rep)"
using vec_mat_mult_diff vec_mat_mult_linear by simp
have vec_index_eq: "∀i < CARD('nc).
fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i = ((?x_rep - ?y_rep) ⇩v* ?c_rep) $ i"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
show "fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i = ((?x_rep - ?y_rep) ⇩v* ?c_rep) $ i"
using c_mult_diff
by (metis (mono_tags, lifting) Abs_fixed_vec_inverse Rep_fixed_mat carrier_matD(2)
fixed_vec_index.rep_eq mult_vec_mat_def vec_carrier)
qed
have vec_mat_expand: "∀i < CARD('nc).
((?x_rep - ?y_rep) ⇩v* ?c_rep) $ i = (∑j = 0..<CARD('nr). (?x_rep - ?y_rep) $ j * ?c_rep $$ (j, i))"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
show "((?x_rep - ?y_rep) ⇩v* ?c_rep) $ i = (∑j = 0..<CARD('nr). (?x_rep - ?y_rep) $ j * ?c_rep $$ (j, i))"
proof -
have carrier_diff: "(?x_rep - ?y_rep) ∈ carrier_vec (CARD('nr))"
using Rep_fixed_vec
using minus_carrier_vec by blast
have carrier_c: "?c_rep ∈ carrier_mat (CARD('nr)) (CARD('nc))"
by (rule Rep_fixed_mat)
show ?thesis
using carrier_diff carrier_c ‹i < CARD('nc)›
mult_vec_mat_def scalar_prod_def
by (simp add: index_vec_mat_mult)
qed
qed
have triangle_step: "(∑i = 0..<CARD('nc). (norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i))⇧2) ≤
(∑i = 0..<CARD('nc). (∑j = 0..<CARD('nr). norm ((?x_rep - ?y_rep) $ j) * norm (?c_rep $$ (j, i)))⇧2)"
proof -
have "∀i < CARD('nc).
norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i) ≤
(∑j = 0..<CARD('nr). norm ((?x_rep - ?y_rep) $ j * ?c_rep $$ (j, i)))"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
have "norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i) =
norm (((?x_rep - ?y_rep) ⇩v* ?c_rep) $ i)"
using vec_index_eq ‹i < CARD('nc)› by simp
also have "... = norm (∑j = 0..<CARD('nr). (?x_rep - ?y_rep) $ j * ?c_rep $$ (j, i))"
using vec_mat_expand ‹i < CARD('nc)› by simp
also have "... ≤ (∑j = 0..<CARD('nr). norm ((?x_rep - ?y_rep) $ j * ?c_rep $$ (j, i)))"
by (rule norm_sum)
finally show "norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i) ≤
(∑j = 0..<CARD('nr). norm ((?x_rep - ?y_rep) $ j * ?c_rep $$ (j, i)))" .
qed
moreover have "∀i < CARD('nc). ∀j < CARD('nr).
norm ((?x_rep - ?y_rep) $ j * ?c_rep $$ (j, i)) =
norm ((?x_rep - ?y_rep) $ j) * norm (?c_rep $$ (j, i))"
using norm_mult by blast
ultimately show ?thesis
proof -
have "∀i < CARD('nc).
(norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i))⇧2 ≤
(∑j = 0..<CARD('nr). norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j) * norm (Rep_fixed_mat c $$ (j, i)))⇧2"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
have "norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i) ≤
(∑j = 0..<CARD('nr). norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j * Rep_fixed_mat c $$ (j, i)))"
using ‹∀i<CARD('nc). norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i) ≤ (∑j = 0..<CARD('nr). norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j * Rep_fixed_mat c $$ (j, i)))›
using ‹i < CARD('nc)› by blast
also have "... = (∑j = 0..<CARD('nr). norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j) * norm (Rep_fixed_mat c $$ (j, i)))"
using ‹∀i<CARD('nc). ∀j<CARD('nr). norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j * Rep_fixed_mat c $$ (j, i)) = norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j) * norm (Rep_fixed_mat c $$ (j, i))›
using ‹i < CARD('nc)› by simp
finally have "norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i) ≤
(∑j = 0..<CARD('nr). norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j) * norm (Rep_fixed_mat c $$ (j, i)))" .
thus "(norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i))⇧2 ≤
(∑j = 0..<CARD('nr). norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ j) * norm (Rep_fixed_mat c $$ (j, i)))⇧2"
using norm_ge_zero power_mono by blast
qed
thus ?thesis
by (meson atLeastLessThan_iff sum_mono)
qed
qed
have cauchy_schwarz_step:
"(∑i = 0..<CARD('nc). (∑j = 0..<CARD('nr). norm ((?x_rep - ?y_rep) $ j) * norm (?c_rep $$ (j, i)))⇧2) ≤
(∑i = 0..<CARD('nc).
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2) *
(∑j = 0..<CARD('nr). (norm (?c_rep $$ (j, i)))⇧2))"
proof -
have "∀i < CARD('nc).
(∑j = 0..<CARD('nr). norm ((?x_rep - ?y_rep) $ j) * norm (?c_rep $$ (j, i)))⇧2 ≤
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2) *
(∑j = 0..<CARD('nr). (norm (?c_rep $$ (j, i)))⇧2)"
proof (intro allI impI)
fix i
assume "i < CARD('nc)"
let ?a = "λj. norm ((?x_rep - ?y_rep) $ j)"
let ?b = "λj. norm (?c_rep $$ (j, i))"
have nonneg_a: "∀j. ?a j ≥ 0" by simp
have nonneg_b: "∀j. ?b j ≥ 0" by simp
have "(∑j = 0..<CARD('nr). ?a j * ?b j)⇧2 ≤ (∑j = 0..<CARD('nr). (?a j)⇧2) * (∑j = 0..<CARD('nr). (?b j)⇧2)"
by (simp add: Cauchy_Schwarz_ineq_sum)
thus "(∑j = 0..<CARD('nr). norm ((?x_rep - ?y_rep) $ j) * norm (?c_rep $$ (j, i)))⇧2 ≤
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2) * (∑j = 0..<CARD('nr). (norm (?c_rep $$ (j, i)))⇧2)"
by simp
qed
thus ?thesis by (meson atLeastLessThan_iff sum_mono)
qed
have factor_step:
"(∑i = 0..<CARD('nc).
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2) *
(∑j = 0..<CARD('nr). (norm (?c_rep $$ (j, i)))⇧2)) =
(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2) *
(∑i = 0..<CARD('nc). ∑j = 0..<CARD('nr). (norm (?c_rep $$ (j, i)))⇧2)"
by (simp add: sum_distrib_left)
have norm_vec_diff_eq: "(∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2) = (norm (x - y))⇧2"
proof -
have "norm (x - y) = sqrt (∑j = 0..<CARD('nr). (norm (fixed_vec_index (x - y) j))⇧2)"
unfolding norm_fixed_vec_def by blast
also have "... = sqrt (∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2)"
proof -
have "∀j < CARD('nr). fixed_vec_index (x - y) j = (?x_rep - ?y_rep) $ j"
proof (intro allI impI)
fix j
assume "j < CARD('nr)"
show "fixed_vec_index (x - y) j = (?x_rep - ?y_rep) $ j"
proof -
have "fixed_vec_index (x - y) j = Rep_fixed_vec (x - y) $ j"
by (simp add: fixed_vec_index_def)
also have "... = (?x_rep - ?y_rep) $ j"
by (smt (verit, ccfv_threshold) Abs_fixed_vec_inverse Matrix.minus_vec_def
Rep_fixed_vec carrier_vecD fixed_vec_add minus_add_uminus_vec minus_fixed_vec.rep_eq
pth_2 uminus_fixed_vec vec_carrier zero_minus_vec)
finally show ?thesis .
qed
qed
thus ?thesis by simp
qed
finally have "norm (x - y) = sqrt (∑j = 0..<CARD('nr). (norm ((?x_rep - ?y_rep) $ j))⇧2)" .
thus ?thesis by (metis norm_ge_zero real_sqrt_ge_0_iff real_sqrt_pow2)
qed
have norm_mat_eq: "(∑i = 0..<CARD('nc). ∑j = 0..<CARD('nr). (norm (?c_rep $$ (j, i)))⇧2) = (norm c)⇧2"
proof -
have "(∑i = 0..<CARD('nc). ∑j = 0..<CARD('nr). (norm (?c_rep $$ (j, i)))⇧2) =
(∑j = 0..<CARD('nr). ∑i = 0..<CARD('nc). (norm (?c_rep $$ (j, i)))⇧2)"
by (rule sum.swap)
also have "... = (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index c i j))⇧2)"
proof -
have "∀i < CARD('nr). ∀j < CARD('nc).
norm (?c_rep $$ (i, j)) = norm (fixed_mat_index c i j)"
proof (intro allI impI)
fix i j
assume "i < CARD('nr)" and "j < CARD('nc)"
have "fixed_mat_index c i j = ?c_rep $$ (i, j)"
by (simp add: fixed_mat_index_def)
thus "norm (?c_rep $$ (i, j)) = norm (fixed_mat_index c i j)"
by simp
qed
thus ?thesis by simp
qed
also have "... = (norm c)⇧2"
proof -
have "norm c = sqrt (∑i = 0..<CARD('nr). ∑j = 0..<CARD('nc). (norm (fixed_mat_index c i j))⇧2)"
unfolding norm_fixed_mat_def by blast
thus ?thesis by (metis norm_ge_zero real_sqrt_ge_0_iff real_sqrt_pow2)
qed
finally show ?thesis .
qed
have matrix_ineq: "(∑i = 0..<CARD('nc). (norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i))⇧2) ≤
(norm (x - y))⇧2 * (norm c)⇧2"
using triangle_step cauchy_schwarz_step factor_step norm_vec_diff_eq norm_mat_eq by simp
have "sqrt (∑i = 0..<CARD('nc). (norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i))⇧2) ≤
sqrt ((norm (x - y))⇧2 * (norm c)⇧2)"
using matrix_ineq
using real_sqrt_le_iff by blast
also have "... = norm (x - y) * norm c"
proof -
have "sqrt ((norm (x - y))⇧2 * (norm c)⇧2) = sqrt ((norm (x - y))⇧2) * sqrt ((norm c)⇧2)"
by (rule real_sqrt_mult)
also have "... = norm (x - y) * norm c"
by simp
finally show ?thesis by simp
qed
also have "... = norm c * norm (x - y)"
by (simp add: mult.commute)
also have "... ≤ C * norm (x - y)"
using C_bound C_nonneg by (simp add: mult_right_mono norm_ge_zero)
also have "... = C * sqrt ((norm (x - y))⇧2)"
by simp
also have "... = C * sqrt (∑i = 0..<CARD('nr). (norm (fixed_vec_index (x - y) i))⇧2)"
proof -
have "norm (x - y) = sqrt (∑i = 0..<CARD('nr). (norm (fixed_vec_index (x - y) i))⇧2)"
unfolding norm_fixed_vec_def by blast
thus ?thesis
using ‹(C::real) * norm ((x::('a, 'nr) fixed_vec) - (y::('a, 'nr) fixed_vec)) = C * sqrt ((norm (x - y))⇧2)› by presburger
qed
finally show "sqrt (∑i = 0..<CARD('nc). (norm (fixed_vec_index (x ⇩f⇩v* c - y ⇩f⇩v* c) i))⇧2) ≤
C * sqrt (∑i = 0..<CARD('nr). (norm (fixed_vec_index (x - y) i))⇧2)" .
qed
lemma lipschitz_on_vec_mult:
assumes ‹0 ≤ C › and "norm c ≤ C"
shows ‹C-lipschitz_on U (λ y . y ⇩f⇩v* (c::('a:: {real_inner,real_normed_field}, 'nr::finite, 'nc::finite) fixed_mat))›
unfolding mult_vec_mat_def lipschitz_on_def
apply (intro conjI impI allI)
unfolding dist_fixed_vec_def dist_fixed_mat_def
unfolding norm_fixed_vec_def norm_fixed_mat_def
subgoal using assms by blast
subgoal using matrix_vector_inequality[of c C _ U _]
using assms(1) assms(2) by blast
done
lemma C_ge_norm:
"norm (c::('a:: {real_algebra_1,real_normed_vector}, 'nr::finite, 'nc::finite) fixed_mat) ≤ C ⟹ 0 ≤ C"
by (smt (verit, ccfv_SIG) norm_ge_zero)
lemma lipschitz_on_weighted_sum_bias':
assumes "norm c ≤ C"
shows ‹C-lipschitz_on U (λ y . (y ⇩f⇩v* (c::('a:: {real_inner,real_normed_field}, 'nr::finite, 'nc::finite) fixed_mat)) + b)›
using lipschitz_on_vec_mult assms C_ge_norm[of c C, simplified assms, simplified]
using Lipschitz.lipschitz_on_constant lipschitz_on_add
by fastforce
lemma lipschitz_on_dense:
assumes "norm c ≤ C"
assumes "D-lipschitz_on ((λy. (c::('a:: {real_inner,real_normed_field}, 'n::finite) fixed_vec) ⇩f⇩v* y + b) ` U) f"
shows "(D * C)-lipschitz_on U (λ y . f ((c ⇩f⇩v* y) + b))"
using lipschitz_on_weighted_sum_bias[of D c ]
using lipschitz_on_compose2[of D "U" "λ y . (c ⇩f⇩v* y) + b" C f, simplified assms]
using assms(1) assms(2) lipschitz_on_compose2 lipschitz_on_weighted_sum_bias
proof -
have "0 ≤ C"
by (meson assms(1) landau_o.R_trans norm_ge_zero)
then show ?thesis
using assms(1) assms(2) lipschitz_on_compose2 lipschitz_on_weighted_sum_bias by blast
qed
lemma lipschitz_on_dense':
assumes "norm c ≤ C"
assumes "D-lipschitz_on ((λy. y ⇩f⇩v* (c::('a:: {real_inner,real_normed_field}, 'nr::finite, 'nc::finite) fixed_mat) + b) ` U) f"
shows "(D * C)-lipschitz_on U (λ y . f ((y ⇩f⇩v* c) + b))"
using lipschitz_on_weighted_sum_bias[of D _ _ b ]
using lipschitz_on_compose2[of D "U" "λ y . (y ⇩f⇩v* c) + b" C f, simplified assms]
using assms(1) assms(2) lipschitz_on_compose2 lipschitz_on_weighted_sum_bias
using lipschitz_on_weighted_sum_bias' by blast
lemma lipschitz_on_input_ouput:
shows "1-lipschitz_on U (λ i . i)"
unfolding lipschitz_on_def by simp
lemma lipschhitz_on_activation:
assumes "C-lipschitz_on U f"
shows "C-lipschitz_on U (λ i . f i)"
using assms by simp
paragraph ‹Neural Network: Layers›
fun predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f :: "(('a::{real_algebra_1,real_normed_vector}, 'b::finite) fixed_vec, 'c, 'd) neural_network_seq_layers
⇒ ('a, 'b::finite) fixed_vec ⇒ (('a, 'b) fixed_vec, 'c, ('a, 'b, 'b) fixed_mat) layer ⇒ ('a, 'b) fixed_vec "
where
‹predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N (vs) (In l) = vs ›
| ‹predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N (vs) (Out l) = vs›
| ‹predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N (vs) (Dense pl) = ((the (activation_tab N (φ pl))) ((vs ⇩f⇩v* ω pl) + β pl)) ›
| ‹predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N (vs) (Activation pl) = ((the (activation_tab N (φ pl))) vs) ›
definition ‹predict⇩s⇩e⇩q⇩_⇩l⇩a⇩y⇩e⇩r_⇩f N inputs = foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) inputs (layers N)›
definition ‹lipschitz_continuous_activation_tab⇩f tab U = (∀ f ∈ ran (tab). ∃ C. C-lipschitz_on U f)›
lemma input_layer_lipschitz_on:
"1-lipschitz_on U ((λ vs . (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs (In x1))))"
by (simp add: lipschitz_on_def)
lemma output_layer_lipschitz_on:
"1-lipschitz_on U ((λ vs . (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs (Out x1))))"
by (simp add: lipschitz_on_def)
lemma dense_layer_lipschitz_on:
assumes "norm (ω x1) ≤ C"
assumes "D-lipschitz_on ((λy. y ⇩f⇩v* ω x1 + β x1) ` U) (the (activation_tab N (φ x1)))"
shows "(C * D)-lipschitz_on U (λ vs::('a:: {real_inner,real_normed_field}, 'c::finite) fixed_vec . (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs (Dense x1)))"
using predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f.simps(3)[of N _ x1]
using lipschitz_on_dense'[of "ω x1" C D "β x1" U, simplified assms]
by (metis (no_types, lifting) assms(2) lipschitz_on_transform mult_commute_abs)
lemma activation_layer_lipschitz_on:
assumes "C-lipschitz_on U (the (activation_tab N (φ x1)))"
shows "C-lipschitz_on U (λ vs . (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs (Activation x1)))"
using assms by simp
lemma foldl_layer_lipschitz_on:
fixes N :: "(('a::{real_algebra_1,real_normed_vector}, 'b::finite) fixed_vec, 'c, 'd) neural_network_seq_layers"
assumes layer_lipschitz: "∀l ∈ set ls. ∃C. C-lipschitz_on U (λvs. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l)"
assumes domain_invariant: "∀l ∈ set ls. ∀vs ∈ U. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l ∈ U"
shows "∃C. C-lipschitz_on U (λvs. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) vs ls)"
using assms
proof (induction ls )
case Nil
then show ?case
by (auto simp: lipschitz_on_def intro: exI[where x=1])
next
case (Cons l ls)
have l: "l ∈ set (l#ls)" using Cons by simp
obtain C1 where h1: "C1-lipschitz_on U (λvs. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l)"
using Cons(2) by auto
obtain C2 where h2: "C2-lipschitz_on U (λvs. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) vs ls)"
using Cons by auto
have fold_step: "∀vs. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) vs (l # ls) =
foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l) ls"
by simp
have composition: "∀vs. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) vs (l # ls) =
(λx. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) x ls) (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l)"
using fold_step by simp
have image_in_domain: "(λvs. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l) ` U ⊆ U"
using Cons(1) h1 h2
using l local.Cons(3) by fastforce
have "(C1 * C2)-lipschitz_on U (λvs. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) vs (l # ls))"
using lipschitz_on_compose[of C1 U "(λvs. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l)" C2 "(λvs. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) vs ls)", simplified h1, simplified]
image_in_domain composition
proof -
have "(C2 * C1)-lipschitz_on U (λf. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) f (l # ls))"
using ‹C2-lipschitz_on ((λvs. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l) ` U) (λvs. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) vs ls) ⟹ (C2 * C1)-lipschitz_on U (λx. foldl (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N) (predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N x l) ls)› h2 image_in_domain lipschitz_on_subset by force
then show ?thesis
by argo
qed
thus ?case by auto
qed
lemma layers_lipschitz_from_components:
fixes N :: "(('a::{real_algebra_1,real_normed_vector,real_inner,real_normed_field}, 'b::finite) fixed_vec, 'c, 'd) neural_network_seq_layers"
assumes weight_bounded: "∀l ∈ set ls. (case l of Dense pl ⇒ norm (ω pl) ≤ W )"
assumes activation_lipschitz: "∀l ∈ set ls. (case l of
Dense pl ⇒ ∃D. D-lipschitz_on ((λy. y ⇩f⇩v* ω pl + β pl) ` U) (the (activation_tab N (φ pl))) |
Activation pl ⇒ ∃C. C-lipschitz_on U (the (activation_tab N (φ pl))))"
shows "∀l ∈ set ls. ∃C. C-lipschitz_on U (λvs. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l)"
proof
fix l assume "l ∈ set ls"
show "∃C. C-lipschitz_on U (λvs. predict⇩l⇩a⇩y⇩e⇩r⇩_⇩f N vs l)"
proof (cases l)
case (In x)
then show ?thesis using input_layer_lipschitz_on by blast
next
case (Out x)
then show ?thesis using output_layer_lipschitz_on by blast
next
case (Dense x)
obtain D where "D-lipschitz_on ((λy. y ⇩f⇩v* ω x + β x) ` U) (the (activation_tab N (φ x)))"
using activation_lipschitz Dense ‹l ∈ set ls›
by fastforce
moreover have "norm (ω x) ≤ W"
using weight_bounded Dense ‹l ∈ set ls› by auto
ultimately show ?thesis
using dense_layer_lipschitz_on[of x W D U N] Dense
by auto
next
case (Activation x)
obtain C where "C-lipschitz_on U (the (activation_tab N (φ x)))"
using activation_lipschitz Activation ‹l ∈ set ls› by fastforce
then show ?thesis
using activation_layer_lipschitz_on Activation
by auto
qed
qed
lemma Rep_fixed_vec_minus: "Rep_fixed_vec (x - y) = Rep_fixed_vec x - Rep_fixed_vec y"
proof -
have "x - y = Abs_fixed_vec (Rep_fixed_vec x + smult_vec (-1) (Rep_fixed_vec y))"
unfolding minus_fixed_vec_def minus_fixed_vec.rep_eq uminus_fixed_vec.rep_eq
by (simp add: Rep_fixed_vec_inverse)
then have "Rep_fixed_vec (x - y) = Rep_fixed_vec x + smult_vec (-1) (Rep_fixed_vec y)"
using minus_fixed_vec.rep_eq by blast
also have "... = Rep_fixed_vec x + (- Rep_fixed_vec y)"
by (simp add: smult_vec_def uminus_vec_def)
also have "... = Rep_fixed_vec x - Rep_fixed_vec y"
using Rep_fixed_vec by fastforce
finally show ?thesis .
qed
subsubsection ‹Lipschitz Continuity of Functions (Interval)›
paragraph ‹Neural Network: Activations›
lemma relu_lipschitz': "⋀x y. (x::(real, 'b::finite) fixed_vec) ∈ X ⟹
(y::(real, 'b::finite) fixed_vec) ∈ X ⟹
dist
((Abs_fixed_vec
(Matrix.vec (dim_vec (Rep_fixed_vec x))
(λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)))::(real, 'b::finite) fixed_vec)
((Abs_fixed_vec
(Matrix.vec (dim_vec (Rep_fixed_vec y))
(λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b::finite) fixed_vec)
≤ dist x y"
proof -
fix x y::"(real, 'b::finite) fixed_vec" assume "x ∈ X" "y ∈ X"
have dist_eq: "dist ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (x::(real, 'b) fixed_vec))) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)))::(real, 'b) fixed_vec)
((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (y::(real, 'b) fixed_vec))) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b) fixed_vec)
= norm ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (x::(real, 'b) fixed_vec))) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0))::(real, 'b) fixed_vec)
- (Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (y::(real, 'b) fixed_vec))) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b) fixed_vec)"
by (simp add: dist_norm)
have relu_bound: "∀a b::real. abs (max 0 a - max 0 b) ≤ abs (a - b)"
proof (intro allI)
fix a b :: real
have "1-lipschitz_on {a, b} relu"
using relu_lipschitz[of "UNIV"]
by (rule lipschitz_on_subset) auto
show "abs (max 0 a - max 0 b) ≤ abs (a - b)"
unfolding lipschitz_on_def relu_def dist_real_def
by auto
qed
have norm_bound: "norm ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0))
- Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b::finite) fixed_vec)
≤ norm (x - y)"
proof -
have "norm ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0))
- Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b) fixed_vec)
= sqrt (∑i∈{0..<CARD('b)}. (norm (fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0))
- Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b) fixed_vec) i))^2)"
unfolding norm_fixed_vec_def by simp
also have "... = sqrt (∑i∈{0..<CARD('b)}. (abs ((if 0 ≤ vec_index (Rep_fixed_vec (x::(real, 'b) fixed_vec)) i then vec_index (Rep_fixed_vec (x::(real, 'b) fixed_vec)) i else 0)
- (if 0 ≤ vec_index (Rep_fixed_vec (y::(real, 'b) fixed_vec)) i then vec_index (Rep_fixed_vec (y::(real, 'b) fixed_vec)) i else 0)))^2)"
proof -
show ?thesis
proof -
have valid_x: "Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0) ∈ carrier_vec CARD('b)"
proof -
have "dim_vec (Rep_fixed_vec x) = CARD('b)"
using Rep_fixed_vec[of x] by simp
then show ?thesis
using vec_carrier_vec by blast
qed
have valid_y: "Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0) ∈ carrier_vec CARD('b)"
proof -
have "dim_vec (Rep_fixed_vec y) = CARD('b)"
using Rep_fixed_vec[of y] by simp
then show ?thesis using vec_carrier_vec by blast
qed
have index_eq: "∀i < CARD('b).
fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b::finite) fixed_vec) i
= (if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0) -
(if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)"
proof (clarify)
fix i assume "i < CARD('b)"
have "fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. if 0 ≤ Rep_fixed_vec x $ j then Rep_fixed_vec x $ j else 0)) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. if 0 ≤ Rep_fixed_vec y $ j then Rep_fixed_vec y $ j else 0)))::(real, 'b) fixed_vec) i
= Rep_fixed_vec ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. if 0 ≤ Rep_fixed_vec x $ j then Rep_fixed_vec x $ j else 0)) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. if 0 ≤ Rep_fixed_vec y $ j then Rep_fixed_vec y $ j else 0)))::(real, 'b) fixed_vec) $ i"
by (simp add: fixed_vec_index_def)
also have "... = (Rep_fixed_vec ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. if 0 ≤ Rep_fixed_vec x $ j then Rep_fixed_vec x $ j else 0)))::(real, 'b) fixed_vec) -
Rep_fixed_vec ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. if 0 ≤ Rep_fixed_vec y $ j then Rep_fixed_vec y $ j else 0)))::(real, 'b) fixed_vec)) $ i"
using Rep_fixed_vec_minus
by (smt (verit, del_insts))
also have "... = (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. if 0 ≤ Rep_fixed_vec x $ j then Rep_fixed_vec x $ j else 0) -
Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. if 0 ≤ Rep_fixed_vec y $ j then Rep_fixed_vec y $ j else 0)) $ i"
using Abs_fixed_vec_inverse[OF valid_x] Abs_fixed_vec_inverse[OF valid_y] by simp
also have "... = Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. if 0 ≤ Rep_fixed_vec x $ j then Rep_fixed_vec x $ j else 0) $ i -
Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. if 0 ≤ Rep_fixed_vec y $ j then Rep_fixed_vec y $ j else 0) $ i"
apply (simp add: minus_vec_def) using ‹(i::nat) < CARD('b::finite)› valid_y by fastforce
also have "... = (if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0) -
(if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)"
proof -
have "dim_vec (Rep_fixed_vec x) = CARD('b)" using Rep_fixed_vec[of x] by simp
have "dim_vec (Rep_fixed_vec y) = CARD('b)" using Rep_fixed_vec[of y] by simp
then show ?thesis using `i < CARD('b)`
by (simp add: ‹dim_vec (Rep_fixed_vec (x::(real, 'b::finite) fixed_vec)) = CARD('b::finite)›)
qed
finally show " fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b::finite) fixed_vec) i
= (if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0) -
(if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)" .
qed
have "sqrt (∑i = 0..<CARD('b). (norm (fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b::finite) fixed_vec) i))^2)
= sqrt (∑i = 0..<CARD('b). (norm ((if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0) -
(if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))^2)"
using index_eq by simp
also have "... = sqrt (∑i = 0..<CARD('b). abs ((if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0) -
(if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0))^2)"
by (simp add: real_norm_def)
finally show ?thesis .
qed
qed
also have "... ≤ sqrt (∑i∈{0..<CARD('b)}. (abs (Rep_fixed_vec x $ i - Rep_fixed_vec y $ i))^2)"
proof -
have "∀i. abs ((if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)
- (if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0))
≤ abs (Rep_fixed_vec x $ i - Rep_fixed_vec y $ i)"
using relu_bound by (auto simp: max_def)
then show ?thesis
using sum_mono power_mono
by (smt (verit, best) real_sqrt_le_mono)
qed
also have "... = norm (x - y)"
proof -
have "norm (x - y) = sqrt (∑i∈{0..<CARD('b)}. (norm (fixed_vec_index (x - y) i))^2)"
by (simp add: norm_fixed_vec_def)
also have "... = sqrt (∑i∈{0..<CARD('b)}. (norm (Rep_fixed_vec (x - y) $ i))^2)"
by (simp add: fixed_vec_index_def)
also have "... = sqrt (∑i∈{0..<CARD('b)}. (norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ i))^2)"
using Rep_fixed_vec_minus by metis
also have "... = sqrt (∑i∈{0..<CARD('b)}. (norm (Rep_fixed_vec x $ i - Rep_fixed_vec y $ i))^2)"
apply (simp add: minus_vec_def)
by (metis (no_types, lifting) Finite_Cartesian_Product.sum_cong_aux Rep_fixed_vec atLeastLessThan_iff carrier_vecD index_vec)
also have "... = sqrt (∑i∈{0..<CARD('b)}. ¦Rep_fixed_vec x $ i - Rep_fixed_vec y $ i¦^2)"
by simp
finally show ?thesis by simp
qed
finally show " norm
((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (x::(real, 'b::finite) fixed_vec))) (λi::nat. if (0::real) ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else (0::real))) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (y::(real, 'b::finite) fixed_vec))) (λi::nat. if (0::real) ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else (0::real))))::(real, 'b::finite) fixed_vec)
≤ norm (x - y)" by simp
qed
have a0: " map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) (λb. if 0 ≤ b then b else 0) x =
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. relu (Rep_fixed_vec x $ i)))"
unfolding relu_def max_def
by (simp add: map_fun_def)
moreover have a1: "map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) (λb. if 0 ≤ b then b else 0) y =
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. relu (Rep_fixed_vec y $ i)))"
unfolding relu_def max_def
by (simp add: map_fun_def)
also have a2: "dist ((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) (λb. if 0 ≤ b then b else 0) x)::(real, 'b) fixed_vec)
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) (λb. if 0 ≤ b then b else 0) y)::(real, 'b) fixed_vec)
≤ 1 * dist x y =
( dist ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)))::(real, 'b) fixed_vec)
((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b) fixed_vec)
≤1 * dist x y )"
apply (subst a0 a1)+
unfolding relu_def max_def
by blast
have b0: "dist ((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) (λb. if 0 ≤ b then b else 0) x)::(real, 'b) fixed_vec)
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) (λb. if 0 ≤ b then b else 0) y)::(real, 'b) fixed_vec)
≤ 1 * dist x y"
using dist_eq norm_bound a0 a1 a2 dist_norm
by (smt (verit, del_insts))
show " dist
((Abs_fixed_vec
(Matrix.vec (dim_vec (Rep_fixed_vec x))
(λi::nat. if 0 ≤ Rep_fixed_vec x $ i then Rep_fixed_vec x $ i else 0)))::(real, 'b) fixed_vec)
((Abs_fixed_vec
(Matrix.vec (dim_vec (Rep_fixed_vec y))
(λi::nat. if 0 ≤ Rep_fixed_vec y $ i then Rep_fixed_vec y $ i else 0)))::(real, 'b) fixed_vec)
≤ dist x y"
using a0 a1 a2 b0
by argo
qed
lemma relu_lipschitz_fv: "1-lipschitz_on (X::(real, 'b::finite) fixed_vec set) (map_fixed_vec relu)"
unfolding lipschitz_on_def relu_def map_fixed_vec_def max_def map_vec_def
apply (intro conjI impI allI)
subgoal using rel_simps(44) by blast
subgoal using relu_lipschitz'[of _ X] by simp
done
lemma identity_lipschitz_fv: "1-lipschitz_on (X) (map_fixed_vec identity)"
unfolding lipschitz_on_def relu_def map_fixed_vec_def map_vec_def
by (auto, smt (verit) Rep_fixed_vec_inverse dim_vec eq_vecI identity_def
index_vec verit_comp_simplify1(2))
lemma softplus_lipschitz': " ⋀x y. (x::(real, 'b::finite) fixed_vec) ∈ X ⟹
(y::(real, 'b::finite) fixed_vec) ∈ X ⟹
dist ((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) softplus x)::(real, 'b) fixed_vec)
(map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) softplus y)
≤ 1 * dist x y"
proof -
fix x y::"(real, 'b::finite) fixed_vec" assume "x ∈ X" "y ∈ X"
have softplus_bound: "∀a b::real. abs (softplus a - softplus b) ≤ abs (a - b)"
proof (intro allI)
fix a b :: real
have deriv_bound: "∀ (z::real) . softplus' z ≤ 1"
proof -
fix z :: real
have "softplus' z = 1 / (1 + exp(-z))"
by (simp add: softplus'_def)
also have "... ≤ 1"
by (simp add: add_sign_intros(2))
finally show ?thesis
by (simp add: add_sign_intros(2) softplus'_def)
qed
have cont: "continuous_on {min a b..max a b} softplus"
by (meson DERIV_isCont softplus' continuous_at_imp_continuous_on)
have diff: "⋀x. min a b < x ⟹ x < max a b ⟹ softplus differentiable at x"
using real_differentiable_def softplus' by blast
have mvt: "∃c. softplus b - softplus a = (b - a) * softplus' c"
proof (cases "a = b")
case True
then have "softplus b - softplus a = 0" by simp
also have "... = (b - a) * softplus' a" using True by simp
finally show ?thesis by blast
next
case False
obtain l c where c_bounds: "min a b < c ∧ c < max a b" and
has_deriv: "(softplus has_real_derivative l) (at c)" and
mvt_eq: "softplus (max a b) - softplus (min a b) = (max a b - min a b) * l"
using MVT[of "min a b" "max a b" softplus] cont diff False
by fastforce
have "l = softplus' c"
using has_deriv softplus'[of c]
by (simp add: DERIV_unique)
have result: "softplus b - softplus a = (b - a) * softplus' c"
proof (cases "a ≤ b")
case True
then have "min a b = a" "max a b = b" by auto
with mvt_eq `l = softplus' c` show ?thesis
by simp
next
case False
then have "min a b = b" "max a b = a" by auto
with mvt_eq `l = softplus' c` have "softplus a - softplus b = (a - b) * softplus' c" by simp
then show ?thesis by (simp add: algebra_simps)
qed
show ?thesis using result by blast
qed
obtain c where mvt_eq: "softplus b - softplus a = (b - a) * softplus' c"
using mvt by blast
have "abs (softplus a - softplus b) = abs (softplus b - softplus a)"
by simp
also have "... = abs ((b - a) * softplus' c)"
using mvt_eq by simp
also have "... = abs (b - a) * abs (softplus' c)"
by (simp add: abs_mult)
also have "... ≤ abs (b - a) * 1"
using deriv_bound
apply (simp add: mult_left_mono)
by (smt (verit, ccfv_threshold) divide_pos_pos exp_ge_zero mult_left_le softplus'_def)
also have "... = abs (a - b)"
by simp
finally show "abs (softplus a - softplus b) ≤ abs (a - b)" .
qed
have "dist
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i)))
softplus x)::(real, 'b::finite) fixed_vec)
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i)))
softplus y)::(real, 'b::finite) fixed_vec)
≤ 1 * dist x y"
proof -
have dist_eq: "dist ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (x::(real, 'b) fixed_vec))) (λi. softplus (Rep_fixed_vec x $ i))))::(real, 'b) fixed_vec)
((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (y::(real, 'b) fixed_vec))) (λi. softplus (Rep_fixed_vec y $ i))))::(real, 'b) fixed_vec)
= norm ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (x::(real, 'b) fixed_vec))) (λi. softplus (Rep_fixed_vec x $ i)))::(real, 'b) fixed_vec) -
(Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec (y::(real, 'b) fixed_vec))) (λi. softplus (Rep_fixed_vec y $ i))))::(real, 'b) fixed_vec)"
by (simp add: dist_norm softplus_def)
also have "... ≤ norm (x - y)"
proof -
have "norm ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i)))
- Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. softplus (Rep_fixed_vec y $ i))))::(real, 'b) fixed_vec)
= sqrt (∑i∈{0..<CARD('b)}. (norm (fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i)))
- Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. softplus (Rep_fixed_vec y $ i))))::(real, 'b) fixed_vec) i))^2)"
unfolding norm_fixed_vec_def by simp
also have "... = sqrt (∑i∈{0..<CARD('b)}. (abs (softplus (vec_index (Rep_fixed_vec (x::(real, 'b) fixed_vec)) i)
- softplus (vec_index (Rep_fixed_vec (y::(real, 'b) fixed_vec)) i)))^2)"
proof -
show ?thesis
proof -
have valid_x: "Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i)) ∈ carrier_vec CARD('b)"
proof -
have "dim_vec (Rep_fixed_vec x) = CARD('b)"
using Rep_fixed_vec[of x] by simp
then show ?thesis
using vec_carrier_vec by blast
qed
have valid_y: "Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. softplus (Rep_fixed_vec y $ i)) ∈ carrier_vec CARD('b)"
proof -
have "dim_vec (Rep_fixed_vec y) = CARD('b)"
using Rep_fixed_vec[of y] by simp
then show ?thesis using vec_carrier_vec by blast
qed
have index_eq: "∀i < CARD('b).
fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i))) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. softplus (Rep_fixed_vec y $ i))))::(real, 'b::finite) fixed_vec) i
= softplus (Rep_fixed_vec x $ i) - softplus (Rep_fixed_vec y $ i)"
proof (clarify)
fix i assume "i < CARD('b)"
have "fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. softplus (Rep_fixed_vec x $ j))) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. softplus (Rep_fixed_vec y $ j))))::(real, 'b) fixed_vec) i
= Rep_fixed_vec ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. softplus (Rep_fixed_vec x $ j))) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. softplus (Rep_fixed_vec y $ j))))::(real, 'b) fixed_vec) $ i"
by (simp add: fixed_vec_index_def)
also have "... = (Rep_fixed_vec ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. softplus (Rep_fixed_vec x $ j))))::(real, 'b) fixed_vec) -
Rep_fixed_vec ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. softplus (Rep_fixed_vec y $ j))))::(real, 'b) fixed_vec)) $ i"
using Rep_fixed_vec_minus
by (smt (verit, del_insts))
also have "... = (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. softplus (Rep_fixed_vec x $ j)) -
Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. softplus (Rep_fixed_vec y $ j))) $ i"
using Abs_fixed_vec_inverse[OF valid_x] Abs_fixed_vec_inverse[OF valid_y] by simp
also have "... = Matrix.vec (dim_vec (Rep_fixed_vec x)) (λj. softplus (Rep_fixed_vec x $ j)) $ i -
Matrix.vec (dim_vec (Rep_fixed_vec y)) (λj. softplus (Rep_fixed_vec y $ j)) $ i"
apply (simp add: minus_vec_def) using ‹(i::nat) < CARD('b::finite)› valid_y by fastforce
also have "... = softplus (Rep_fixed_vec x $ i) - softplus (Rep_fixed_vec y $ i)"
proof -
have "dim_vec (Rep_fixed_vec x) = CARD('b)" using Rep_fixed_vec[of x] by simp
have "dim_vec (Rep_fixed_vec y) = CARD('b)" using Rep_fixed_vec[of y] by simp
then show ?thesis using `i < CARD('b)`
by (simp add: ‹dim_vec (Rep_fixed_vec (x::(real, 'b::finite) fixed_vec)) = CARD('b::finite)›)
qed
finally show "fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i))) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. softplus (Rep_fixed_vec y $ i))))::(real, 'b::finite) fixed_vec) i
= softplus (Rep_fixed_vec x $ i) - softplus (Rep_fixed_vec y $ i)" .
qed
have "sqrt (∑i = 0..<CARD('b). (norm (fixed_vec_index ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i))) -
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. softplus (Rep_fixed_vec y $ i))))::(real, 'b::finite) fixed_vec) i))^2)
= sqrt (∑i = 0..<CARD('b). (norm (softplus (Rep_fixed_vec x $ i) - softplus (Rep_fixed_vec y $ i)))^2)"
using index_eq by simp
also have "... = sqrt (∑i = 0..<CARD('b). abs (softplus (Rep_fixed_vec x $ i) - softplus (Rep_fixed_vec y $ i))^2)"
by (simp add: real_norm_def)
finally show ?thesis .
qed
qed
also have "... ≤ sqrt (∑i∈{0..<CARD('b)}. (abs (Rep_fixed_vec x $ i - Rep_fixed_vec y $ i))^2)"
proof -
have "∀i. abs (softplus (Rep_fixed_vec x $ i) - softplus (Rep_fixed_vec y $ i))
≤ abs (Rep_fixed_vec x $ i - Rep_fixed_vec y $ i)"
using softplus_bound by auto
then show ?thesis
using sum_mono power_mono
by (smt (verit, best) real_sqrt_le_mono)
qed
also have "... = norm (x - y)"
proof -
have "norm (x - y) = sqrt (∑i∈{0..<CARD('b)}. (norm (fixed_vec_index (x - y) i))^2)"
by (simp add: norm_fixed_vec_def)
also have "... = sqrt (∑i∈{0..<CARD('b)}. (norm (Rep_fixed_vec (x - y) $ i))^2)"
by (simp add: fixed_vec_index_def)
also have "... = sqrt (∑i∈{0..<CARD('b)}. (norm ((Rep_fixed_vec x - Rep_fixed_vec y) $ i))^2)"
using Rep_fixed_vec_minus by metis
also have "... = sqrt (∑i∈{0..<CARD('b)}. (norm (Rep_fixed_vec x $ i - Rep_fixed_vec y $ i))^2)"
apply (simp add: minus_vec_def)
by (metis (no_types, lifting) Finite_Cartesian_Product.sum_cong_aux Rep_fixed_vec atLeastLessThan_iff carrier_vecD index_vec)
also have "... = sqrt (∑i∈{0..<CARD('b)}. ¦Rep_fixed_vec x $ i - Rep_fixed_vec y $ i¦^2)"
by simp
finally show ?thesis by simp
qed
finally show ?thesis by simp
qed
also have "... = dist x y"
by (simp add: dist_norm)
have a0: "dist ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i))))::(real, 'b::finite) fixed_vec) ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi::nat. softplus (Rep_fixed_vec y $ i))))::(real, 'b::finite) fixed_vec)
≤ dist x y"
by (metis calculation dist_norm)
have map_fun_eq_x: "map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) softplus x =
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i)))"
by (simp add: map_fun_def)
have map_fun_eq_y: "map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) softplus y =
Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi. softplus (Rep_fixed_vec y $ i)))"
by (simp add: map_fun_def)
have a1: " dist
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i)))
softplus x)::(real, 'b) fixed_vec)
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i)))
softplus y)::(real, 'b) fixed_vec)
≤ 1 * dist x y =
(dist ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec x)) (λi. softplus (Rep_fixed_vec x $ i))))::(real, 'b::finite) fixed_vec) ((Abs_fixed_vec (Matrix.vec (dim_vec (Rep_fixed_vec y)) (λi::nat. softplus (Rep_fixed_vec y $ i))))::(real, 'b::finite) fixed_vec)
≤ dist x y )"
apply(subst map_fun_eq_x map_fun_eq_y )+
by simp
show "dist ((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i))) softplus x)::(real, 'b::finite) fixed_vec)
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i))) softplus y)::(real, 'b::finite) fixed_vec)
≤ 1 * dist x y" using a0 a1 by meson
qed
show "
dist ((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) softplus x)::(real, 'b) fixed_vec)
((map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λf v. Matrix.vec (dim_vec v) (λi. f (v $ i))) softplus y)::(real, 'b) fixed_vec)
≤ 1 * dist x y "
using
‹dist (map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i))) softplus (x::(real, 'b::finite) fixed_vec)) (map_fun id (map_fun Rep_fixed_vec Abs_fixed_vec) (λ(f::real ⇒ real) v::real Matrix.vec. Matrix.vec (dim_vec v) (λi::nat. f (v $ i))) softplus (y::(real, 'b::finite) fixed_vec)) ≤ 1 * dist x y›
by fastforce
qed
lemma softplus_lipschitz: "1-lipschitz_on (X::(real, 'b::finite) fixed_vec set) (map_fixed_vec softplus)"
unfolding lipschitz_on_def map_fixed_vec_def map_vec_def
apply(clarsimp)[1]
using softplus_lipschitz'[of _ X]
by simp
end