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›.
›

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>‹uniformity›, SOME \<^typ>‹('a::uniformity × 'a) filter›)›

setup ‹Sign.add_const_constraint
  (\<^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]
  by (simp add: group_add_class.add_eq_0_iff)

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)"
  by (cases "finite A", induct set: finite, simp_all add: cinner_add_left)

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]
  by (metis complex_cnj_add local.cinner_commute)

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))"
    by (simp add: cinner_sum_left)
  thus "cnj (cinner (sum f A) x) = (∑y∈A. (cinner x (f y)))"
    by (subst (2) cinner_commute)
qed

lemmas cinner_add [algebra_simps] = cinner_add_left cinner_add_right
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_left_distrib = cinner_add_left
lemmas cinner_right_distrib = cinner_add_right
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)⇧² = 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))⇧² = (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)⇧² = 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)"
  by (simp add: of_complex_def)

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"
  by (simp add: complex_inner_class.cinner_scaleC_right of_complex_def)

(* In Inner_Product, we have
lemma Cauchy_Schwarz_ineq:
  "(cinner x y)⇧² ≤ 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
    by (smt (z3) cancel_comm_monoid_add_class.diff_cancel cancel_comm_monoid_add_class.diff_zero complex_cnj_divide group_add_class.diff_add_cancel local.cinner_commute local.cinner_eq_zero_iff local.cinner_scaleC_left mult.assoc mult.commute mult_eq_0_iff nonzero_eq_divide_eq r_def y)
  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"
    by (simp add: le_diff_eq)
  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))"
    by (simp add: power2_norm_eq_cinner)
  also have "… = (norm x * norm y)⇧²"
    by (simp add: power_mult_distrib)
  finally show "(cmod (cinner x y))^2 ≤ (norm x * norm y)⇧²" .
  show "0 ≤ norm x * norm y"
    by (simp add: local.norm_eq_sqrt_cinner)
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))"
      by (metis complex_add_cnj local.cinner_commute)
    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))⇧²) = cinner (x+y) (x+y)"
      by (simp add: power2_norm_eq_cinner)
    also have "… = cinner x x + cinner x y + cinner y x + cinner y y"
      by (simp add: cinner_add)
    also have "… = complex_of_real ((norm x)⇧²) + complex_of_real ((norm y)⇧²) + cinner x y + cinner y x"
      by (simp add: power2_norm_eq_cinner)
    also have "… ≤ complex_of_real ((norm x)⇧²) + complex_of_real ((norm y)⇧²) + complex_of_real (2 * norm x * norm y)"
      using xyyx by auto
    also have "… = complex_of_real ((norm x + norm y)⇧²)"
      unfolding power2_sum by auto
    finally show "(norm (x + y))⇧² ≤ (norm x + norm y)⇧²"
      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))⇧² = (cmod a * norm x)⇧²"
      by (simp_all add: norm_eq_sqrt_cinner norm_mult power2_eq_square)
    show "0 ≤ norm (a *⇩_C x)"
      by (simp_all add: norm_eq_sqrt_cinner)
    show "0 ≤ cmod a * norm x"
      by (simp_all add: norm_eq_sqrt_cinner)
  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]
  by (force simp add: power2_eq_square)

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 complex_of_real_cmod norm_eq_sqrt_cinner norm_one of_real_1 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›.
›

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

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

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_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"
    by (rule cinner_add_left)
  show "cinner x (y + z) = cinner x y + cinner x z"
    by (rule cinner_add_right)
  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"
    by (simp add: complex_inner_class.Cauchy_Schwarz_ineq2)
  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
    by (simp add: ring_class.ring_distribs(2))
  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
    by (simp add: power2_eq_square)
  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)⇧²)"
  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⇧²)"
  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⇧²)"
  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⇧²)"
  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⇧²)"
  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⇧²)"
  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.›

lemmas cinner_simps = cinner_add_left cinner_add_right cinner_diff_right cinner_diff_left
  cinner_scaleC_left cinner_scaleC_right

(* Analogue to both dot_norm and dot_norm_neg *)
lemma cdot_norm: "cinner x y = ((norm (x+y))⇧² - (norm (x-y))⇧² - 𝗂 * (norm (x + 𝗂 *⇩_C y))⇧² + 𝗂 * (norm (x - 𝗂 *⇩_C y))⇧²) / 4"
  unfolding power2_norm_eq_cinner
  by (simp add: power2_norm_eq_cinner cinner_add_left cinner_add_right
      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

subsection ‹Gradient derivative›

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)

lemma cGDERIV_add:
  "⟦cGDERIV f x :> df; cGDERIV g x :> dg⟧
     ⟹ cGDERIV (λx. f x + g x) x :> df + dg"
  unfolding cgderiv_def cinner_add_left[THEN ext] by (rule has_derivative_add)

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)))"
  unfolding cgderiv_def has_field_derivative_def cinner_add_left cinner_scaleC_left
  apply (rule has_derivative_subst)
   apply (erule (1) has_derivative_scaleC)
  by (simp add: ac_simps)

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)
  by (simp add: cinner_add ac_simps)

lemma cGDERIV_inverse:
  "⟦cGDERIV f x :> df; f x ≠ 0⟧
     ⟹ cGDERIV (λx. inverse (f x)) x :> - cnj ((inverse (f x))⇧²) *⇩_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