(* Title: Inner_Product.thy Author: Brian Huffman *) header {* Inner Product Spaces and the Gradient Derivative *} theory Inner_Product imports Complex_Main FrechetDeriv begin subsection {* Real inner product spaces *} class real_inner = real_vector + sgn_div_norm + fixes inner :: "'a \ 'a \ real" assumes inner_commute: "inner x y = inner y x" and inner_left_distrib: "inner (x + y) z = inner x z + inner y z" and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)" and inner_ge_zero [simp]: "0 \ inner x x" and inner_eq_zero_iff [simp]: "inner x x = 0 \ x = 0" and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)" begin lemma inner_zero_left [simp]: "inner 0 x = 0" using inner_left_distrib [of 0 0 x] by simp lemma inner_minus_left [simp]: "inner (- x) y = - inner x y" using inner_left_distrib [of x "- x" y] by simp lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z" by (simp add: diff_minus inner_left_distrib) text {* Transfer distributivity rules to right argument. *} lemma inner_right_distrib: "inner x (y + z) = inner x y + inner x z" using inner_left_distrib [of y z x] by (simp only: inner_commute) lemma inner_scaleR_right: "inner x (scaleR r y) = r * (inner x y)" using inner_scaleR_left [of r y x] by (simp only: inner_commute) lemma inner_zero_right [simp]: "inner x 0 = 0" using inner_zero_left [of x] by (simp only: inner_commute) lemma inner_minus_right [simp]: "inner x (- y) = - inner x y" using inner_minus_left [of y x] by (simp only: inner_commute) lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z" using inner_diff_left [of y z x] by (simp only: inner_commute) lemmas inner_distrib = inner_left_distrib inner_right_distrib lemmas inner_diff = inner_diff_left inner_diff_right lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right lemma inner_gt_zero_iff [simp]: "0 < inner x x \ x \ 0" by (simp add: order_less_le) lemma power2_norm_eq_inner: "(norm x)\ = inner x x" by (simp add: norm_eq_sqrt_inner) lemma Cauchy_Schwarz_ineq: "(inner x y)\ \ inner x x * inner y y" proof (cases) assume "y = 0" thus ?thesis by simp next assume y: "y \ 0" let ?r = "inner x y / inner y y" have "0 \ inner (x - scaleR ?r y) (x - scaleR ?r y)" by (rule inner_ge_zero) also have "\ = inner x x - inner y x * ?r" by (simp add: inner_diff inner_scaleR) also have "\ = inner x x - (inner x y)\ / inner y y" by (simp add: power2_eq_square inner_commute) finally have "0 \ inner x x - (inner x y)\ / inner y y" . hence "(inner x y)\ / inner y y \ inner x x" by (simp add: le_diff_eq) thus "(inner x y)\ \ inner x x * inner y y" by (simp add: pos_divide_le_eq y) qed lemma Cauchy_Schwarz_ineq2: "\inner x y\ \ norm x * norm y" proof (rule power2_le_imp_le) have "(inner x y)\ \ inner x x * inner y y" using Cauchy_Schwarz_ineq . thus "\inner x y\\ \ (norm x * norm y)\" by (simp add: power_mult_distrib power2_norm_eq_inner) show "0 \ norm x * norm y" unfolding norm_eq_sqrt_inner by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) qed subclass real_normed_vector proof fix a :: real and x y :: 'a show "0 \ norm x" unfolding norm_eq_sqrt_inner by simp show "norm x = 0 \ x = 0" unfolding norm_eq_sqrt_inner by simp show "norm (x + y) \ norm x + norm y" proof (rule power2_le_imp_le) have "inner x y \ norm x * norm y" by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2]) thus "(norm (x + y))\ \ (norm x + norm y)\" unfolding power2_sum power2_norm_eq_inner by (simp add: inner_distrib inner_commute) show "0 \ norm x + norm y" unfolding norm_eq_sqrt_inner by (simp add: add_nonneg_nonneg) qed have "sqrt (a\ * inner x x) = \a\ * sqrt (inner x x)" by (simp add: real_sqrt_mult_distrib) then show "norm (a *\<^sub>R x) = \a\ * norm x" unfolding norm_eq_sqrt_inner by (simp add: inner_scaleR power2_eq_square mult_assoc) qed end interpretation inner!: bounded_bilinear "inner::'a::real_inner \ 'a \ real" proof fix x y z :: 'a and r :: real show "inner (x + y) z = inner x z + inner y z" by (rule inner_left_distrib) show "inner x (y + z) = inner x y + inner x z" by (rule inner_right_distrib) show "inner (scaleR r x) y = scaleR r (inner x y)" unfolding real_scaleR_def by (rule inner_scaleR_left) show "inner x (scaleR r y) = scaleR r (inner x y)" unfolding real_scaleR_def by (rule inner_scaleR_right) show "\K. \x y::'a. norm (inner x y) \ norm x * norm y * K" proof show "\x y::'a. norm (inner x y) \ norm x * norm y * 1" by (simp add: Cauchy_Schwarz_ineq2) qed qed interpretation inner_left!: bounded_linear "\x::'a::real_inner. inner x y" by (rule inner.bounded_linear_left) interpretation inner_right!: bounded_linear "\y::'a::real_inner. inner x y" by (rule inner.bounded_linear_right) subsection {* Class instances *} instantiation real :: real_inner begin definition inner_real_def [simp]: "inner = op *" instance proof fix x y z r :: real show "inner x y = inner y x" unfolding inner_real_def by (rule mult_commute) show "inner (x + y) z = inner x z + inner y z" unfolding inner_real_def by (rule left_distrib) show "inner (scaleR r x) y = r * inner x y" unfolding inner_real_def real_scaleR_def by (rule mult_assoc) show "0 \ inner x x" unfolding inner_real_def by simp show "inner x x = 0 \ x = 0" unfolding inner_real_def by simp show "norm x = sqrt (inner x x)" unfolding inner_real_def by simp qed end instantiation complex :: real_inner begin definition inner_complex_def: "inner x y = Re x * Re y + Im x * Im y" instance proof fix x y z :: complex and r :: real show "inner x y = inner y x" unfolding inner_complex_def by (simp add: mult_commute) show "inner (x + y) z = inner x z + inner y z" unfolding inner_complex_def by (simp add: left_distrib) show "inner (scaleR r x) y = r * inner x y" unfolding inner_complex_def by (simp add: right_distrib) show "0 \ inner x x" unfolding inner_complex_def by (simp add: add_nonneg_nonneg) show "inner x x = 0 \ x = 0" unfolding inner_complex_def by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) show "norm x = sqrt (inner x x)" unfolding inner_complex_def complex_norm_def by (simp add: power2_eq_square) qed end subsection {* Gradient derivative *} definition gderiv :: "['a::real_inner \ real, 'a, 'a] \ bool" ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where "GDERIV f x :> D \ FDERIV f x :> (\h. inner h D)" lemma deriv_fderiv: "DERIV f x :> D \ FDERIV f x :> (\h. h * D)" by (simp only: deriv_def field_fderiv_def) lemma gderiv_deriv [simp]: "GDERIV f x :> D \ DERIV f x :> D" by (simp only: gderiv_def deriv_fderiv inner_real_def) lemma GDERIV_DERIV_compose: "\GDERIV f x :> df; DERIV g (f x) :> dg\ \ GDERIV (\x. g (f x)) x :> scaleR dg df" unfolding gderiv_def deriv_fderiv apply (drule (1) FDERIV_compose) apply (simp add: inner_scaleR_right mult_ac) done lemma FDERIV_subst: "\FDERIV f x :> df; df = d\ \ FDERIV f x :> d" by simp lemma GDERIV_subst: "\GDERIV f x :> df; df = d\ \ GDERIV f x :> d" by simp lemma GDERIV_const: "GDERIV (\x. k) x :> 0" unfolding gderiv_def inner_right.zero by (rule FDERIV_const) lemma GDERIV_add: "\GDERIV f x :> df; GDERIV g x :> dg\ \ GDERIV (\x. f x + g x) x :> df + dg" unfolding gderiv_def inner_right.add by (rule FDERIV_add) lemma GDERIV_minus: "GDERIV f x :> df \ GDERIV (\x. - f x) x :> - df" unfolding gderiv_def inner_right.minus by (rule FDERIV_minus) lemma GDERIV_diff: "\GDERIV f x :> df; GDERIV g x :> dg\ \ GDERIV (\x. f x - g x) x :> df - dg" unfolding gderiv_def inner_right.diff by (rule FDERIV_diff) lemma GDERIV_scaleR: "\DERIV f x :> df; GDERIV g x :> dg\ \ GDERIV (\x. scaleR (f x) (g x)) x :> (scaleR (f x) dg + scaleR df (g x))" unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR apply (rule FDERIV_subst) apply (erule (1) scaleR.FDERIV) apply (simp add: mult_ac) done lemma GDERIV_mult: "\GDERIV f x :> df; GDERIV g x :> dg\ \ GDERIV (\x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df" unfolding gderiv_def apply (rule FDERIV_subst) apply (erule (1) FDERIV_mult) apply (simp add: inner_distrib inner_scaleR mult_ac) done lemma GDERIV_inverse: "\GDERIV f x :> df; f x \ 0\ \ GDERIV (\x. inverse (f x)) x :> - (inverse (f x))\ *\<^sub>R df" apply (erule GDERIV_DERIV_compose) apply (erule DERIV_inverse [folded numeral_2_eq_2]) done lemma GDERIV_norm: assumes "x \ 0" shows "GDERIV (\x. norm x) x :> sgn x" proof - have 1: "FDERIV (\x. inner x x) x :> (\h. inner x h + inner h x)" by (intro inner.FDERIV FDERIV_ident) have 2: "(\h. inner x h + inner h x) = (\h. inner h (scaleR 2 x))" by (simp add: expand_fun_eq inner_scaleR inner_commute) have "0 < inner x x" using `x \ 0` by simp then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" by (rule DERIV_real_sqrt) have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x" by (simp add: sgn_div_norm norm_eq_sqrt_inner) show ?thesis unfolding norm_eq_sqrt_inner apply (rule GDERIV_subst [OF _ 4]) apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"]) apply (subst gderiv_def) apply (rule FDERIV_subst [OF _ 2]) apply (rule 1) apply (rule 3) done qed lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def] end