Theory Inner_Product

theory Inner_Product
imports Complex_Main
(*  Title:      HOL/Library/Inner_Product.thy
    Author:     Brian Huffman
*)

header {* Inner Product Spaces and the Gradient Derivative *}

theory Inner_Product
imports "~~/src/HOL/Complex_Main"
begin

subsection {* Real inner product spaces *}

text {*
  Temporarily relax type constraints for @{term "open"},
  @{term dist}, and @{term norm}.
*}

setup {* Sign.add_const_constraint
  (@{const_name "open"}, SOME @{typ "'a::open set => bool"}) *}

setup {* Sign.add_const_constraint
  (@{const_name dist}, SOME @{typ "'a::dist => 'a => real"}) *}

setup {* Sign.add_const_constraint
  (@{const_name norm}, SOME @{typ "'a::norm => real"}) *}

class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
  fixes inner :: "'a => 'a => real"
  assumes inner_commute: "inner x y = inner y x"
  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
  and inner_scaleR_left [simp]: "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_add_left [of 0 0 x] by simp

lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
  using inner_add_left [of x "- x" y] by simp

lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
  using inner_add_left [of x "- y" z] by simp

lemma inner_setsum_left: "inner (∑x∈A. f x) y = (∑x∈A. inner (f x) y)"
  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)

text {* Transfer distributivity rules to right argument. *}

lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
  using inner_add_left [of y z x] by (simp only: inner_commute)

lemma inner_scaleR_right [simp]: "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)

lemma inner_setsum_right: "inner x (∑y∈A. f y) = (∑y∈A. inner x (f y))"
  using inner_setsum_left [of f A x] by (simp only: inner_commute)

lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right

text {* Legacy theorem names *}
lemmas inner_left_distrib = inner_add_left
lemmas inner_right_distrib = inner_add_right
lemmas inner_distrib = inner_left_distrib inner_right_distrib

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)2 = inner x x"
  by (simp add: norm_eq_sqrt_inner)

lemma Cauchy_Schwarz_ineq:
  "(inner x y)2 ≤ 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)
  also have "… = inner x x - (inner x y)2 / inner y y"
    by (simp add: power2_eq_square inner_commute)
  finally have "0 ≤ inner x x - (inner x y)2 / inner y y" .
  hence "(inner x y)2 / inner y y ≤ inner x x"
    by (simp add: le_diff_eq)
  thus "(inner x y)2 ≤ 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)2 ≤ inner x x * inner y y"
    using Cauchy_Schwarz_ineq .
  thus "¦inner x y¦2 ≤ (norm x * norm y)2"
    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

lemma norm_cauchy_schwarz: "inner x y ≤ norm x * norm y"
  using Cauchy_Schwarz_ineq2 [of x y] by auto

subclass real_normed_vector
proof
  fix a :: real and x y :: 'a
  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 norm_cauchy_schwarz)
      thus "(norm (x + y))2 ≤ (norm x + norm y)2"
        unfolding power2_sum power2_norm_eq_inner
        by (simp add: inner_add inner_commute)
      show "0 ≤ norm x + norm y"
        unfolding norm_eq_sqrt_inner by simp
    qed
  have "sqrt (a2 * inner x x) = ¦a¦ * sqrt (inner x x)"
    by (simp add: real_sqrt_mult_distrib)
  then show "norm (a *R x) = ¦a¦ * norm x"
    unfolding norm_eq_sqrt_inner
    by (simp add: power2_eq_square mult.assoc)
qed

end

text {*
  Re-enable constraints for @{term "open"},
  @{term dist}, and @{term norm}.
*}

setup {* Sign.add_const_constraint
  (@{const_name "open"}, SOME @{typ "'a::topological_space set => bool"}) *}

setup {* Sign.add_const_constraint
  (@{const_name dist}, SOME @{typ "'a::metric_space => 'a => real"}) *}

setup {* Sign.add_const_constraint
  (@{const_name norm}, SOME @{typ "'a::real_normed_vector => real"}) *}

lemma bounded_bilinear_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_add_left)
  show "inner x (y + z) = inner x y + inner x z"
    by (rule inner_add_right)
  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

lemmas tendsto_inner [tendsto_intros] =
  bounded_bilinear.tendsto [OF bounded_bilinear_inner]

lemmas isCont_inner [simp] =
  bounded_bilinear.isCont [OF bounded_bilinear_inner]

lemmas has_derivative_inner [derivative_intros] =
  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]

lemmas bounded_linear_inner_left =
  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]

lemmas bounded_linear_inner_right =
  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]

lemmas has_derivative_inner_right [derivative_intros] =
  bounded_linear.has_derivative [OF bounded_linear_inner_right]

lemmas has_derivative_inner_left [derivative_intros] =
  bounded_linear.has_derivative [OF bounded_linear_inner_left]

lemma differentiable_inner [simp]:
  "f differentiable (at x within s) ==> g differentiable at x within s ==> (λx. inner (f x) (g x)) differentiable at x within s"
  unfolding differentiable_def by (blast intro: has_derivative_inner)

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 distrib_right)
  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: distrib_right)
  show "inner (scaleR r x) y = r * inner x y"
    unfolding inner_complex_def by (simp add: distrib_left)
  show "0 ≤ inner x x"
    unfolding inner_complex_def by simp
  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

lemma complex_inner_1 [simp]: "inner 1 x = Re x"
  unfolding inner_complex_def by simp

lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
  unfolding inner_complex_def by simp

lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
  unfolding inner_complex_def by simp

lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
  unfolding inner_complex_def by simp


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 gderiv_deriv [simp]: "GDERIV f x :> D <-> DERIV f x :> D"
  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)

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 has_field_derivative_def
  apply (drule (1) has_derivative_compose)
  apply (simp add: ac_simps)
  done

lemma has_derivative_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_zero_right by (rule has_derivative_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_add_right by (rule has_derivative_add)

lemma GDERIV_minus:
    "GDERIV f x :> df ==> GDERIV (λx. - f x) x :> - df"
  unfolding gderiv_def inner_minus_right by (rule has_derivative_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_diff_right by (rule has_derivative_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 has_field_derivative_def inner_add_right inner_scaleR_right
  apply (rule has_derivative_subst)
  apply (erule (1) has_derivative_scaleR)
  apply (simp add: ac_simps)
  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 has_derivative_subst)
  apply (erule (1) has_derivative_mult)
  apply (simp add: inner_add ac_simps)
  done

lemma GDERIV_inverse:
    "[|GDERIV f x :> df; f x ≠ 0|]
     ==> GDERIV (λx. inverse (f x)) x :> - (inverse (f x))2 *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 has_derivative_inner has_derivative_ident)
  have 2: "(λh. inner x h + inner h x) = (λh. inner h (scaleR 2 x))"
    by (simp add: fun_eq_iff 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) *R 2 *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 has_derivative_subst [OF _ 2])
    apply (rule 1)
    apply (rule 3)
    done
qed

lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]

end