# Theory Complex_Inner_Product0

```(*  Based on HOL/Inner_Product.thy by Brian Huffman
Adapted to the complex case by Dominique Unruh *)

section ‹‹Complex_Inner_Product0› -- Inner Product Spaces and Gradient Derivative›

theory Complex_Inner_Product0
imports
Complex_Main Complex_Vector_Spaces
"HOL-Analysis.Inner_Product"
"Complex_Bounded_Operators.Extra_Ordered_Fields"
begin

subsection ‹Complex inner product spaces›

text ‹
Temporarily relax type constraints for \<^term>‹open›, \<^term>‹uniformity›,
\<^term>‹dist›, and \<^term>‹norm›.
›

(\<^const_name>‹open›, SOME \<^typ>‹'a::open set ⇒ bool›)›

(\<^const_name>‹dist›, SOME \<^typ>‹'a::dist ⇒ 'a ⇒ real›)›

(\<^const_name>‹uniformity›, SOME \<^typ>‹('a::uniformity × 'a) filter›)›

(\<^const_name>‹norm›, SOME \<^typ>‹'a::norm ⇒ real›)›

class complex_inner = complex_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
fixes cinner :: "'a ⇒ 'a ⇒ complex"
assumes cinner_commute: "cinner x y = cnj (cinner y x)"
and cinner_add_left: "cinner (x + y) z = cinner x z + cinner y z"
and cinner_scaleC_left [simp]: "cinner (scaleC r x) y = (cnj r) * (cinner x y)"
and cinner_ge_zero [simp]: "0 ≤ cinner x x"
and cinner_eq_zero_iff [simp]: "cinner x x = 0 ⟷ x = 0"
and norm_eq_sqrt_cinner: "norm x = sqrt (cmod (cinner x x))"
begin

lemma cinner_zero_left [simp]: "cinner 0 x = 0"
using cinner_add_left [of 0 0 x] by simp

lemma cinner_minus_left [simp]: "cinner (- x) y = - cinner x y"
using cinner_add_left [of x "- x" y]

lemma cinner_diff_left: "cinner (x - y) z = cinner x z - cinner y z"
using cinner_add_left [of x "- y" z] by simp

lemma cinner_sum_left: "cinner (∑x∈A. f x) y = (∑x∈A. cinner (f x) y)"

lemma call_zero_iff [simp]: "(∀u. cinner x u = 0) ⟷ (x = 0)"
by auto (use cinner_eq_zero_iff in blast)

text ‹Transfer distributivity rules to right argument.›

lemma cinner_add_right: "cinner x (y + z) = cinner x y + cinner x z"
using cinner_add_left [of y z x]

lemma cinner_scaleC_right [simp]: "cinner x (scaleC r y) = r * (cinner x y)"
using cinner_scaleC_left [of r y x]
by (metis complex_cnj_cnj complex_cnj_mult local.cinner_commute)

lemma cinner_zero_right [simp]: "cinner x 0 = 0"
using cinner_zero_left [of x]
by (metis (mono_tags, opaque_lifting) complex_cnj_zero local.cinner_commute)

lemma cinner_minus_right [simp]: "cinner x (- y) = - cinner x y"
using cinner_minus_left [of y x]
by (metis complex_cnj_minus local.cinner_commute)

lemma cinner_diff_right: "cinner x (y - z) = cinner x y - cinner x z"
using cinner_diff_left [of y z x]
by (metis complex_cnj_diff local.cinner_commute)

lemma cinner_sum_right: "cinner x (∑y∈A. f y) = (∑y∈A. cinner x (f y))"
proof (subst cinner_commute)
have "(∑y∈A. cinner (f y) x) = (∑y∈A. cinner (f y) x)"
by blast
hence "cnj (∑y∈A. cinner (f y) x) = cnj (∑y∈A. (cinner (f y) x))"
by simp
hence "cnj (cinner (sum f A) x) = (∑y∈A. cnj (cinner (f y) x))"
thus "cnj (cinner (sum f A) x) = (∑y∈A. (cinner x (f y)))"
by (subst (2) cinner_commute)
qed

lemmas cinner_diff [algebra_simps]  = cinner_diff_left cinner_diff_right
lemmas cinner_scaleC = cinner_scaleC_left cinner_scaleC_right

(* text ‹Legacy theorem names›
lemmas cinner_distrib = cinner_left_distrib cinner_right_distrib *)

lemma cinner_gt_zero_iff [simp]: "0 < cinner x x ⟷ x ≠ 0"
by (smt (verit) less_irrefl local.cinner_eq_zero_iff local.cinner_ge_zero order.not_eq_order_implies_strict)

(* In Inner_Product, we have
lemma power2_norm_eq_cinner: "(norm x)⇧2 = cinner x x"
The following are two ways of inserting the conversions between real and complex into this:
*)

lemma power2_norm_eq_cinner:
shows "(complex_of_real (norm x))⇧2 = (cinner x x)"
by (smt (verit, del_insts) Im_complex_of_real Re_complex_of_real cinner_gt_zero_iff cinner_zero_right cmod_def complex_eq_0 complex_eq_iff less_complex_def local.norm_eq_sqrt_cinner of_real_power real_sqrt_abs real_sqrt_pow2_iff zero_complex.sel(1))

lemma power2_norm_eq_cinner':
shows "(norm x)⇧2 = Re (cinner x x)"
by (metis Re_complex_of_real of_real_power power2_norm_eq_cinner)

text ‹Identities involving real multiplication and division.›

lemma cinner_mult_left: "cinner (of_complex m * a) b = cnj m * (cinner a b)"

lemma cinner_mult_right: "cinner a (of_complex m * b) = m * (cinner a b)"
by (metis complex_inner_class.cinner_scaleC_right scaleC_conv_of_complex)

lemma cinner_mult_left': "cinner (a * of_complex m) b = cnj m * (cinner a b)"
by (metis cinner_mult_left mult.right_neutral mult_scaleC_right scaleC_conv_of_complex)

lemma cinner_mult_right': "cinner a (b * of_complex m) = (cinner a b) * m"

(* In Inner_Product, we have
lemma Cauchy_Schwarz_ineq:
"(cinner x y)⇧2 ≤ cinner x x * cinner y y"
The following are two ways of inserting the conversions between real and complex into this:
*)

lemma Cauchy_Schwarz_ineq:
"(cinner x y) * (cinner y x) ≤ cinner x x * cinner y y"
proof (cases)
assume "y = 0"
thus ?thesis by simp
next
assume y: "y ≠ 0"
have [simp]: "cnj (cinner y y) = cinner y y" for y
by (metis cinner_commute)
define r where "r = cnj (cinner x y) / cinner y y"
have "0 ≤ cinner (x - scaleC r y) (x - scaleC r y)"
by (rule cinner_ge_zero)
also have "… = cinner x x - r * cinner x y - cnj r * cinner y x + r * cnj r * cinner y y"
unfolding cinner_diff_left cinner_diff_right cinner_scaleC_left cinner_scaleC_right
also have "… = cinner x x - cinner y x * cnj r"
unfolding r_def by auto
also have "… = cinner x x - cinner x y * cnj (cinner x y) / cinner y y"
unfolding r_def
by (metis complex_cnj_divide local.cinner_commute mult.commute times_divide_eq_left)
finally have "0 ≤ cinner x x - cinner x y * cnj (cinner x y) / cinner y y" .
hence "cinner x y * cnj (cinner x y) / cinner y y ≤ cinner x x"
thus "cinner x y * cinner y x ≤ cinner x x * cinner y y"
by (metis cinner_gt_zero_iff local.cinner_commute nice_ordered_field_class.pos_divide_le_eq y)
qed

lemma Cauchy_Schwarz_ineq2:
shows "norm (cinner x y) ≤ norm x * norm y"
proof (rule power2_le_imp_le)
have "(norm (cinner x y))^2 = Re (cinner x y * cinner y x)"
by (metis (full_types) Re_complex_of_real complex_norm_square local.cinner_commute)
also have "… ≤ Re (cinner x x * cinner y y)"
using Cauchy_Schwarz_ineq by (rule Re_mono)
also have "… = Re (complex_of_real ((norm x)^2) * complex_of_real ((norm y)^2))"
also have "… = (norm x * norm y)⇧2"
finally show "(cmod (cinner x y))^2 ≤ (norm x * norm y)⇧2" .
show "0 ≤ norm x * norm y"
qed

(* The following variant does not hold in the complex case: *)
(* lemma norm_cauchy_schwarz: "cinner x y ≤ norm x * norm y"
using Cauchy_Schwarz_ineq2 [of x y] by auto *)

subclass complex_normed_vector
proof
fix a :: complex and r :: real and x y :: 'a
show "norm x = 0 ⟷ x = 0"
unfolding norm_eq_sqrt_cinner by simp
show "norm (x + y) ≤ norm x + norm y"
proof (rule power2_le_imp_le)
have "Re (cinner x y) ≤ cmod (cinner x y)"
if "⋀x. Re x ≤ cmod x" and
"⋀x y. x ≤ y ⟹ complex_of_real x ≤ complex_of_real y"
using that by simp
hence a1: "2 * Re (cinner x y) ≤ 2 * cmod (cinner x y)"
if "⋀x. Re x ≤ cmod x" and
"⋀x y. x ≤ y ⟹ complex_of_real x ≤ complex_of_real y"
using that by simp
have "cinner x y + cinner y x = complex_of_real (2 * Re (cinner x y))"
also have "… ≤ complex_of_real (2 * cmod (cinner x y))"
using complex_Re_le_cmod complex_of_real_mono a1
by blast
also have "… = 2 * abs (cinner x y)"
unfolding abs_complex_def by simp
also have "… ≤ 2 * complex_of_real (norm x) * complex_of_real (norm y)"
using Cauchy_Schwarz_ineq2 unfolding abs_complex_def less_eq_complex_def by auto
finally have xyyx: "cinner x y + cinner y x ≤ complex_of_real (2 * norm x * norm y)"
by auto
have "complex_of_real ((norm (x + y))⇧2) = cinner (x+y) (x+y)"
also have "… = cinner x x + cinner x y + cinner y x + cinner y y"
also have "… = complex_of_real ((norm x)⇧2) + complex_of_real ((norm y)⇧2) + cinner x y + cinner y x"
also have "… ≤ complex_of_real ((norm x)⇧2) + complex_of_real ((norm y)⇧2) + complex_of_real (2 * norm x * norm y)"
using xyyx by auto
also have "… = complex_of_real ((norm x + norm y)⇧2)"
unfolding power2_sum by auto
finally show "(norm (x + y))⇧2 ≤ (norm x + norm y)⇧2"
using complex_of_real_mono_iff by blast
show "0 ≤ norm x + norm y"
unfolding norm_eq_sqrt_cinner by simp
qed
show norm_scaleC: "norm (a *⇩C x) = cmod a * norm x" for a
proof (rule power2_eq_imp_eq)
show "(norm (a *⇩C x))⇧2 = (cmod a * norm x)⇧2"
by (simp_all add: norm_eq_sqrt_cinner norm_mult power2_eq_square)
show "0 ≤ norm (a *⇩C x)"
show "0 ≤ cmod a * norm x"
qed
show "norm (r *⇩R x) = ¦r¦ * norm x"
unfolding scaleR_scaleC norm_scaleC by auto
qed

end

(* Does not hold in the complex case *)
(* lemma csquare_bound_lemma:
fixes x :: complex
shows "x < (1 + x) * (1 + x)" *)

lemma csquare_continuous:
fixes e :: real
shows "e > 0 ⟹ ∃d. 0 < d ∧ (∀y. cmod (y - x) < d ⟶ cmod (y * y - x * x) < e)"
using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]

lemma cnorm_le: "norm x ≤ norm y ⟷ cinner x x ≤ cinner y y"
by (smt (verit) complex_of_real_mono_iff norm_eq_sqrt_cinner norm_ge_zero of_real_power power2_norm_eq_cinner real_sqrt_le_mono real_sqrt_pow2)

lemma cnorm_lt: "norm x < norm y ⟷ cinner x x < cinner y y"
by (meson cnorm_le less_le_not_le)

lemma cnorm_eq: "norm x = norm y ⟷ cinner x x = cinner y y"
by (metis norm_eq_sqrt_cinner power2_norm_eq_cinner)

lemma cnorm_eq_1: "norm x = 1 ⟷ cinner x x = 1"
by (metis cinner_ge_zero cmod_Re norm_eq_sqrt_cinner norm_one of_real_1 of_real_power power2_norm_eq_cinner power2_norm_eq_cinner' real_sqrt_eq_iff real_sqrt_one)

lemma cinner_divide_left:
fixes a :: "'a :: {complex_inner,complex_div_algebra}"
shows "cinner (a / of_complex m) b = (cinner a b) / cnj m"
by (metis cinner_mult_left' complex_cnj_inverse divide_inverse mult.commute of_complex_inverse)

lemma cinner_divide_right:
fixes a :: "'a :: {complex_inner,complex_div_algebra}"
shows "cinner a (b / of_complex m) = (cinner a b) / m"
by (metis cinner_mult_right' divide_inverse of_complex_inverse)

text ‹
Re-enable constraints for \<^term>‹open›, \<^term>‹uniformity›,
\<^term>‹dist›, and \<^term>‹norm›.
›

(\<^const_name>‹open›, SOME \<^typ>‹'a::topological_space set ⇒ bool›)›

(\<^const_name>‹uniformity›, SOME \<^typ>‹('a::uniform_space × 'a) filter›)›

(\<^const_name>‹dist›, SOME \<^typ>‹'a::metric_space ⇒ 'a ⇒ real›)›

(\<^const_name>‹norm›, SOME \<^typ>‹'a::real_normed_vector ⇒ real›)›

lemma bounded_sesquilinear_cinner:
"bounded_sesquilinear (cinner::'a::complex_inner ⇒ 'a ⇒ complex)"
proof
fix x y z :: 'a and r :: complex
show "cinner (x + y) z = cinner x z + cinner y z"
show "cinner x (y + z) = cinner x y + cinner x z"
show "cinner (scaleC r x) y = scaleC (cnj r) (cinner x y)"
unfolding complex_scaleC_def by (rule cinner_scaleC_left)
show "cinner x (scaleC r y) = scaleC r (cinner x y)"
unfolding complex_scaleC_def by (rule cinner_scaleC_right)
have "∀x y::'a. norm (cinner x y) ≤ norm x * norm y * 1"
thus "∃K. ∀x y::'a. norm (cinner x y) ≤ norm x * norm y * K"
by metis
qed

lemmas tendsto_cinner [tendsto_intros] =
bounded_bilinear.tendsto [OF bounded_sesquilinear_cinner[THEN bounded_sesquilinear.bounded_bilinear]]

lemmas isCont_cinner [simp] =
bounded_bilinear.isCont [OF bounded_sesquilinear_cinner[THEN bounded_sesquilinear.bounded_bilinear]]

lemmas has_derivative_cinner [derivative_intros] =
bounded_bilinear.FDERIV [OF bounded_sesquilinear_cinner[THEN bounded_sesquilinear.bounded_bilinear]]

lemmas bounded_antilinear_cinner_left =
bounded_sesquilinear.bounded_antilinear_left [OF bounded_sesquilinear_cinner]

lemmas bounded_clinear_cinner_right =
bounded_sesquilinear.bounded_clinear_right [OF bounded_sesquilinear_cinner]

lemmas bounded_antilinear_cinner_left_comp = bounded_antilinear_cinner_left[THEN bounded_antilinear_o_bounded_clinear]

lemmas bounded_clinear_cinner_right_comp = bounded_clinear_cinner_right[THEN bounded_clinear_compose]

lemmas has_derivative_cinner_right [derivative_intros] =
bounded_linear.has_derivative [OF bounded_clinear_cinner_right[THEN bounded_clinear.bounded_linear]]

lemmas has_derivative_cinner_left [derivative_intros] =
bounded_linear.has_derivative [OF bounded_antilinear_cinner_left[THEN bounded_antilinear.bounded_linear]]

lemma differentiable_cinner [simp]:
"f differentiable (at x within s) ⟹ g differentiable at x within s ⟹ (λx. cinner (f x) (g x)) differentiable at x within s"
unfolding differentiable_def by (blast intro: has_derivative_cinner)

subsection ‹Class instances›

instantiation complex :: complex_inner
begin

definition cinner_complex_def [simp]: "cinner x y = cnj x * y"

instance
proof
fix x y z r :: complex
show "cinner x y = cnj (cinner y x)"
unfolding cinner_complex_def by auto
show "cinner (x + y) z = cinner x z + cinner y z"
unfolding cinner_complex_def
show "cinner (scaleC r x) y = cnj r * cinner x y"
unfolding cinner_complex_def complex_scaleC_def by simp
show "0 ≤ cinner x x"
by simp
show "cinner x x = 0 ⟷ x = 0"
unfolding cinner_complex_def by simp
have "cmod (Complex x1 x2) = sqrt (cmod (cinner (Complex x1 x2) (Complex x1 x2)))"
for x1 x2
unfolding cinner_complex_def complex_cnj complex_mult complex_norm
thus "norm x = sqrt (cmod (cinner x x))"
by (cases x, hypsubst_thin)
qed

end

lemma
shows complex_inner_1_left[simp]: "cinner 1 x = x"
and complex_inner_1_right[simp]: "cinner x 1 = cnj x"
by simp_all

(* No analogue to ‹instantiation complex :: real_inner› or to
lemma complex_inner_1 [simp]: "inner 1 x = Re x"
lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
lemma complex_inner_i_left [simp]: "inner 𝗂 x = Im x"
lemma complex_inner_i_right [simp]: "inner x 𝗂 = Im x"
*)

lemma cdot_square_norm: "cinner x x = complex_of_real ((norm x)⇧2)"
by (metis Im_complex_of_real Re_complex_of_real cinner_ge_zero complex_eq_iff less_eq_complex_def power2_norm_eq_cinner' zero_complex.simps(2))

lemma cnorm_eq_square: "norm x = a ⟷ 0 ≤ a ∧ cinner x x = complex_of_real (a⇧2)"
by (metis cdot_square_norm norm_ge_zero of_real_eq_iff power2_eq_iff_nonneg)

lemma cnorm_le_square: "norm x ≤ a ⟷ 0 ≤ a ∧ cinner x x ≤ complex_of_real (a⇧2)"
by (smt (verit) cdot_square_norm complex_of_real_mono_iff norm_ge_zero power2_le_imp_le)

lemma cnorm_ge_square: "norm x ≥ a ⟷ a ≤ 0 ∨ cinner x x ≥ complex_of_real (a⇧2)"
by (smt (verit, best) antisym_conv cnorm_eq_square cnorm_le_square complex_of_real_nn_iff nn_comparable zero_le_power2)

lemma norm_lt_square: "norm x < a ⟷ 0 < a ∧ cinner x x < complex_of_real (a⇧2)"
by (meson cnorm_ge_square cnorm_le_square less_le_not_le)

lemma norm_gt_square: "norm x > a ⟷ a < 0 ∨ cinner x x > complex_of_real (a⇧2)"
by (smt (verit, ccfv_SIG) cdot_square_norm complex_of_real_strict_mono_iff norm_ge_zero power2_eq_imp_eq power_mono)

text‹Dot product in terms of the norm rather than conversely.›

cinner_scaleC_left cinner_scaleC_right

(* Analogue to both dot_norm and dot_norm_neg *)
lemma cdot_norm: "cinner x y = ((norm (x+y))⇧2 - (norm (x-y))⇧2 - 𝗂 * (norm (x + 𝗂 *⇩C y))⇧2 + 𝗂 * (norm (x - 𝗂 *⇩C y))⇧2) / 4"
unfolding power2_norm_eq_cinner
cinner_diff_left cinner_diff_right ring_distribs)

lemma of_complex_inner_1 [simp]:
"cinner (of_complex x) (1 :: 'a :: {complex_inner, complex_normed_algebra_1}) = cnj x"
by (metis Complex_Inner_Product0.complex_inner_1_right cinner_complex_def cinner_mult_left complex_cnj_one norm_one of_complex_def power2_norm_eq_cinner scaleC_conv_of_complex)

lemma summable_of_complex_iff:
"summable (λx. of_complex (f x) :: 'a :: {complex_normed_algebra_1,complex_inner}) ⟷ summable f"
proof
assume *: "summable (λx. of_complex (f x) :: 'a)"
have "bounded_clinear (cinner (1::'a))"
by (rule bounded_clinear_cinner_right)
then interpret bounded_linear "λx::'a. cinner 1 x"
by (rule bounded_clinear.bounded_linear)
from summable [OF *] show "summable f"
apply (subst (asm) cinner_commute) by simp
next
assume sum: "summable f"
thus "summable (λx. of_complex (f x) :: 'a)"
by (rule summable_of_complex)
qed

definition✐‹tag important›
cgderiv :: "['a::complex_inner ⇒ complex, 'a, 'a] ⇒ bool"
("(cGDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
where
(* Must be "cinner D" not "λh. cinner h D", otherwise not even "cGDERIV id x :> 1" holds *)
"cGDERIV f x :> D ⟷ FDERIV f x :> cinner D"

lemma cgderiv_deriv [simp]: "cGDERIV f x :> D ⟷ DERIV f x :> cnj D"
by (simp only: cgderiv_def has_field_derivative_def cinner_complex_def[THEN ext])

lemma cGDERIV_DERIV_compose:
assumes "cGDERIV f x :> df" and "DERIV g (f x) :> cnj dg"
shows "cGDERIV (λx. g (f x)) x :> scaleC dg df"
proof (insert assms)
show "cGDERIV (λx. g (f x)) x :> dg *⇩C df"
if "cGDERIV f x :> df"
and "(g has_field_derivative cnj dg) (at (f x))"
unfolding cgderiv_def has_field_derivative_def cinner_scaleC_left complex_cnj_cnj
using that
by (simp add: cgderiv_def has_derivative_compose has_field_derivative_imp_has_derivative)

qed

(* Not specific to complex/real *)
(* lemma has_derivative_subst: "⟦FDERIV f x :> df; df = d⟧ ⟹ FDERIV f x :> d" *)

lemma cGDERIV_subst: "⟦cGDERIV f x :> df; df = d⟧ ⟹ cGDERIV f x :> d"
by simp

lemma cGDERIV_const: "cGDERIV (λx. k) x :> 0"
unfolding cgderiv_def cinner_zero_left[THEN ext] by (rule has_derivative_const)

"⟦cGDERIV f x :> df; cGDERIV g x :> dg⟧
⟹ cGDERIV (λx. f x + g x) x :> df + dg"

lemma cGDERIV_minus:
"cGDERIV f x :> df ⟹ cGDERIV (λx. - f x) x :> - df"
unfolding cgderiv_def cinner_minus_left[THEN ext] by (rule has_derivative_minus)

lemma cGDERIV_diff:
"⟦cGDERIV f x :> df; cGDERIV g x :> dg⟧
⟹ cGDERIV (λx. f x - g x) x :> df - dg"
unfolding cgderiv_def cinner_diff_left by (rule has_derivative_diff)

lemma cGDERIV_scaleC:
"⟦DERIV f x :> df; cGDERIV g x :> dg⟧
⟹ cGDERIV (λx. scaleC (f x) (g x)) x
:> (scaleC (cnj (f x)) dg + scaleC (cnj df) (cnj (g x)))"
apply (rule has_derivative_subst)
apply (erule (1) has_derivative_scaleC)

lemma GDERIV_mult:
"⟦cGDERIV f x :> df; cGDERIV g x :> dg⟧
⟹ cGDERIV (λx. f x * g x) x :> cnj (f x) *⇩C dg + cnj (g x) *⇩C df"
unfolding cgderiv_def
apply (rule has_derivative_subst)
apply (erule (1) has_derivative_mult)
apply (rule ext)

lemma cGDERIV_inverse:
"⟦cGDERIV f x :> df; f x ≠ 0⟧
⟹ cGDERIV (λx. inverse (f x)) x :> - cnj ((inverse (f x))⇧2) *⇩C df"
by (metis DERIV_inverse cGDERIV_DERIV_compose complex_cnj_cnj complex_cnj_minus numerals(2))

(* Don't know if this holds: *)
(* lemma cGDERIV_norm:
assumes "x ≠ 0" shows "cGDERIV (λx. norm x) x :> sgn x"
*)

lemma has_derivative_norm[derivative_intros]:
fixes x :: "'a::complex_inner"
assumes "x ≠ 0"
shows "(norm has_derivative (λh. Re (cinner (sgn x) h))) (at x)"
thm has_derivative_norm
proof -
have Re_pos: "0 < Re (cinner x x)"
using assms
by (metis Re_strict_mono cinner_gt_zero_iff zero_complex.simps(1))
have Re_plus_Re: "Re (cinner x y) + Re (cinner y x) = 2 * Re (cinner x y)"
for x y :: 'a
by (metis cinner_commute cnj.simps(1) mult_2_right semiring_normalization_rules(7))
have norm: "norm x = sqrt (Re (cinner x x))" for x :: 'a
apply (subst norm_eq_sqrt_cinner, subst cmod_Re)
using cinner_ge_zero by auto
have v2:"((λx. sqrt (Re (cinner x x))) has_derivative
(λxa. (Re (cinner x xa) + Re (cinner xa x)) * (inverse (sqrt (Re (cinner x x))) / 2))) (at x)"
by (rule derivative_eq_intros | simp add: Re_pos)+
have v1: "((λx. sqrt (Re (cinner x x))) has_derivative (λy. Re (cinner x y) / sqrt (Re (cinner x x)))) (at x)"
if "((λx. sqrt (Re (cinner x x))) has_derivative (λxa. Re (cinner x xa) * inverse (sqrt (Re (cinner x x))))) (at x)"
using that apply (subst divide_real_def)
by simp
have ‹(norm has_derivative (λy. Re (cinner x y) / norm x)) (at x)›
using v2
apply (auto simp: Re_plus_Re norm [abs_def])
using v1 by blast
then show ?thesis
by (auto simp: power2_eq_square sgn_div_norm scaleR_scaleC)
qed

bundle cinner_syntax begin
notation cinner (infix "∙⇩C" 70)
end

bundle no_cinner_syntax begin
no_notation cinner (infix "∙⇩C" 70)
end

end
```