Theory InnerProduct

header {* Inner Product Spaces *}

theory InnerProduct
imports Complex FrechetDeriv
begin

subsection {* Real inner product spaces *}

class inner = type +
  fixes inner :: "'a => 'a => real"

class real_inner = real_vector + inner + sgn_div_norm +
  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: "0 ≤ inner x x"
  and inner_eq_zero: "(inner x x = 0) = (x = 0)"
  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"

lemma inner_right_distrib:
  fixes x y z :: "'a::real_inner"
  shows "inner x (y + z) = inner x y + inner x z"
proof -
  have "inner x (y + z) = inner (y + z) x"
    by (rule inner_commute)
  also have "… = inner y x + inner z x"
    by (rule inner_left_distrib)
  finally show ?thesis
    by (simp add: inner_commute)
qed

lemma inner_scaleR_right:
  fixes x y z :: "'a::real_inner"
  shows "inner x (scaleR r y) = r * (inner x y)"
proof -
  have "inner x (scaleR r y) = inner (scaleR r y) x"
    by (rule inner_commute)
  also have "… = r * (inner y x)"
    by (rule inner_scaleR_left)
  finally show ?thesis
    by (simp add: inner_commute)
qed

interpretation inner_left: additive ["(λx::'a::real_inner. inner x y)"]
  by unfold_locales (rule inner_left_distrib)

interpretation inner_right: additive ["(λy::'a::real_inner. inner x y)"]
  by unfold_locales (rule inner_right_distrib)

lemmas inner_zero_left [simp] = inner_left.zero
lemmas inner_zero_right [simp] = inner_right.zero
lemmas inner_left_diff_distrib = inner_left.diff
lemmas inner_right_diff_distrib = inner_right.diff

lemmas inner_distrib = inner_left_distrib inner_right_distrib
lemmas inner_diff = inner_left_diff_distrib inner_right_diff_distrib
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right

lemma zero_less_inner_iff: "(0 < inner x x) = (x ≠ (0::'a::real_inner))"
  by (simp add: order_less_le inner_ge_zero inner_eq_zero)

lemma Cauchy_Schwartz_ineq:
  fixes x y :: "'a::real_inner"
  shows "(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_left_diff_distrib inner_right_diff_distrib
                  inner_scaleR_left inner_scaleR_right)
  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 zero_less_inner_iff y)
qed

lemma norm_squared_eq_inner: "(norm x)² = inner x (x::'a::real_inner)"
  by (simp add: norm_eq_sqrt_inner inner_ge_zero)

lemma Cauchy_Schwartz_ineq2:
  fixes x y :: "'a::real_inner"
  shows "¦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_Schwartz_ineq .
  thus "¦inner x y¦² ≤ (norm x * norm y)²"
    by (simp add: power_mult_distrib norm_squared_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

instance real_inner ⊆ real_normed_vector
proof
  fix a :: real and x y :: "'a::real_inner"
  show "0 ≤ norm x"
    unfolding norm_eq_sqrt_inner by (simp add: inner_ge_zero)
  show "(norm x = 0) = (x = 0)"
    unfolding norm_eq_sqrt_inner by (simp add: inner_eq_zero)
  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_Schwartz_ineq2])
      thus "(norm (x + y))² ≤ (norm x + norm y)²"
        unfolding power2_sum norm_squared_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 inner_ge_zero)
    qed
  show "norm (a *R x) = ¦a¦ * norm x"
    unfolding norm_eq_sqrt_inner
    apply (simp add: inner_scaleR)
    apply (simp add: mult_assoc [symmetric] power2_eq_square [symmetric])
    apply (simp add: real_sqrt_mult_distrib)
    done
qed

interpretation inner:
  bounded_bilinear ["inner::'a::real_inner => 'a => real"]
  apply (unfold_locales)
  apply (unfold real_scaleR_def)
  apply (rule inner_left_distrib)
  apply (rule inner_right_distrib)
  apply (rule inner_scaleR_left)
  apply (rule inner_scaleR_right)
  apply (rule_tac x="1" in exI)
  apply (simp add: Cauchy_Schwartz_ineq2)
  done

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 {* Instances *}

instantiation real :: real_inner
begin

definition
  inner_real_def [simp]: "inner = op *"

instance
apply (intro_classes, unfold inner_real_def real_scaleR_def)
apply (rule mult_commute)
apply (rule left_distrib)
apply (rule mult_assoc)
apply simp
apply simp
apply simp
done

end

lemma add_nonneg_eq_0_iff:
  fixes x y :: "'a::pordered_ab_group_add"
  assumes x: "0 ≤ x" and y: "0 ≤ y"
  shows "x + y = 0 <-> x = 0 ∧ y = 0"
proof (auto)
  have "x = x + 0" by simp
  also have "x + 0 ≤ x + y" using y by (rule add_left_mono)
  also assume "x + y = 0"
  also have "0 ≤ x" using x .
  finally show "x = 0" .
next
  have "y = 0 + y" by simp
  also have "0 + y ≤ x + y" using x by (rule add_right_mono)
  also assume "x + y = 0"
  also have "0 ≤ y" using y .
  finally show "y = 0" .
qed

instantiation complex :: real_inner
begin

definition
  inner_complex_def: "inner x y = Re x * Re y + Im x * Im y"

instance
apply (intro_classes, unfold inner_complex_def)
apply (simp add: mult_commute)
apply (simp add: left_distrib)
apply (simp add: right_distrib)
apply (simp add: power2_eq_square [symmetric])
apply (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
apply (simp add: complex_norm_def power2_eq_square)
done

end

end