Theory Complex_Bounded_Linear_Function

```section ‹‹Complex_Bounded_Linear_Function› -- Complex bounded linear functions (bounded operators)›

(*
Authors:

Dominique Unruh, University of Tartu, unruh@ut.ee
Jose Manuel Rodriguez Caballero, University of Tartu, jose.manuel.rodriguez.caballero@ut.ee

*)

theory Complex_Bounded_Linear_Function
imports
"HOL-Types_To_Sets.Types_To_Sets"
Banach_Steinhaus.Banach_Steinhaus
Complex_Inner_Product
One_Dimensional_Spaces
Complex_Bounded_Linear_Function0
"HOL-Library.Function_Algebras"
begin

unbundle lattice_syntax

subsection ‹Misc basic facts and declarations›

notation cblinfun_apply (infixr "*⇩V" 70)

lemma id_cblinfun_apply[simp]: "id_cblinfun *⇩V ψ = ψ"
by simp

lemma apply_id_cblinfun[simp]: ‹(*⇩V) id_cblinfun = id›
by auto

lemma isCont_cblinfun_apply[simp]: "isCont ((*⇩V) A) ψ"

declare cblinfun.scaleC_left[simp]

lemma cblinfun_apply_clinear[simp]: ‹clinear (cblinfun_apply A)›
using bounded_clinear.axioms(1) cblinfun_apply by blast

lemma cblinfun_cinner_eqI:
fixes A B :: ‹'a::chilbert_space ⇒⇩C⇩L 'a›
assumes ‹⋀ψ. norm ψ = 1 ⟹ cinner ψ (A *⇩V ψ) = cinner ψ (B *⇩V ψ)›
shows ‹A = B›
proof -
define C where ‹C = A - B›
have C0[simp]: ‹cinner ψ (C ψ) = 0› for ψ
apply (cases ‹ψ = 0›)
using assms[of ‹sgn ψ›]
by (simp_all add: C_def norm_sgn sgn_div_norm cblinfun.scaleR_right assms cblinfun.diff_left cinner_diff_right)
{ fix f g α
have ‹0 = cinner (f + α *⇩C g) (C *⇩V (f + α *⇩C g))›
also have ‹… = α *⇩C cinner f (C g) + cnj α *⇩C cinner g (C f)›
finally have ‹α *⇩C cinner f (C g) = - cnj α *⇩C cinner g (C f)›
}
then have ‹cinner f (C g) = 0› for f g
by (metis complex_cnj_i complex_cnj_one complex_vector.scale_cancel_right complex_vector.scale_left_imp_eq equation_minus_iff i_squared mult_eq_0_iff one_neq_neg_one)
then have ‹C g = 0› for g
using cinner_eq_zero_iff by blast
then have ‹C = 0›
then show ‹A = B›
using C_def by auto
qed

lemma id_cblinfun_not_0[simp]: ‹(id_cblinfun :: 'a::{complex_normed_vector, not_singleton} ⇒⇩C⇩L _) ≠ 0›
by (metis (full_types) Extra_General.UNIV_not_singleton cblinfun.zero_left cblinfun_id_cblinfun_apply ex_norm1 norm_zero one_neq_zero)

lemma cblinfun_norm_geqI:
assumes ‹norm (f *⇩V x) / norm x ≥ K›
shows ‹norm f ≥ K›
using assms by transfer (smt (z3) bounded_clinear.bounded_linear le_onorm)

(* This lemma is proven in Complex_Bounded_Linear_Function0 but we add the [simp]
only here because we try to keep Complex_Bounded_Linear_Function0 as close to
Bounded_Linear_Function as possible. *)
declare scaleC_conv_of_complex[simp]

lemma cblinfun_eq_0_on_span:
fixes S::‹'a::complex_normed_vector set›
assumes "x ∈ cspan S"
and "⋀s. s∈S ⟹ F *⇩V s = 0"
shows ‹F *⇩V x = 0›
using bounded_clinear.axioms(1) cblinfun_apply assms complex_vector.linear_eq_0_on_span
by blast

lemma cblinfun_eq_on_span:
fixes S::‹'a::complex_normed_vector set›
assumes "x ∈ cspan S"
and "⋀s. s∈S ⟹ F *⇩V s = G *⇩V s"
shows ‹F *⇩V x = G *⇩V x›
using bounded_clinear.axioms(1) cblinfun_apply assms complex_vector.linear_eq_on_span
by blast

lemma cblinfun_eq_0_on_UNIV_span:
fixes basis::‹'a::complex_normed_vector set›
assumes "cspan basis = UNIV"
and "⋀s. s∈basis ⟹ F *⇩V s = 0"
shows ‹F = 0›
by (metis cblinfun_eq_0_on_span UNIV_I assms cblinfun.zero_left cblinfun_eqI)

lemma cblinfun_eq_on_UNIV_span:
fixes basis::"'a::complex_normed_vector set" and φ::"'a ⇒ 'b::complex_normed_vector"
assumes "cspan basis = UNIV"
and "⋀s. s∈basis ⟹ F *⇩V s = G *⇩V s"
shows ‹F = G›
by (metis (no_types) assms cblinfun_eqI cblinfun_eq_on_span iso_tuple_UNIV_I)

lemma cblinfun_eq_on_canonical_basis:
fixes f g::"'a::{basis_enum,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector"
defines "basis == set (canonical_basis::'a list)"
assumes "⋀u. u ∈ basis ⟹ f *⇩V u = g *⇩V u"
shows  "f = g"
using assms cblinfun_eq_on_UNIV_span is_generator_set by blast

lemma cblinfun_eq_0_on_canonical_basis:
fixes f ::"'a::{basis_enum,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector"
defines "basis == set (canonical_basis::'a list)"
assumes "⋀u. u ∈ basis ⟹ f *⇩V u = 0"
shows  "f = 0"

lemma cinner_canonical_basis_eq_0:
defines "basisA == set (canonical_basis::'a::onb_enum list)"
and   "basisB == set (canonical_basis::'b::onb_enum list)"
assumes "⋀u v. u∈basisA ⟹ v∈basisB ⟹ is_orthogonal v (F *⇩V u)"
shows "F = 0"
proof-
have "F *⇩V u = 0"
if "u∈basisA" for u
proof-
have "⋀v. v∈basisB ⟹ is_orthogonal v (F *⇩V u)"
moreover have "(⋀v. v∈basisB ⟹ is_orthogonal v x) ⟹ x = 0"
for x
proof-
assume r1: "⋀v. v∈basisB ⟹ is_orthogonal v x"
have "is_orthogonal v x" for v
proof-
have "cspan basisB = UNIV"
using basisB_def is_generator_set  by auto
hence "v ∈ cspan basisB"
by (smt iso_tuple_UNIV_I)
hence "∃t s. v = (∑a∈t. s a *⇩C a) ∧ finite t ∧ t ⊆ basisB"
using complex_vector.span_explicit
by (smt mem_Collect_eq)
then obtain t s where b1: "v = (∑a∈t. s a *⇩C a)" and b2: "finite t" and b3: "t ⊆ basisB"
by blast
have "v ∙⇩C x = (∑a∈t. s a *⇩C a) ∙⇩C x"
also have "… = (∑a∈t. (s a *⇩C a) ∙⇩C x)"
using cinner_sum_left by blast
also have "… = (∑a∈t. cnj (s a) * (a ∙⇩C x))"
by auto
also have "… = 0"
using b3 r1 subsetD by force
finally show ?thesis by simp
qed
thus ?thesis
by (simp add: ‹⋀v. (v ∙⇩C x) = 0› cinner_extensionality)
qed
ultimately show ?thesis by simp
qed
thus ?thesis
using basisA_def cblinfun_eq_0_on_canonical_basis by auto
qed

lemma cinner_canonical_basis_eq:
defines "basisA == set (canonical_basis::'a::onb_enum list)"
and   "basisB == set (canonical_basis::'b::onb_enum list)"
assumes "⋀u v. u∈basisA ⟹ v∈basisB ⟹ v ∙⇩C (F *⇩V u) = v ∙⇩C (G *⇩V u)"
shows "F = G"
proof-
define H where "H = F - G"
have "⋀u v. u∈basisA ⟹ v∈basisB ⟹ is_orthogonal v (H *⇩V u)"
unfolding H_def
by (simp add: assms(3) cinner_diff_right minus_cblinfun.rep_eq)
hence "H = 0"
by (simp add: basisA_def basisB_def cinner_canonical_basis_eq_0)
thus ?thesis unfolding H_def by simp
qed

lemma cinner_canonical_basis_eq':
defines "basisA == set (canonical_basis::'a::onb_enum list)"
and   "basisB == set (canonical_basis::'b::onb_enum list)"
assumes "⋀u v. u∈basisA ⟹ v∈basisB ⟹ (F *⇩V u) ∙⇩C v = (G *⇩V u) ∙⇩C v"
shows "F = G"
using cinner_canonical_basis_eq assms
by (metis cinner_commute')

lemma not_not_singleton_cblinfun_zero:
‹x = 0› if ‹¬ class.not_singleton TYPE('a)› for x :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector›
apply (rule cblinfun_eqI)
apply (subst not_not_singleton_zero[OF that])
by simp

lemma cblinfun_norm_approx_witness:
fixes A :: ‹'a::{not_singleton,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹ε > 0›
shows ‹∃ψ. norm (A *⇩V ψ) ≥ norm A - ε ∧ norm ψ = 1›
proof (transfer fixing: ε)
fix A :: ‹'a ⇒ 'b› assume [simp]: ‹bounded_clinear A›
have ‹∃y∈{norm (A x) |x. norm x = 1}. y > ⨆ {norm (A x) |x. norm x = 1} - ε›
apply (rule Sup_real_close)
using assms by (auto simp: ex_norm1 bounded_clinear.bounded_linear bdd_above_norm_f)
also have ‹⨆ {norm (A x) |x. norm x = 1} = onorm A›
finally
show ‹∃ψ. onorm A - ε ≤ norm (A ψ) ∧ norm ψ = 1›
by force
qed

lemma cblinfun_norm_approx_witness_mult:
fixes A :: ‹'a::{not_singleton,complex_normed_vector} ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹ε < 1›
shows ‹∃ψ.  norm (A *⇩V ψ) ≥ norm A * ε ∧ norm ψ = 1›
proof (cases ‹norm A = 0›)
case True
then show ?thesis
next
case False
then have ‹(1 - ε) * norm A > 0›
using assms by fastforce
then obtain ψ where geq: ‹norm (A *⇩V ψ) ≥ norm A - ((1 - ε) * norm A)› and ‹norm ψ = 1›
using cblinfun_norm_approx_witness by blast
have ‹norm A * ε = norm A - (1 - ε) * norm A›
also have ‹… ≤ norm (A *⇩V ψ)›
by (rule geq)
finally show ?thesis
using ‹norm ψ = 1› by auto
qed

lemma cblinfun_norm_approx_witness':
fixes A :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector›
assumes ‹ε > 0›
shows ‹∃ψ. norm (A *⇩V ψ) / norm ψ ≥ norm A - ε›
proof (cases ‹class.not_singleton TYPE('a)›)
case True
obtain ψ where ‹norm (A *⇩V ψ) ≥ norm A - ε› and ‹norm ψ = 1›
apply atomize_elim
using complex_normed_vector_axioms True assms
by (rule cblinfun_norm_approx_witness[internalize_sort' 'a])
then have ‹norm (A *⇩V ψ) / norm ψ ≥ norm A - ε›
by simp
then show ?thesis
by auto
next
case False
show ?thesis
apply (subst not_not_singleton_cblinfun_zero[OF False])
apply simp
apply (subst not_not_singleton_cblinfun_zero[OF False])
using ‹ε > 0› by simp
qed

lemma cblinfun_to_CARD_1_0[simp]: ‹(A :: _ ⇒⇩C⇩L _::CARD_1) = 0›

lemma cblinfun_from_CARD_1_0[simp]: ‹(A :: _::CARD_1 ⇒⇩C⇩L _) = 0›
using cblinfun_eq_on_UNIV_span by force

lemma cblinfun_cspan_UNIV:
fixes basis :: ‹('a::{complex_normed_vector,cfinite_dim} ⇒⇩C⇩L 'b::complex_normed_vector) set›
and basisA :: ‹'a set› and basisB :: ‹'b set›
assumes ‹cspan basisA = UNIV› and ‹cspan basisB = UNIV›
assumes basis: ‹⋀a b. a∈basisA ⟹ b∈basisB ⟹ ∃F∈basis. ∀a'∈basisA. F *⇩V a' = (if a'=a then b else 0)›
shows ‹cspan basis = UNIV›
proof -
obtain basisA' where ‹basisA' ⊆ basisA› and ‹cindependent basisA'› and ‹cspan basisA' = UNIV›
by (metis assms(1) complex_vector.maximal_independent_subset complex_vector.span_eq top_greatest)
then have [simp]: ‹finite basisA'›
have basis': ‹⋀a b. a∈basisA' ⟹ b∈basisB ⟹ ∃F∈basis. ∀a'∈basisA'. F *⇩V a' = (if a'=a then b else 0)›
using basis ‹basisA' ⊆ basisA› by fastforce

obtain F where F: ‹F a b ∈ basis ∧ F a b *⇩V a' = (if a'=a then b else 0)›
if ‹a∈basisA'› ‹b∈basisB› ‹a'∈basisA'› for a b a'
apply atomize_elim apply (intro choice allI)
using basis' by metis
then have F_apply: ‹F a b *⇩V a' = (if a'=a then b else 0)›
if ‹a∈basisA'› ‹b∈basisB› ‹a'∈basisA'› for a b a'
using that by auto
have F_basis: ‹F a b ∈ basis›
if ‹a∈basisA'› ‹b∈basisB› for a b
using that F by auto
have b_span: ‹∃G∈cspan {F a b|b. b∈basisB}. ∀a'∈basisA'. G *⇩V a' = (if a'=a then b else 0)› if ‹a∈basisA'› for a b
proof -
from ‹cspan basisB = UNIV›
obtain r t where ‹finite t› and ‹t ⊆ basisB› and b_lincom: ‹b = (∑a∈t. r a *⇩C a)›
unfolding complex_vector.span_alt by atomize_elim blast
define G where ‹G = (∑i∈t. r i *⇩C F a i)›
have ‹G ∈ cspan {F a b|b. b∈basisB}›
using ‹finite t› ‹t ⊆ basisB› unfolding G_def
by (smt (verit) complex_vector.span_scale complex_vector.span_sum complex_vector.span_superset mem_Collect_eq subsetD)
moreover have ‹G *⇩V a' = (if a'=a then b else 0)› if ‹a'∈basisA'› for a'
using ‹t ⊆ basisB› ‹a∈basisA'› ‹a'∈basisA'›
by (auto simp: b_lincom G_def cblinfun.sum_left F_apply intro!: sum.neutral sum.cong)
ultimately show ?thesis
by blast
qed

have a_span: ‹cspan (⋃a∈basisA'. cspan {F a b|b. b∈basisB}) = UNIV›
proof (intro equalityI subset_UNIV subsetI, rename_tac H)
fix H
obtain G where G: ‹G a b ∈ cspan {F a b|b. b∈basisB} ∧ G a b *⇩V a' = (if a'=a then b else 0)›
if ‹a∈basisA'› and ‹a'∈basisA'› for a b a'
apply atomize_elim apply (intro choice allI)
using b_span by blast
then have G_cspan: ‹G a b ∈ cspan {F a b|b. b∈basisB}› if ‹a∈basisA'› for a b
using that by auto
from G have G: ‹G a b *⇩V a' = (if a'=a then b else 0)› if ‹a∈basisA'› and ‹a'∈basisA'› for a b a'
using that by auto
define H' where ‹H' = (∑a∈basisA'. G a (H *⇩V a))›
have ‹H' ∈ cspan (⋃a∈basisA'. cspan {F a b|b. b∈basisB})›
unfolding H'_def using G_cspan
by (smt (verit, del_insts) UN_iff complex_vector.span_clauses(1) complex_vector.span_sum)
moreover have ‹H' = H›
using ‹cspan basisA' = UNIV›
by (auto simp: H'_def cblinfun_eq_on_UNIV_span cblinfun.sum_left G)
ultimately show ‹H ∈ cspan (⋃a∈basisA'. cspan {F a b |b. b ∈ basisB})›
by simp
qed

moreover have ‹cspan basis ⊇ cspan (⋃a∈basisA'. cspan {F a b|b. b∈basisB})›
by (smt (verit) F_basis UN_subset_iff complex_vector.span_base complex_vector.span_minimal complex_vector.subspace_span mem_Collect_eq subsetI)

ultimately show ‹cspan basis = UNIV›
by auto
qed

instance cblinfun :: (‹{cfinite_dim,complex_normed_vector}›, ‹{cfinite_dim,complex_normed_vector}›) cfinite_dim
proof intro_classes
obtain basisA :: ‹'a set› where [simp]: ‹cspan basisA = UNIV› ‹cindependent basisA› ‹finite basisA›
using finite_basis by blast
obtain basisB :: ‹'b set› where [simp]: ‹cspan basisB = UNIV› ‹cindependent basisB› ‹finite basisB›
using finite_basis by blast
define f where ‹f a b = cconstruct basisA (λx. if x=a then b else 0)› for a :: 'a and b :: 'b
have f_a: ‹f a b a = b› if ‹a : basisA› for a b
by (simp add: complex_vector.construct_basis f_def that)
have f_not_a: ‹f a b c = 0› if ‹a : basisA› and ‹c : basisA› and ‹a ≠ c›for a b c
using that by (simp add: complex_vector.construct_basis f_def)
define F where ‹F a b = CBlinfun (f a b)› for a b
have ‹clinear (f a b)› for a b
by (auto intro: complex_vector.linear_construct simp: f_def)
then have ‹bounded_clinear (f a b)› for a b
by auto
then have F_apply: ‹cblinfun_apply (F a b) = f a b› for a b
define basis where ‹basis = {F a b| a b. a∈basisA ∧ b∈basisB}›
have "⋀a b. ⟦a ∈ basisA; b ∈ basisB⟧ ⟹ ∃F∈basis. ∀a'∈basisA. F *⇩V a' = (if a' = a then b else 0)"
by (smt (verit, del_insts) F_apply basis_def f_a f_not_a mem_Collect_eq)
then have ‹cspan basis = UNIV›
by (metis ‹cspan basisA = UNIV› ‹cspan basisB = UNIV› cblinfun_cspan_UNIV)

moreover have ‹finite basis›
unfolding basis_def by (auto intro: finite_image_set2)
ultimately show ‹∃S :: ('a ⇒⇩C⇩L 'b) set. finite S ∧ cspan S = UNIV›
by auto
qed

lemma norm_cblinfun_bound_dense:
assumes ‹0 ≤ b›
assumes S: ‹closure S = UNIV›
assumes bound: ‹⋀x. x∈S ⟹ norm (cblinfun_apply f x) ≤ b * norm x›
shows ‹norm f ≤ b›
proof -
have 1: ‹continuous_on UNIV (λa. norm (f *⇩V a))›
have 2: ‹continuous_on UNIV (λa. b * norm a)›
using continuous_on_mult_left continuous_on_norm_id by blast
have ‹norm (cblinfun_apply f x) ≤ b * norm x› for x
by (metis (mono_tags, lifting) UNIV_I S bound 1 2 on_closure_leI)
then show ‹norm f ≤ b›
using ‹0 ≤ b› norm_cblinfun_bound by blast
qed

lemma infsum_cblinfun_apply:
assumes ‹g summable_on S›
shows ‹infsum (λx. A *⇩V g x) S = A *⇩V (infsum g S)›
using infsum_bounded_linear[unfolded o_def] assms cblinfun.real.bounded_linear_right by blast

lemma has_sum_cblinfun_apply:
assumes ‹(g has_sum x) S›
shows ‹((λx. A *⇩V g x) has_sum (A *⇩V x)) S›
using assms has_sum_bounded_linear[unfolded o_def] using cblinfun.real.bounded_linear_right by blast

lemma abs_summable_on_cblinfun_apply:
assumes ‹g abs_summable_on S›
shows ‹(λx. A *⇩V g x) abs_summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_right] assms
by (rule abs_summable_on_bounded_linear[unfolded o_def])

lemma summable_on_cblinfun_apply:
assumes ‹g summable_on S›
shows ‹(λx. A *⇩V g x) summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_right] assms
by (rule summable_on_bounded_linear[unfolded o_def])

lemma summable_on_cblinfun_apply_left:
assumes ‹A summable_on S›
shows ‹(λx. A x *⇩V g) summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_left] assms
by (rule summable_on_bounded_linear[unfolded o_def])

lemma abs_summable_on_cblinfun_apply_left:
assumes ‹A abs_summable_on S›
shows ‹(λx. A x *⇩V g) abs_summable_on S›
using bounded_clinear.bounded_linear[OF cblinfun.bounded_clinear_left] assms
by (rule abs_summable_on_bounded_linear[unfolded o_def])
lemma infsum_cblinfun_apply_left:
assumes ‹A summable_on S›
shows ‹infsum (λx. A x *⇩V g) S = (infsum A S) *⇩V g›
apply (rule infsum_bounded_linear[unfolded o_def, of ‹λA. cblinfun_apply A g›])
using assms
by (auto simp add: bounded_clinear.bounded_linear bounded_cbilinear_cblinfun_apply)
lemma has_sum_cblinfun_apply_left:
assumes ‹(A has_sum x) S›
shows ‹((λx. A x *⇩V g) has_sum (x *⇩V g)) S›
apply (rule has_sum_bounded_linear[unfolded o_def, of ‹λA. cblinfun_apply A g›])
using assms by (auto simp add: bounded_clinear.bounded_linear cblinfun.bounded_clinear_left)

text ‹The next eight lemmas logically belong in \<^theory>‹Complex_Bounded_Operators.Complex_Inner_Product›
but the proofs use facts from this theory.›
lemma has_sum_cinner_left:
assumes ‹(f has_sum x) I›
shows ‹((λi. cinner a (f i)) has_sum cinner a x) I›
by (metis assms cblinfun_cinner_right.rep_eq has_sum_cblinfun_apply)

lemma summable_on_cinner_left:
assumes ‹f summable_on I›
shows ‹(λi. cinner a (f i)) summable_on I›
by (metis assms has_sum_cinner_left summable_on_def)

lemma infsum_cinner_left:
assumes ‹φ summable_on I›
shows ‹cinner ψ (∑⇩∞i∈I. φ i) = (∑⇩∞i∈I. cinner ψ (φ i))›
by (metis assms has_sum_cinner_left has_sum_infsum infsumI)

lemma has_sum_cinner_right:
assumes ‹(f has_sum x) I›
shows ‹((λi. f i ∙⇩C a) has_sum (x ∙⇩C a)) I›
using assms has_sum_bounded_linear[unfolded o_def] bounded_antilinear.bounded_linear
bounded_antilinear_cinner_left by blast

lemma summable_on_cinner_right:
assumes ‹f summable_on I›
shows ‹(λi. f i ∙⇩C a) summable_on I›
by (metis assms has_sum_cinner_right summable_on_def)

lemma infsum_cinner_right:
assumes ‹φ summable_on I›
shows ‹(∑⇩∞i∈I. φ i) ∙⇩C ψ = (∑⇩∞i∈I. φ i ∙⇩C ψ)›
by (metis assms has_sum_cinner_right has_sum_infsum infsumI)

lemma Cauchy_cinner_product_summable:
assumes asum: ‹a summable_on UNIV›
assumes bsum: ‹b summable_on UNIV›
assumes ‹finite X› ‹finite Y›
assumes pos: ‹⋀x y. x ∉ X ⟹ y ∉ Y ⟹ cinner (a x) (b y) ≥ 0›
shows absum: ‹(λ(x, y). cinner (a x) (b y)) summable_on UNIV›
proof -
have ‹(∑(x,y)∈F. norm (cinner (a x) (b y))) ≤ norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) + norm (infsum b (-Y)) + 1›
if ‹finite F› and ‹F ⊆ (-X)×(-Y)› for F
proof -
from asum ‹finite X›
have ‹a summable_on (-X)›
then obtain MA where ‹finite MA› and ‹MA ⊆ -X›
and MA: ‹G ⊇ MA ⟹ G ⊆ -X ⟹ finite G ⟹ norm (sum a G - infsum a (-X)) ≤ 1› for G
apply (simp add: summable_iff_has_sum_infsum has_sum_metric dist_norm)
by (meson less_eq_real_def zero_less_one)

from bsum ‹finite Y›
have ‹b summable_on (-Y)›
then obtain MB where ‹finite MB› and ‹MB ⊆ -Y›
and MB: ‹G ⊇ MB ⟹ G ⊆ -Y ⟹ finite G ⟹ norm (sum b G - infsum b (-Y)) ≤ 1› for G
apply (simp add: summable_iff_has_sum_infsum has_sum_metric dist_norm)
by (meson less_eq_real_def zero_less_one)

define F1 F2 where ‹F1 = fst ` F ∪ MA› and ‹F2 = snd ` F ∪ MB›
define t1 t2 where ‹t1 = sum a F1 - infsum a (-X)› and ‹t2 = sum b F2 - infsum b (-Y)›

have [simp]: ‹finite F1› ‹finite F2›
using F1_def F2_def ‹finite MA› ‹finite MB› that by auto
have [simp]: ‹F1 ⊆ -X› ‹F2 ⊆ -Y›
using ‹F ⊆ (-X)×(-Y)› ‹MA ⊆ -X› ‹MB ⊆ -Y›
by (auto simp: F1_def F2_def)
from MA[OF _ ‹F1 ⊆ -X› ‹finite F1›] have ‹norm t1 ≤ 1›
by (auto simp: t1_def F1_def)
from MB[OF _ ‹F2 ⊆ -Y› ‹finite F2›] have ‹norm t2 ≤ 1›
by (auto simp: t2_def F2_def)
have [simp]: ‹F ⊆ F1 × F2›
by (force simp: F1_def F2_def image_def)
have ‹(∑(x,y)∈F. norm (cinner (a x) (b y))) ≤ (∑(x,y)∈F1×F2. norm (cinner (a x) (b y)))›
by (intro sum_mono2) auto
also have "... = (∑x∈F1 × F2. norm (a (fst x) ∙⇩C b (snd x)))"
by (auto  simp: case_prod_beta)
also have "... =  norm (∑x∈F1 × F2. a (fst x) ∙⇩C b (snd x))"
proof -
have "(∑x∈F1 × F2. ¦a (fst x) ∙⇩C b (snd x)¦) = ¦∑x∈F1 × F2. a (fst x) ∙⇩C b (snd x)¦"
by (smt (verit, best) pos sum.cong sum_nonneg ComplD SigmaE ‹F1 ⊆ - X› ‹F2 ⊆ - Y› abs_pos prod.sel subset_iff)
then show ?thesis
by (smt (verit) abs_complex_def norm_ge_zero norm_of_real o_def of_real_sum sum.cong sum_norm_le)
qed
also from pos have ‹… = norm (∑(x,y)∈F1×F2. cinner (a x) (b y))›
by (auto simp: case_prod_beta)
also have ‹… = norm (cinner (sum a F1) (sum b F2))›
also have ‹… = norm (cinner (infsum a (-X) + t1) (infsum b (-Y) + t2))›
also have ‹… ≤ norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) * norm t2 + norm t1 * norm (infsum b (-Y)) + norm t1 * norm t2›
by (smt (verit, del_insts) complex_inner_class.Cauchy_Schwarz_ineq2 norm_triangle_ineq)
also from ‹norm t1 ≤ 1› ‹norm t2 ≤ 1›
have ‹… ≤ norm (cinner (infsum a (-X)) (infsum b (-Y))) + norm (infsum a (-X)) + norm (infsum b (-Y)) + 1›
by (auto intro!: add_mono mult_left_le mult_left_le_one_le mult_le_one)
finally show ?thesis
by -
qed

then have ‹(λ(x, y). cinner (a x) (b y)) abs_summable_on (-X)×(-Y)›
apply (rule_tac nonneg_bdd_above_summable_on)
by (auto intro!: bdd_aboveI2 simp: case_prod_unfold)
then have 1: ‹(λ(x, y). cinner (a x) (b y)) summable_on (-X)×(-Y)›
using abs_summable_summable by blast

from bsum
have ‹(λy. b y) summable_on (-Y)›
by (simp add: Compl_eq_Diff_UNIV assms(4) summable_on_cofin_subset)
then have ‹(λy. cinner (a x) (b y)) summable_on (-Y)› for x
using summable_on_cinner_left by blast
with ‹finite X› have 2: ‹(λ(x, y). cinner (a x) (b y)) summable_on X×(-Y)›
by (force intro: summable_on_product_finite_left)

from asum
have ‹(λx. a x) summable_on (-X)›
by (simp add: Compl_eq_Diff_UNIV assms(3) summable_on_cofin_subset)
then have ‹(λx. cinner (a x) (b y)) summable_on (-X)› for y
using summable_on_cinner_right by blast
with ‹finite Y› have 3: ‹(λ(x, y). cinner (a x) (b y)) summable_on (-X)×Y›
by (force intro: summable_on_product_finite_right)

have 4: ‹(λ(x, y). cinner (a x) (b y)) summable_on X×Y›
by (simp add: ‹finite X› ‹finite Y›)

have §: "UNIV = ((-X) × -Y) ∪ (X × -Y) ∪ ((-X) × Y) ∪ (X × Y)"
by auto
show ?thesis
using 1 2 3 4 by (force simp: § intro!: summable_on_Un_disjoint)
qed

text ‹A variant of @{thm [source] Series.Cauchy_product_sums} with \<^term>‹(*)› replaced by \<^term>‹cinner›.
Differently from @{thm [source] Series.Cauchy_product_sums}, we do not require absolute summability
of \<^term>‹a› and \<^term>‹b› individually but only unconditional summability of \<^term>‹a›, \<^term>‹b›, and their product.
While on, e.g., reals, unconditional summability is equivalent to absolute summability, in
general unconditional summability is a weaker requirement.

Logically belong in \<^theory>‹Complex_Bounded_Operators.Complex_Inner_Product›
but the proof uses facts from this theory.›
lemma
fixes a b :: "nat ⇒ 'a::complex_inner"
assumes asum: ‹a summable_on UNIV›
assumes bsum: ‹b summable_on UNIV›
assumes absum: ‹(λ(x, y). cinner (a x) (b y)) summable_on UNIV›
(* ― ‹See @{thm [source] Cauchy_cinner_product_summable} or @{thm [source] Cauchy_cinner_product_summable'} for a way to rewrite this premise.› *)
shows Cauchy_cinner_product_infsum: ‹(∑⇩∞k. ∑i≤k. cinner (a i) (b (k - i))) = cinner (∑⇩∞k. a k) (∑⇩∞k. b k)›
and Cauchy_cinner_product_infsum_exists: ‹(λk. ∑i≤k. cinner (a i) (b (k - i))) summable_on UNIV›
proof -
have img: ‹(λ(k::nat, i). (i, k - i)) ` {(k, i). i ≤ k} = UNIV›
apply (auto simp: image_def)
have inj: ‹inj_on (λ(k::nat, i). (i, k - i)) {(k, i). i ≤ k}›
by (smt (verit, del_insts) Pair_inject case_prodE case_prod_conv eq_diff_iff inj_onI mem_Collect_eq)
have sigma: ‹(SIGMA k:UNIV. {i. i ≤ k}) = {(k, i). i ≤ k}›
by auto

