<commit_before>(* Title:      Inner_Product.thy
   Author:     <NAME>
*)

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 + dist_norm +
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> 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 \<le> inner x x"
  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> 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
<commit_msg>class real_inner derives from open_dist<commit_after>(* Title:      Inner_Product.thy
   Author:     <NAME>
*)

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 + dist_norm + open_dist +
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> 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 \<le> inner x x"
  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> 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

{'fraction_non_alphanumeric': 0.10504694835680752, 'fraction_numerical': 0.008215962441314555, 'mean_word_length': 4.0, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2116525', 'n_tokens_mistral': 646, 'n_tokens_neox': 606, 'n_words': 223}