from absum
have §: ‹(λ(x, y). cinner (a y) (b (x - y))) summable_on {(k, i). i ≤ k}›
by (rule Cauchy_cinner_product_summable'[THEN iffD1])
then have ‹(λk. ∑⇩∞i|i≤k. cinner (a i) (b (k-i))) summable_on UNIV›
by (metis (mono_tags, lifting) sigma summable_on_Sigma_banach summable_on_cong)
then show ‹(λk. ∑i≤k. cinner (a i) (b (k - i))) summable_on UNIV›
by (metis (mono_tags, lifting) atMost_def finite_Collect_le_nat infsum_finite summable_on_cong)

have ‹cinner (∑⇩∞k. a k) (∑⇩∞k. b k) = (∑⇩∞k. ∑⇩∞l. cinner (a k) (b l))›
by (smt (verit, best) asum bsum infsum_cinner_left infsum_cinner_right infsum_cong)
also have ‹… = (∑⇩∞(k,l). cinner (a k) (b l))›
by (smt (verit) UNIV_Times_UNIV infsum_Sigma'_banach infsum_cong local.absum)
also have ‹… = (∑⇩∞(k, l)∈(λ(k, i). (i, k - i)) ` {(k, i). i ≤ k}. cinner (a k) (b l))›
by (simp only: img)
also have ‹… = infsum ((λ(k, l). a k ∙⇩C b l) ∘ (λ(k, i). (i, k - i))) {(k, i). i ≤ k}›
using inj by (rule infsum_reindex)
also have ‹… = (∑⇩∞(k,i)|i≤k. a i ∙⇩C b (k-i))›
also have ‹… = (∑⇩∞k. ∑⇩∞i|i≤k. a i ∙⇩C b (k-i))›
by (metis (no_types) § infsum_Sigma'_banach sigma)
also have ‹… = (∑⇩∞k. ∑i≤k. a i ∙⇩C b (k-i))›
finally show ‹(∑⇩∞k. ∑i≤k. a i ∙⇩C b (k - i)) = (∑⇩∞k. a k) ∙⇩C (∑⇩∞k. b k)›
by simp
qed

lemma CBlinfun_plus:
assumes [simp]: ‹bounded_clinear f› ‹bounded_clinear g›
shows ‹CBlinfun (f + g) = CBlinfun f + CBlinfun g›

lemma CBlinfun_scaleC:
assumes ‹bounded_clinear f›
shows ‹CBlinfun (λy. c *⇩C f y) = c *⇩C CBlinfun f›
by (simp add: assms eq_onp_same_args scaleC_cblinfun.abs_eq)

lemma cinner_sup_norm_cblinfun:
fixes A :: ‹'a::{complex_normed_vector,not_singleton} ⇒⇩C⇩L 'b::complex_inner›
shows ‹norm A = (SUP (ψ,φ). cmod (cinner ψ (A *⇩V φ)) / (norm ψ * norm φ))›
apply transfer
apply (rule cinner_sup_onorm)

lemma norm_cblinfun_Sup: ‹norm A = (SUP ψ. norm (A *⇩V ψ) / norm ψ)›

lemma cblinfun_eq_on:
fixes A B :: "'a::cbanach ⇒⇩C⇩L'b::complex_normed_vector"
assumes "⋀x. x ∈ G ⟹ A *⇩V x = B *⇩V x" and ‹t ∈ closure (cspan G)›
shows "A *⇩V t = B *⇩V t"
using assms
apply transfer
using bounded_clinear_eq_on_closure by blast

lemma cblinfun_eq_gen_eqI:
fixes A B :: "'a::cbanach ⇒⇩C⇩L'b::complex_normed_vector"
assumes "⋀x. x ∈ G ⟹ A *⇩V x = B *⇩V x" and ‹ccspan G = ⊤›
shows "A = B"
by (metis assms cblinfun_eqI cblinfun_eq_on ccspan.rep_eq iso_tuple_UNIV_I top_ccsubspace.rep_eq)

declare cnj_bounded_antilinear[bounded_antilinear]

lemma Cblinfun_comp_bounded_cbilinear: ‹bounded_clinear (CBlinfun o p)› if ‹bounded_cbilinear p›
by (metis bounded_cbilinear.bounded_clinear_prod_right bounded_cbilinear.prod_right_def comp_id map_fun_def that)

lemma Cblinfun_comp_bounded_sesquilinear: ‹bounded_antilinear (CBlinfun o p)› if ‹bounded_sesquilinear p›
by (metis (mono_tags, opaque_lifting) bounded_clinear_CBlinfun_apply bounded_sesquilinear.bounded_clinear_right comp_apply that transfer_bounded_sesquilinear_bounded_antilinearI)

subsection ‹Relationship to real bounded operators (\<^typ>‹_ ⇒⇩L _›)›

instantiation blinfun :: (real_normed_vector, complex_normed_vector) "complex_normed_vector"
begin
lift_definition scaleC_blinfun :: ‹complex ⇒
('a::real_normed_vector, 'b::complex_normed_vector) blinfun ⇒
('a, 'b) blinfun›
is ‹λ c::complex. λ f::'a⇒'b. (λ x. c *⇩C (f x) )›
proof
fix c::complex and f :: ‹'a⇒'b› and b1::'a and b2::'a
assume ‹bounded_linear f›
show ‹c *⇩C f (b1 + b2) = c *⇩C f b1 + c *⇩C f b2›

fix c::complex and f :: ‹'a⇒'b› and b::'a and r::real
assume ‹bounded_linear f›
show ‹c *⇩C f (r *⇩R b) = r *⇩R (c *⇩C f b)›
by (simp add: ‹bounded_linear f› linear_simps(5) scaleR_scaleC)

fix c::complex and f :: ‹'a⇒'b›
assume ‹bounded_linear f›

have ‹∃ K. ∀ x. norm (f x) ≤ norm x * K›
using ‹bounded_linear f›
then obtain K where ‹∀ x. norm (f x) ≤ norm x * K›
by blast
have ‹cmod c ≥ 0›
by simp
hence ‹∀ x. (cmod c) * norm (f x) ≤ (cmod c) * norm x * K›
using  ‹∀ x. norm (f x) ≤ norm x * K›
by (metis ordered_comm_semiring_class.comm_mult_left_mono vector_space_over_itself.scale_scale)
moreover have ‹norm (c *⇩C f x) = (cmod c) * norm (f x)›
for x
by simp
ultimately show ‹∃K. ∀x. norm (c *⇩C f x) ≤ norm x * K›
by (metis ab_semigroup_mult_class.mult_ac(1) mult.commute)
qed

instance
proof
have "r *⇩R x = complex_of_real r *⇩C x"
for x :: "('a, 'b) blinfun" and r
thus "((*⇩R) r::'a ⇒⇩L 'b ⇒ _) = (*⇩C) (complex_of_real r)" for r
by auto
show "a *⇩C (x + y) = a *⇩C x + a *⇩C y"
for a :: complex and x y :: "'a ⇒⇩L 'b"

show "(a + b) *⇩C x = a *⇩C x + b *⇩C x"
for a b :: complex and x :: "'a ⇒⇩L 'b"

show "a *⇩C b *⇩C x = (a * b) *⇩C x"
for a b :: complex and x :: "'a ⇒⇩L 'b"
by transfer simp

have ‹1 *⇩C f x = f x›
for f :: ‹'a⇒'b› and x
by auto
thus "1 *⇩C x = x"
for x :: "'a ⇒⇩L 'b"

have ‹onorm (λx. a *⇩C f x) = cmod a * onorm f›
if ‹bounded_linear f›
for f :: ‹'a ⇒ 'b› and a :: complex
proof-
have ‹cmod a ≥ 0›
by simp
have ‹∃ K::real. ∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
using ‹bounded_linear f› le_onorm by fastforce
then obtain K::real where ‹∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
by blast
hence  ‹∀ x. (cmod a) *(¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ (cmod a) * K›
using ‹cmod a ≥ 0›
by (metis abs_ereal.simps(1) abs_ereal_pos   abs_pos ereal_mult_left_mono  times_ereal.simps(1))
hence  ‹∀ x.  (¦ ereal ((cmod a) * (norm (f x)) / (norm x)) ¦) ≤ (cmod a) * K›
by simp
hence ‹bdd_above {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}›
by simp
moreover have ‹{ereal (cmod a * (norm (f x)) / (norm x)) | x. True} ≠ {}›
by auto
ultimately have p1: ‹(SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦) ≤ cmod a * K›
using ‹∀ x. ¦ ereal (cmod a * (norm (f x)) / (norm x)) ¦ ≤ cmod a * K›
Sup_least mem_Collect_eq
have  p2: ‹⋀i. i ∈ UNIV ⟹ 0 ≤ ereal (cmod a * norm (f i) / norm i)›
by simp
hence ‹¦SUP x. ereal (cmod a * (norm (f x)) / (norm x))¦
≤ (SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦)›
using  ‹bdd_above {ereal (cmod a * (norm (f x)) / (norm x)) | x. True}›
‹{ereal (cmod a * (norm (f x)) / (norm x)) | x. True} ≠ {}›
by (metis (mono_tags, lifting) SUP_upper2 Sup.SUP_cong UNIV_I
p2 abs_ereal_ge0 ereal_le_real)
hence ‹¦SUP x. ereal (cmod a * (norm (f x)) / (norm x))¦ ≤ cmod a * K›
using  ‹(SUP x. ¦ereal (cmod a * (norm (f x)) / (norm x))¦) ≤ cmod a * K›
by simp
hence ‹¦ ( SUP i∈UNIV::'a set. ereal ((λ x. (cmod a) * (norm (f x)) / norm x) i)) ¦ ≠ ∞›
by auto
hence w2: ‹( SUP i∈UNIV::'a set. ereal ((λ x. cmod a * (norm (f x)) / norm x) i))
= ereal ( Sup ((λ x. cmod a * (norm (f x)) / norm x) ` (UNIV::'a set) ))›
have ‹(UNIV::('a set)) ≠ {}›
by simp
moreover have ‹⋀ i. i ∈ (UNIV::('a set)) ⟹ (λ x. (norm (f x)) / norm x :: ereal) i ≥ 0›
by simp
moreover have ‹cmod a ≥ 0›
by simp
ultimately have ‹(SUP i∈(UNIV::('a set)). ((cmod a)::ereal) * (λ x. (norm (f x)) / norm x :: ereal) i )
= ((cmod a)::ereal) * ( SUP i∈(UNIV::('a set)). (λ x. (norm (f x)) / norm x :: ereal) i )›
hence ‹(SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) )
= ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) )›
by simp
hence z1: ‹real_of_ereal ( (SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) ) )
= real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )›
by simp
have z2: ‹real_of_ereal (SUP x. ((cmod a)::ereal) * ( (norm (f x)) / norm x :: ereal) )
= (SUP x. cmod a * (norm (f x) / norm x))›
using w2
by auto
have ‹real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )
=  (cmod a) * real_of_ereal ( SUP x. ( (norm (f x)) / norm x :: ereal) )›
by simp
moreover have ‹real_of_ereal ( SUP x. ( (norm (f x)) / norm x :: ereal) )
= ( SUP x. ((norm (f x)) / norm x) )›
proof-
have ‹¦ ( SUP i∈UNIV::'a set. ereal ((λ x. (norm (f x)) / norm x) i)) ¦ ≠ ∞›
proof-
have ‹∃ K::real. ∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
using ‹bounded_linear f› le_onorm by fastforce
then obtain K::real where ‹∀ x. (¦ ereal ((norm (f x)) / (norm x)) ¦) ≤ K›
by blast
hence ‹bdd_above {ereal ((norm (f x)) / (norm x)) | x. True}›
by simp
moreover have ‹{ereal ((norm (f x)) / (norm x)) | x. True} ≠ {}›
by auto
ultimately have ‹(SUP x. ¦ereal ((norm (f x)) / (norm x))¦) ≤ K›
using ‹∀ x. ¦ ereal ((norm (f x)) / (norm x)) ¦ ≤ K›
Sup_least mem_Collect_eq
hence ‹¦SUP x. ereal ((norm (f x)) / (norm x))¦
≤ (SUP x. ¦ereal ((norm (f x)) / (norm x))¦)›
using  ‹bdd_above {ereal ((norm (f x)) / (norm x)) | x. True}›
‹{ereal ((norm (f x)) / (norm x)) | x. True} ≠ {}›
by (metis (mono_tags, lifting) SUP_upper2 Sup.SUP_cong UNIV_I ‹⋀i. i ∈ UNIV ⟹ 0 ≤ ereal (norm (f i) / norm i)› abs_ereal_ge0 ereal_le_real)
hence ‹¦SUP x. ereal ((norm (f x)) / (norm x))¦ ≤ K›
using  ‹(SUP x. ¦ereal ((norm (f x)) / (norm x))¦) ≤ K›
by simp
thus ?thesis
by auto
qed
hence ‹ ( SUP i∈UNIV::'a set. ereal ((λ x. (norm (f x)) / norm x) i))
= ereal ( Sup ((λ x. (norm (f x)) / norm x) ` (UNIV::'a set) ))›
thus ?thesis
by simp
qed
have z3: ‹real_of_ereal ( ((cmod a)::ereal) * ( SUP x. ( (norm (f x)) / norm x :: ereal) ) )
= cmod a * (SUP x. norm (f x) / norm x)›
by (simp add: ‹real_of_ereal (SUP x. ereal (norm (f x) / norm x)) = (SUP x. norm (f x) / norm x)›)
hence w1: ‹(SUP x. cmod a * (norm (f x) / norm x)) =
cmod a * (SUP x. norm (f x) / norm x)›
using z1 z2 by linarith
have v1: ‹onorm (λx. a *⇩C f x) = (SUP x. norm (a *⇩C f x) / norm x)›
have v2: ‹(SUP x. norm (a *⇩C f x) / norm x) = (SUP x. ((cmod a) * norm (f x)) / norm x)›
by simp
have v3: ‹(SUP x. ((cmod a) * norm (f x)) / norm x) =  (SUP x. (cmod a) * ((norm (f x)) / norm x))›
by simp
have v4: ‹(SUP x. (cmod a) * ((norm (f x)) / norm x)) = (cmod a) *  (SUP x. ((norm (f x)) / norm x))›
using w1
by blast
show ‹onorm (λx. a *⇩C f x) = cmod a * onorm f›
using v1 v2 v3 v4
by (metis (mono_tags, lifting) onorm_def)
qed
thus ‹norm (a *⇩C x) = cmod a * norm x›
for a::complex and x::‹('a, 'b) blinfun›
by transfer blast
qed
end

(* We do not have clinear_blinfun_compose_right *)
lemma clinear_blinfun_compose_left: ‹clinear (λx. blinfun_compose x y)›
by (auto intro!: clinearI simp: blinfun_eqI scaleC_blinfun.rep_eq bounded_bilinear.add_left
bounded_bilinear_blinfun_compose)

instance blinfun :: (real_normed_vector, cbanach) cbanach..

lemma blinfun_compose_assoc: "(A o⇩L B) o⇩L C = A o⇩L (B  o⇩L C)"

lift_definition blinfun_of_cblinfun::‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector
⇒ 'a ⇒⇩L 'b› is "id"

lift_definition blinfun_cblinfun_eq ::
‹'a ⇒⇩L 'b ⇒ 'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector ⇒ bool› is "(=)" .

lemma blinfun_cblinfun_eq_bi_unique[transfer_rule]: ‹bi_unique blinfun_cblinfun_eq›
unfolding bi_unique_def by transfer auto

lemma blinfun_cblinfun_eq_right_total[transfer_rule]: ‹right_total blinfun_cblinfun_eq›
unfolding right_total_def by transfer (simp add: bounded_clinear.bounded_linear)

named_theorems cblinfun_blinfun_transfer

lemma cblinfun_blinfun_transfer_0[cblinfun_blinfun_transfer]:
"blinfun_cblinfun_eq (0::(_,_) blinfun) (0::(_,_) cblinfun)"
by transfer simp

lemma cblinfun_blinfun_transfer_plus[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (+) (+)"
unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_minus[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (-) (-)"
unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_uminus[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (uminus) (uminus)"
unfolding rel_fun_def by transfer auto

definition "real_complex_eq r c ⟷ complex_of_real r = c"

lemma bi_unique_real_complex_eq[transfer_rule]: ‹bi_unique real_complex_eq›
unfolding real_complex_eq_def bi_unique_def by auto

lemma left_total_real_complex_eq[transfer_rule]: ‹left_total real_complex_eq›
unfolding real_complex_eq_def left_total_def by auto

lemma cblinfun_blinfun_transfer_scaleC[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(real_complex_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (scaleR) (scaleC)"
unfolding rel_fun_def by transfer (simp add: real_complex_eq_def scaleR_scaleC)

lemma cblinfun_blinfun_transfer_CBlinfun[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(eq_onp bounded_clinear ===> blinfun_cblinfun_eq) Blinfun CBlinfun"
unfolding rel_fun_def blinfun_cblinfun_eq.rep_eq eq_onp_def
by (auto simp: CBlinfun_inverse Blinfun_inverse bounded_clinear.bounded_linear)

lemma cblinfun_blinfun_transfer_norm[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> (=)) norm norm"
unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_dist[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> (=)) dist dist"
unfolding rel_fun_def dist_norm by transfer auto

lemma cblinfun_blinfun_transfer_sgn[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) sgn sgn"
unfolding rel_fun_def sgn_blinfun_def sgn_cblinfun_def by transfer (auto simp: scaleR_scaleC)

lemma cblinfun_blinfun_transfer_Cauchy[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(((=) ===> blinfun_cblinfun_eq) ===> (=)) Cauchy Cauchy"
proof -
note cblinfun_blinfun_transfer[transfer_rule]
show ?thesis
unfolding Cauchy_def
by transfer_prover
qed

lemma cblinfun_blinfun_transfer_tendsto[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) tendsto tendsto"
proof -
note cblinfun_blinfun_transfer[transfer_rule]
show ?thesis
unfolding tendsto_iff
by transfer_prover
qed

lemma cblinfun_blinfun_transfer_compose[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (o⇩L) (o⇩C⇩L)"
unfolding rel_fun_def by transfer auto

lemma cblinfun_blinfun_transfer_apply[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> (=) ===> (=)) blinfun_apply cblinfun_apply"
unfolding rel_fun_def by transfer auto

lemma blinfun_of_cblinfun_inj:
‹blinfun_of_cblinfun f = blinfun_of_cblinfun g ⟹ f = g›
by (metis cblinfun_apply_inject blinfun_of_cblinfun.rep_eq)

lemma blinfun_of_cblinfun_inv:
assumes "⋀c. ⋀x. f *⇩v (c *⇩C x) = c *⇩C (f *⇩v x)"
shows "∃g. blinfun_of_cblinfun g = f"
using assms
proof transfer
show "∃g∈Collect bounded_clinear. id g = f"
if "bounded_linear f"
and "⋀c x. f (c *⇩C x) = c *⇩C f x"
for f :: "'a ⇒ 'b"
using that bounded_linear_bounded_clinear by auto
qed

lemma blinfun_of_cblinfun_zero:
‹blinfun_of_cblinfun 0 = 0›
by transfer simp

lemma blinfun_of_cblinfun_uminus:
‹blinfun_of_cblinfun (- f) = - (blinfun_of_cblinfun f)›
by transfer auto

lemma blinfun_of_cblinfun_minus:
‹blinfun_of_cblinfun (f - g) = blinfun_of_cblinfun f - blinfun_of_cblinfun g›
by transfer auto

lemma blinfun_of_cblinfun_scaleC:
‹blinfun_of_cblinfun (c *⇩C f) = c *⇩C (blinfun_of_cblinfun f)›
by transfer auto

lemma blinfun_of_cblinfun_scaleR:
‹blinfun_of_cblinfun (c *⇩R f) = c *⇩R (blinfun_of_cblinfun f)›
by transfer auto

lemma blinfun_of_cblinfun_norm:
fixes f::‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector›
shows ‹norm f = norm (blinfun_of_cblinfun f)›
by transfer auto

lemma blinfun_of_cblinfun_cblinfun_compose:
fixes f::‹'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector›
and g::‹'a::complex_normed_vector ⇒⇩C⇩L 'b›
shows ‹blinfun_of_cblinfun (f  o⇩C⇩L g) = (blinfun_of_cblinfun f) o⇩L (blinfun_of_cblinfun g)›
by transfer auto

subsection ‹Composition›

lemma cblinfun_compose_assoc:
shows "(A o⇩C⇩L B) o⇩C⇩L C = A o⇩C⇩L (B o⇩C⇩L C)"
by (metis (no_types, lifting) cblinfun_apply_inject fun.map_comp cblinfun_compose.rep_eq)

lemma cblinfun_compose_zero_right[simp]: "U o⇩C⇩L 0 = 0"
using bounded_cbilinear.zero_right bounded_cbilinear_cblinfun_compose by blast

lemma cblinfun_compose_zero_left[simp]: "0 o⇩C⇩L U = 0"
using bounded_cbilinear.zero_left bounded_cbilinear_cblinfun_compose by blast

lemma cblinfun_compose_scaleC_left[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹(a *⇩C A) o⇩C⇩L B = a *⇩C (A o⇩C⇩L B)›

lemma cblinfun_compose_scaleR_left[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹(a *⇩R A) o⇩C⇩L B = a *⇩R (A o⇩C⇩L B)›

lemma cblinfun_compose_scaleC_right[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹A o⇩C⇩L (a *⇩C B) = a *⇩C (A o⇩C⇩L B)›
by transfer (auto intro!: ext bounded_clinear.clinear complex_vector.linear_scale)

lemma cblinfun_compose_scaleR_right[simp]:
fixes A::"'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector"
and B::"'a::complex_normed_vector ⇒⇩C⇩L 'b"
shows ‹A o⇩C⇩L (a *⇩R B) = a *⇩R (A o⇩C⇩L B)›

lemma cblinfun_compose_id_right[simp]:
shows "U o⇩C⇩L id_cblinfun = U"
by transfer auto

lemma cblinfun_compose_id_left[simp]:
shows "id_cblinfun o⇩C⇩L U  = U"
by transfer auto

lemma cblinfun_compose_add_left: ‹(a + b) o⇩C⇩L c = (a o⇩C⇩L c) + (b o⇩C⇩L c)›

lemma cblinfun_compose_add_right: ‹a o⇩C⇩L (b + c) = (a o⇩C⇩L b) + (a o⇩C⇩L c)›

lemma cbilinear_cblinfun_compose[simp]: "cbilinear cblinfun_compose"

lemma cblinfun_compose_sum_left: ‹(∑i∈S. g i) o⇩C⇩L x = (∑i∈S. g i o⇩C⇩L x)›
by (induction S rule:infinite_finite_induct) (auto simp: cblinfun_compose_add_left)

lemma cblinfun_compose_sum_right: ‹x o⇩C⇩L (∑i∈S. g i) = (∑i∈S. x o⇩C⇩L g i)›
by (induction S rule:infinite_finite_induct) (auto simp: cblinfun_compose_add_right)

lemma cblinfun_compose_minus_right: ‹a o⇩C⇩L (b - c) = (a o⇩C⇩L b) - (a o⇩C⇩L c)›
lemma cblinfun_compose_minus_left: ‹(a - b) o⇩C⇩L c = (a o⇩C⇩L c) - (b o⇩C⇩L c)›

lemma simp_a_oCL_b: ‹a o⇩C⇩L b = c ⟹ a o⇩C⇩L (b o⇩C⇩L d) = c o⇩C⇩L d›
― ‹A convenience lemma to transform simplification rules of the form \<^term>‹a o⇩C⇩L b = c›.
E.g., ‹simp_a_oCL_b[OF isometryD, simp]› declares a simp-rule for simplifying \<^term>‹adj x o⇩C⇩L (x o⇩C⇩L y) = id_cblinfun o⇩C⇩L y›.›
by (auto simp: cblinfun_compose_assoc)

lemma simp_a_oCL_b': ‹a o⇩C⇩L b = c ⟹ a *⇩V (b *⇩V d) = c *⇩V d›
― ‹A convenience lemma to transform simplification rules of the form \<^term>‹a o⇩C⇩L b = c›.
E.g., ‹simp_a_oCL_b'[OF isometryD, simp]› declares a simp-rule for simplifying \<^term>‹adj x *⇩V x *⇩V y = id_cblinfun *⇩V y›.›
by auto

lemma cblinfun_compose_uminus_left: ‹(- a) o⇩C⇩L b = - (a o⇩C⇩L b)›

lemma cblinfun_compose_uminus_right: ‹a o⇩C⇩L (- b) = - (a o⇩C⇩L b)›

lemma bounded_clinear_cblinfun_compose_left: ‹bounded_clinear (λx. x o⇩C⇩L y)›
lemma bounded_clinear_cblinfun_compose_right: ‹bounded_clinear (λy. x o⇩C⇩L y)›
lemma clinear_cblinfun_compose_left: ‹clinear (λx. x o⇩C⇩L y)›
by (simp add: bounded_cbilinear.bounded_clinear_left bounded_cbilinear_cblinfun_compose bounded_clinear.clinear)
lemma clinear_cblinfun_compose_right: ‹clinear (λy. x o⇩C⇩L y)›

lemma isCont_cblinfun_compose_left: ‹isCont (λx. x o⇩C⇩L a) y›
apply (rule clinear_continuous_at)
by (rule bounded_clinear_cblinfun_compose_left)
lemma isCont_cblinfun_compose_right: ‹isCont (λx. a o⇩C⇩L x) y›
apply (rule clinear_continuous_at)
by (rule bounded_clinear_cblinfun_compose_right)

lemma cspan_compose_closed:
assumes ‹⋀a b. a ∈ A ⟹ b ∈ A ⟹ a o⇩C⇩L b ∈ A›
assumes ‹a ∈ cspan A› and ‹b ∈ cspan A›
shows ‹a o⇩C⇩L b ∈ cspan A›
proof -
from ‹a ∈ cspan A›
obtain F f where ‹finite F› and ‹F ⊆ A› and a_def: ‹a = (∑x∈F. f x *⇩C x)›
by (smt (verit, del_insts) complex_vector.span_explicit mem_Collect_eq)
from ‹b ∈ cspan A›
obtain G g where ‹finite G› and ‹G ⊆ A› and b_def: ‹b = (∑x∈G. g x *⇩C x)›
by (smt (verit, del_insts) complex_vector.span_explicit mem_Collect_eq)
have ‹a o⇩C⇩L b = (∑(x,y)∈F×G. (f x *⇩C x) o⇩C⇩L (g y *⇩C y))›
apply (simp add: a_def b_def cblinfun_compose_sum_left)
by (auto intro!: sum.cong simp add: cblinfun_compose_sum_right scaleC_sum_right sum.cartesian_product case_prod_beta)
also have ‹… = (∑(x,y)∈F×G. (f x * g y) *⇩C (x o⇩C⇩L y))›
by (metis (no_types, opaque_lifting) cblinfun_compose_scaleC_left cblinfun_compose_scaleC_right scaleC_scaleC)
also have ‹… ∈ cspan A›
using assms ‹G ⊆ A› ‹F ⊆ A›
apply (auto intro!: complex_vector.span_sum complex_vector.span_scale
simp: complex_vector.span_clauses)
using complex_vector.span_clauses(1) by blast
finally show ?thesis
by -
qed

lift_definition
adj :: "'a::chilbert_space ⇒⇩C⇩L 'b::complex_inner ⇒ 'b ⇒⇩C⇩L 'a" ("_*" [99] 100)

definition selfadjoint :: ‹('a::chilbert_space ⇒⇩C⇩L 'a) ⇒ bool› where
‹selfadjoint a ⟷ a* = a›

apply transfer using double_cadjoint by blast

fixes B::‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
and A::‹'b ⇒⇩C⇩L 'c::complex_inner›
shows "(A o⇩C⇩L B)* =  (B*) o⇩C⇩L (A*)"
proof transfer
fix  A :: ‹'b ⇒ 'c› and B :: ‹'a ⇒ 'b›
assume ‹bounded_clinear A› and ‹bounded_clinear B›
hence ‹bounded_clinear (A ∘ B)›
have ‹((A ∘ B) u ∙⇩C v) = (u ∙⇩C (B⇧† ∘ A⇧†) v)›
for u v
by (metis (no_types, lifting) cadjoint_univ_prop ‹bounded_clinear A› ‹bounded_clinear B› cinner_commute' comp_def)
thus ‹(A ∘ B)⇧† = B⇧† ∘ A⇧†›
using ‹bounded_clinear (A ∘ B)›
qed

lemma scaleC_adj[simp]: "(a *⇩C A)* = (cnj a) *⇩C (A*)"

lemma scaleR_adj[simp]: "(a *⇩R A)* = a *⇩R (A*)"

lemma adj_plus: ‹(A + B)* = (A*) + (B*)›
proof transfer
fix A B::‹'b ⇒ 'a›
assume a1: ‹bounded_clinear A› and a2: ‹bounded_clinear B›
define F where ‹F = (λx. (A⇧†) x + (B⇧†) x)›
define G where ‹G = (λx. A x + B x)›
have ‹bounded_clinear G›
unfolding G_def
moreover have ‹(F u ∙⇩C v) = (u ∙⇩C G v)› for u v
unfolding F_def G_def
ultimately have ‹F = G⇧† ›
thus ‹(λx. A x + B x)⇧† = (λx. (A⇧†) x + (B⇧†) x)›
unfolding F_def G_def
by auto
qed

fixes G :: "'b::chilbert_space ⇒⇩C⇩L 'a::complex_inner"
shows ‹(G* *⇩V x) ∙⇩C y = x ∙⇩C (G *⇩V y)›
apply transfer using cadjoint_univ_prop by blast

fixes G :: "'b::chilbert_space ⇒⇩C⇩L 'a::complex_inner"
shows ‹x ∙⇩C (G* *⇩V y) = (G *⇩V x) ∙⇩C y›
apply transfer using cadjoint_univ_prop' by blast