# 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
Complex_Inner_Product One_Dimensional_Spaces
Banach_Steinhaus.Banach_Steinhaus
"HOL-Types_To_Sets.Types_To_Sets"
Complex_Bounded_Linear_Function0
begin

unbundle lattice_syntax

subsection ‹Misc basic facts and declarations›

notation cblinfun_apply (infixr "*⇩V" 70)

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

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

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 ‹⋀ψ. cinner ψ (A *⇩V ψ) = cinner ψ (B *⇩V ψ)›
shows ‹A = B›
proof -
define C where ‹C = A - B›
have C0[simp]: ‹cinner ψ (C ψ) = 0› for ψ
by (simp add: C_def 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 apply transfer
by (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›
apply (rule complex_vector.linear_eq_0_on_span[where f=F])
using bounded_clinear.axioms(1) cblinfun_apply assms by auto

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›
apply (rule complex_vector.linear_eq_on_span[where f=F])
using bounded_clinear.axioms(1) cblinfun_apply assms by auto

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›
proof-
have "F - G = 0"
apply (rule cblinfun_eq_0_on_UNIV_span[where basis=basis])
using assms by (auto simp add: cblinfun.diff_left)
thus ?thesis by simp
qed

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"
apply (rule cblinfun_eq_on_UNIV_span[where basis=basis])
using assms is_generator_set is_cindependent_set by auto

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 ⟹ ⟨v, F *⇩V u⟩ = 0"
shows "F = 0"
proof-
have "F *⇩V u = 0"
if "u∈basisA" for u
proof-
have "⋀v. v∈basisB ⟹ ⟨v, F *⇩V u⟩ = 0"
moreover have "(⋀v. v∈basisB ⟹ ⟨v, x⟩ = 0) ⟹ x = 0"
for x
proof-
assume r1: "⋀v. v∈basisB ⟹ ⟨v, x⟩ = 0"
have "⟨v, x⟩ = 0" 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, x⟩ = ⟨(∑a∈t. s a *⇩C a), x⟩"
also have "… = (∑a∈t. ⟨s a *⇩C a, x⟩)"
using cinner_sum_left by blast
also have "… = (∑a∈t. cnj (s a) * ⟨a, 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, 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, F *⇩V u⟩ = ⟨v, G *⇩V u⟩"
shows "F = G"
proof-
define H where "H = F - G"
have "⋀u v. u∈basisA ⟹ v∈basisB ⟹ ⟨v, H *⇩V u⟩ = 0"
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, v⟩ = ⟨G *⇩V u, v⟩"
shows "F = G"
using cinner_canonical_basis_eq assms
by (metis cinner_commute')

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
apply auto
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_to_CARD_1_0[simp]: ‹(A :: _ ⇒⇩C⇩L _::CARD_1) = 0›
apply (rule cblinfun_eqI)
by auto

lemma cblinfun_from_CARD_1_0[simp]: ‹(A :: _::CARD_1 ⇒⇩C⇩L _) = 0›
apply (rule cblinfun_eqI)
apply (subst CARD_1_vec_0)
by auto

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 apply atomize_elim by 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, ccfv_threshold) complex_vector.span_base complex_vector.span_scale complex_vector.span_sum mem_Collect_eq subset_eq)
moreover have ‹G *⇩V a' = (if a'=a then b else 0)› if ‹a'∈basisA'› for a'
apply (cases ‹a'=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› apply (rule cblinfun_eq_on_UNIV_span)
apply (auto simp: H'_def cblinfun.sum_left)
apply (subst sum_single)
by (auto simp: 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})›
using F_basis
by (smt (z3) UN_subset_iff complex_vector.span_alt complex_vector.span_minimal complex_vector.subspace_span mem_Collect_eq subset_iff)

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 ‹cspan basis = UNIV›
apply (rule cblinfun_cspan_UNIV[where basisA=basisA and basisB=basisB])
apply (auto simp: basis_def)
by (metis F_apply f_a f_not_a)

moreover have ‹finite basis›
unfolding basis_def apply (rule finite_image_set2) by auto

ultimately show ‹∃S :: ('a ⇒⇩C⇩L 'b) set. finite S ∧ cspan S = UNIV›
by auto
qed

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
apply transfer
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"
apply transfer

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

show "a *⇩C b *⇩C x = (a * b) *⇩C x"
for a b :: complex and x :: "'a ⇒⇩L 'b"
apply transfer
by 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›
apply transfer
by 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)

instantiation blinfun :: (real_normed_vector, cbanach) "cbanach"
begin
instance..
end

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"
apply transfer by (simp add: bounded_clinear.bounded_linear)

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 apply transfer by auto

lemma blinfun_cblinfun_eq_right_total[transfer_rule]: ‹right_total blinfun_cblinfun_eq›
unfolding right_total_def apply transfer

named_theorems cblinfun_blinfun_transfer

lemma cblinfun_blinfun_transfer_0[cblinfun_blinfun_transfer]:
"blinfun_cblinfun_eq (0::(_,_) blinfun) (0::(_,_) cblinfun)"
apply transfer by 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 apply transfer by 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 apply transfer by 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 apply transfer by 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 apply transfer

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 apply transfer by 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 apply transfer by 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 apply transfer
by (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 apply transfer by auto

lemma cblinfun_blinfun_transfer_apply[cblinfun_blinfun_transfer]:
includes lifting_syntax
shows "(blinfun_cblinfun_eq ===> (=) ===> (=)) blinfun_apply cblinfun_apply"
unfolding rel_fun_def apply transfer by 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›
apply transfer by simp

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

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

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

lemma blinfun_of_cblinfun_scaleR:
‹blinfun_of_cblinfun (c *⇩R f) = c *⇩R (blinfun_of_cblinfun f)›
apply transfer by 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)›
apply transfer by auto

subsection ‹Composition›

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)›
apply transfer by auto

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)›
apply transfer by (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"
apply transfer by auto

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

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 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"
apply (rule cblinfun_eqI)
apply (rule cblinfun_eq_on[where G=G])
using assms apply auto
by (metis ccspan.rep_eq iso_tuple_UNIV_I top_ccsubspace.rep_eq)

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"

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

by (metis eq_id_iff)

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, v ⟩ = ⟨ u, (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*)"
apply transfer

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,  v⟩ = ⟨u, 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

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)

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

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

lemma norm_adj[simp]: ‹norm (A*) = norm A›
for A :: ‹'b::chilbert_space ⇒⇩C⇩L 'c::complex_inner›
proof (cases ‹(∃x y :: 'b. x ≠ y) ∧ (∃x y :: 'c. x ≠ y)›)
case True
then have c1: ‹class.not_singleton TYPE('b)›
apply intro_classes by simp
from True have c2: ‹class.not_singleton TYPE('c)›
apply intro_classes by simp
have normA: ‹norm A = (SUP (ψ, φ). cmod (ψ ∙⇩C (A *⇩V φ)) / (norm ψ * norm φ))›
apply (rule cinner_sup_norm_cblinfun[internalize_sort ‹'a::{complex_normed_vector,not_singleton}›])
apply (rule complex_normed_vector_axioms)
by (rule c1)
have normAadj: ‹norm (A*) = (SUP (ψ, φ). cmod (ψ ∙⇩C (A* *⇩V φ)) / (norm ψ * norm φ))›
apply (rule cinner_sup_norm_cblinfun[internalize_sort ‹'a::{complex_normed_vector,not_singleton}›])
apply (rule complex_normed_vector_axioms)
by (rule c2)

have ‹norm (A*) = (SUP (ψ, φ). cmod (φ ∙⇩C (A *⇩V ψ)) / (norm ψ * norm φ))›
apply (subst cinner_commute)
apply (subst complex_mod_cnj)
by rule
also have ‹… = Sup ((λ(ψ, φ). cmod (φ ∙⇩C (A *⇩V ψ)) / (norm ψ * norm φ)) ` prod.swap ` UNIV)›
by auto
also have ‹… = (SUP (φ, ψ). cmod (φ ∙⇩C (A *⇩V ψ)) / (norm ψ * norm φ))›
apply (subst image_image)
by auto
also have ‹… = norm A›
unfolding normA
finally show ?thesis
by -
next
case False
then consider (b) ‹⋀x::'b. x = 0› | (c) ‹⋀x::'c. x = 0›
by auto
then have ‹A = 0›
apply (cases; transfer)
apply (metis (full_types) bounded_clinear_def complex_vector.linear_0)
by auto
then show ‹norm (A*) = norm A›
by simp
qed

by (auto intro!: antilinearI exI[of _ 1] simp: bounded_antilinear_def bounded_antilinear_axioms_def adj_plus)

fixes G:: ‹'b::chilbert_space ⇒⇩C⇩L 'a::chilbert_space›
and F:: ‹'a ⇒⇩C⇩L 'b›
assumes ‹⋀x y. ⟨(cblinfun_apply F) x, y⟩ = ⟨x, (cblinfun_apply G) y⟩›
shows ‹F = G*›
using assms apply transfer using cadjoint_eqI by auto

lemma cinner_real_hermiteanI:
― ‹Prop. II.2.12 in @{cite conway2013course}›
assumes ‹⋀ψ. cinner ψ (A *⇩V ψ) ∈ ℝ›
shows ‹A = A*›
proof -
{ fix g h :: 'a
{
fix α :: complex
have ‹cinner h (A h) + cnj α *⇩C cinner g (A h) + α *⇩C cinner h (A g) + (abs α)⇧2 * cinner g (A g)
= cinner (h + α *⇩C g) (A *⇩V (h + α *⇩C g))› (is ‹?sum4 = _›)
by (metis cnj_x_x mult.commute)
also have ‹… ∈ ℝ›
using assms by auto
finally have ‹?sum4 = cnj ?sum4›
using Reals_cnj_iff by fastforce
then have ‹cnj α *⇩C cinner g (A h) + α *⇩C cinner h (A g)
= α *⇩C cinner (A h) g + cnj α *⇩C cinner (A g) h›
using Reals_cnj_iff abs_complex_real assms by force
also have ‹… = α *⇩C cinner h (A* *⇩V g) + cnj α *⇩C cinner g (A* *⇩V h)›
finally have ‹cnj α *⇩C cinner g (A h) + α *⇩C cinner h (A g) = α *⇩C cinner h (A* *⇩V g) + cnj α *⇩C cinner g (A* *⇩V h)›
by -
}
from this[where α2=1] this[where α2=𝗂]
have 1: ‹cinner g (A h) + cinner h (A g) = cinner h (A* *⇩V g) + cinner g (A* *⇩V h)›
and i: ‹- 𝗂 * cinner g (A h) + 𝗂 *⇩C cinner h (A g) =  𝗂 *⇩C cinner h (A* *⇩V g) - 𝗂 *⇩C cinner g (A* *⇩V h)›
by auto
from arg_cong2[OF 1 arg_cong[OF i, where f=‹(*) (-𝗂)›], where f=plus]
have ‹cinner h (A g) = cinner h (A* *⇩V g)›
by (auto simp: ring_class.ring_distribs)
}
then show "A = A*"
qed

lemma norm_AAadj[simp]: ‹norm (A o⇩C⇩L A*) = (norm A)⇧2› for A :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::{complex_inner}›
proof (cases ‹class.not_singleton TYPE('b)›)
case True
then have [simp]: ‹class.not_singleton TYPE('b)›
by -
have 1: ‹(norm A)⇧2 * ε ≤ norm (A o⇩C⇩L A*)› if ‹ε < 1› and ‹ε ≥ 0› for ε
proof -
obtain ψ where ψ: ‹norm ((A*) *⇩V ψ) ≥ norm (A*) * sqrt ε› and [simp]: ‹norm ψ = 1›
apply atomize_elim
apply (rule cblinfun_norm_approx_witness_mult[internalize_sort' 'a])
using ‹ε < 1› by (auto intro: complex_normed_vector_class.complex_normed_vector_axioms)
have ‹complex_of_real ((norm A)⇧2 * ε) = (norm (A*) * sqrt ε)⇧2›
also have ‹… ≤ (norm ((A* *⇩V ψ)))⇧2›
apply (rule complex_of_real_mono)
using ψ apply (rule power_mono)
using ‹ε ≥ 0› by auto
also have ‹… ≤ cinner (A* *⇩V ψ) (A* *⇩V ψ)›
by (auto simp flip: power2_norm_eq_cinner)
also have ‹… = cinner ψ (A *⇩V A* *⇩V ψ)›
also have ‹… = cinner ψ ((A o⇩C⇩L A*) *⇩V ψ)›
by auto
also have ‹… ≤ norm (A o⇩C⇩L A*)›
using ‹norm ψ = 1›
by (smt (verit, best) Im_complex_of_real Re_complex_of_real ‹(A* *⇩V ψ) ∙⇩C (A* *⇩V ψ) = ψ ∙⇩C (A *⇩V A* *⇩V ψ)› ‹ψ ∙⇩C (A *⇩V A* *⇩V ψ) = ψ ∙⇩C ((A o⇩C⇩L A*) *⇩V ψ)› cdot_square_norm cinner_ge_zero cmod_Re complex_inner_class.Cauchy_Schwarz_ineq2 less_eq_complex_def mult_cancel_left1 mult_cancel_right1 norm_cblinfun)
finally show ?thesis
by (auto simp: less_eq_complex_def)
qed
then have 1: ‹(norm A)⇧2 ≤ norm (A o⇩C⇩L A*)›
by (metis field_le_mult_one_interval less_eq_real_def ordered_field_class.sign_simps(5))

have 2: ‹norm (A o⇩C⇩L A*) ≤ (norm A)⇧2›
proof (rule norm_cblinfun_bound)
show ‹0 ≤ (norm A)⇧2› by simp
fix ψ
have ‹norm ((A o⇩C⇩L A*) *⇩V ψ) = norm (A *⇩V A* *⇩V ψ)›
by auto
also have ‹… ≤ norm A * norm (A* *⇩V ψ)›
also have ‹… ≤ norm A * norm (A*) * norm ψ›
by (metis mult.assoc norm_cblinfun norm_imp_pos_and_ge ordered_comm_semiring_class.comm_mult_left_mono)
also have ‹… = (norm A)⇧2 * norm ψ›
finally show ‹norm ((A o⇩C⇩L A*) *⇩V ψ) ≤ (norm A)⇧2 * norm ψ›
by -
qed

from 1 2 show ?thesis by simp
next
case False
then have [simp]: ‹class.CARD_1 TYPE('b)›
by (rule not_singleton_vs_CARD_1)
have ‹A = 0›
apply (rule cblinfun_to_CARD_1_0[internalize_sort' 'b])
by (auto intro: complex_normed_vector_class.complex_normed_vector_axioms)
then show ?thesis
by auto
qed

subsection ‹Unitaries / isometries›

definition isometry::‹'a::chilbert_space ⇒⇩C⇩L 'b::complex_inner ⇒ bool› where
‹isometry U ⟷ U* o⇩C⇩L U = id_cblinfun›

definition unitary::‹'a::chilbert_space ⇒⇩C⇩L 'b::complex_inner ⇒ bool› where
‹unitary U ⟷ (U* o⇩C⇩L U  = id_cblinfun) ∧ (U o⇩C⇩L U* = id_cblinfun)›

lemma unitary_twosided_isometry: "unitary U ⟷ isometry U ∧ isometry (U*)"
unfolding unitary_def isometry_def by simp

lemma isometryD[simp]: "isometry U ⟹ U* o⇩C⇩L U = id_cblinfun"
unfolding isometry_def by simp

(* Not [simp] because isometryD[simp] + unitary_isometry[simp] already have the same effect *)
lemma unitaryD1: "unitary U ⟹ U* o⇩C⇩L U = id_cblinfun"
unfolding unitary_def by simp

lemma unitaryD2[simp]: "unitary U ⟹ U o⇩C⇩L U* = id_cblinfun"
unfolding unitary_def by simp

lemma unitary_isometry[simp]: "unitary U ⟹ isometry U"
unfolding unitary_def isometry_def by simp

lemma unitary_adj[simp]: "unitary (U*) = unitary U"
unfolding unitary_def by auto

lemma isometry_cblinfun_compose[simp]:
assumes "isometry A" and "isometry B"
shows "isometry (A o⇩C⇩L B)"
proof-
have "B* o⇩C⇩L A* o⇩C⇩L (A o⇩C⇩L B) = id_cblinfun" if "A* o⇩C⇩L A = id_cblinfun" and "B* o⇩C⇩L B = id_cblinfun"
using that
by (smt (verit, del_insts) adjoint_eqI cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply)
thus ?thesis
using assms unfolding isometry_def by simp
qed

lemma unitary_cblinfun_compose[simp]: "unitary (A o⇩C⇩L B)"
if "unitary A" and "unitary B"
using that

lemma unitary_surj:
assumes "unitary U"
shows "surj (cblinfun_apply U)"
apply (rule surjI[where f=‹cblinfun_apply (U*)›])
using assms unfolding unitary_def apply transfer
using comp_eq_dest_lhs by force

lemma unitary_id[simp]: "unitary id_cblinfun"

lemma orthogonal_on_basis_is_isometry:
assumes spanB: ‹ccspan B = ⊤›
assumes orthoU: ‹⋀b c. b∈B ⟹ c∈B ⟹ cinner (U *⇩V b) (U *⇩V c) = cinner b c›
shows ‹isometry U›
proof -
have [simp]: ‹b ∈ closure (cspan B)› for b
using spanB apply transfer by simp
have *: ‹cinner (U* *⇩V U *⇩V ψ) φ = cinner ψ φ› if ‹ψ∈B› and ‹φ∈B› for ψ φ
have *: ‹cinner (U* *⇩V U *⇩V ψ) φ = cinner ψ φ› if ‹ψ∈B› for ψ φ
apply (rule bounded_clinear_eq_on[where t=φ and G=B])
using bounded_clinear_cinner_right *[OF that]
by auto
have ‹U* *⇩V U *⇩V φ = φ› if ‹φ∈B› for φ
apply (rule cinner_extensionality)
apply (subst cinner_eq_flip)
then have ‹U* o⇩C⇩L U = id_cblinfun›
by (metis cblinfun_apply_cblinfun_compose cblinfun_eq_gen_eqI cblinfun_id_cblinfun_apply spanB)
then show ‹isometry U›
using isometry_def by blast
qed

subsection ‹Images›

(* Closure is necessary. See email 47a3bb3d-3cc3-0934-36eb-3ef0f7b70a85@ut.ee *)
lift_definition cblinfun_image :: ‹'a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector
⇒ 'a ccsubspace ⇒ 'b ccsubspace›  (infixr "*⇩S" 70)
is "λA S. closure (A ` S)"
using  bounded_clinear_def closed_closure  closed_csubspace.intro
by (simp add: bounded_clinear_def complex_vector.linear_subspace_image closure_is_closed_csubspace)

lemma cblinfun_image_mono:
assumes a1: "S ≤ T"
shows "A *⇩S S ≤ A *⇩S T"
using a1
by (simp add: cblinfun_image.rep_eq closure_mono image_mono less_eq_ccsubspace.rep_eq)

lemma cblinfun_image_0[simp]:
shows "U *⇩S 0 = 0"
thm zero_ccsubspace_def
apply transfer

lemma cblinfun_image_bot[simp]: "U *⇩S bot = bot"
using cblinfun_image_0 by auto

lemma cblinfun_image_sup[simp]:
fixes A B :: ‹'a::chilbert_space ccsubspace› and U :: "'a ⇒⇩C⇩L'b::chilbert_space"
shows ‹U *⇩S (sup A B) = sup (U *⇩S A) (U *⇩S B)›
apply transfer using bounded_clinear.bounded_linear closure_image_closed_sum by blast

lemma scaleC_cblinfun_image[simp]:
fixes A :: ‹'a::chilbert_space ⇒⇩C⇩L 'b :: chilbert_space›
and S :: ‹'a ccsubspace› and α :: complex
shows ‹(α *⇩C A) *⇩S S  = α *⇩C (A *⇩S S)›
proof-
have ‹closure ( ( ((*⇩C) α) ∘ (cblinfun_apply A) ) ` space_as_set S) =
((*⇩C) α) ` (closure (cblinfun_apply A ` space_as_set S))›
by (metis closure_scaleC image_comp)
hence ‹(closure (cblinfun_apply (α *⇩C A) ` space_as_set S)) =
((*⇩C) α) ` (closure (cblinfun_apply A ` space_as_set S))›
by (metis (mono_tags, lifting) comp_apply image_cong scaleC_cblinfun.rep_eq)
hence ‹Abs_clinear_space (closure (cblinfun_apply (α *⇩C A) ` space_as_set S)) =
α *⇩C Abs_clinear_space (closure (cblinfun_apply A ` space_as_set S))›
by (metis space_as_set_inverse cblinfun_image.rep_eq scaleC_ccsubspace.rep_eq)
have x1: "Abs_clinear_space (closure ((*⇩V) (α *⇩C A) ` space_as_set S)) =
α *⇩C Abs_clinear_space (closure ((*⇩V) A ` space_as_set S))"
using ‹Abs_clinear_space (closure (cblinfun_apply (α *⇩C A) ` space_as_set S)) =
α *⇩C Abs_clinear_space (closure (cblinfun_apply A ` space_as_set S))›
by blast
show ?thesis
unfolding cblinfun_image_def using x1 by force
qed

lemma cblinfun_image_id[simp]:
"id_cblinfun *⇩S ψ = ψ"
apply transfer

lemma cblinfun_compose_image:
‹(A o⇩C⇩L B) *⇩S S =  A *⇩S (B *⇩S S)›
apply transfer unfolding image_comp[symmetric]
apply (rule closure_bounded_linear_image_subset_eq[symmetric])

lemmas cblinfun_assoc_left = cblinfun_compose_assoc[symmetric] cblinfun_compose_image[symmetric]
lemmas cblinfun_assoc_right = cblinfun_compose_assoc cblinfun_compose_image

lemma cblinfun_image_INF_leq[simp]:
fixes U :: "'b::complex_normed_vector ⇒⇩C⇩L 'c::cbanach"
and V :: "'a ⇒ 'b ccsubspace"
shows ‹U *⇩S (INF i. V i) ≤ (INF i. U *⇩S (V i))›
apply transfer
by (simp add: INT_greatest Inter_lower closure_mono image_mono)

lemma isometry_cblinfun_image_inf_distrib':
fixes U::‹'a::complex_normed_vector ⇒⇩C⇩L 'b::cbanach› and B C::"'a ccsubspace"
shows "U *⇩S (inf B C) ≤ inf (U *⇩S B) (U *⇩S C)"
proof -
define V where ‹V b = (if b then B else C)› for b
have ‹U *⇩S (INF i. V i) ≤ (INF i. U *⇩S (V i))›
by auto
then show ?thesis
unfolding V_def
by (metis (mono_tags, lifting) INF_UNIV_bool_expand)
qed

lemma cblinfun_image_eq:
fixes S :: "'a::cbanach ccsubspace"
and A B :: "'a::cbanach ⇒⇩C⇩L'b::cbanach"
assumes "⋀x. x ∈ G ⟹ A *⇩V x = B *⇩V x" and "ccspan G ≥ S"
shows "A *⇩S S = B *⇩S S"
proof (use assms in transfer)
fix G :: "'a set" and A :: "'a ⇒ 'b" and B :: "'a ⇒ 'b" and S :: "'a set"
assume a1: "bounded_clinear A"
assume a2: "bounded_clinear B"
assume a3: "⋀x. x ∈ G ⟹ A x = B x"
assume a4: "S ⊆ closure (cspan G)"

have "A ` closure S = B ` closure S"
by (smt (verit, best) UnCI a1 a2 a3 a4 bounded_clinear_eq_on closure_Un closure_closure image_cong sup.absorb_iff1)
then show "closure (A ` S) = closure (B ` S)"
by (metis Complex_Vector_Spaces0.bounded_clinear.bounded_linear a1 a2 closure_bounded_linear_image_subset_eq)
qed

lemma cblinfun_fixes_range:
assumes "A o⇩C⇩L B = B" and "ψ ∈ space_as_set (B *⇩S top)"
shows "A *⇩V ψ = ψ"
proof-
define rangeB rangeB' where "rangeB = space_as_set (B *⇩S top)"
and "rangeB' = range (cblinfun_apply B)"
from assms have "ψ ∈ closure rangeB'"
by (simp add: cblinfun_image.rep_eq rangeB'_def top_ccsubspace.rep_eq)

then obtain ψi where ψi_lim: "ψi ⇢ ψ" and ψi_B: "ψi i ∈ rangeB'" for i
using closure_sequential by blast
have A_invariant: "A *⇩V ψi i = ψi i"
for i
proof-
from ψi_B obtain φ where φ: "ψi i = B *⇩V φ"
using rangeB'_def by blast
hence "A *⇩V ψi i = (A o⇩C⇩L B) *⇩V φ"
also have "… = B *⇩V φ"
also have "… = ψi i"
finally show ?thesis.
qed
from ψi_lim have "(λi. A *⇩V (ψi i)) ⇢ A *⇩V ψ"
by (rule isCont_tendsto_compose[rotated], simp)
with A_invariant have "(λi. ψi i) ⇢ A *⇩V ψ"
by auto
with ψi_lim show "A *⇩V ψ = ψ"
using LIMSEQ_unique by blast
qed

lemma zero_cblinfun_image[simp]: "0 *⇩S S = (0::_ ccsubspace)"
apply transfer by (simp add: complex_vector.subspace_0 image_constant[where x=0])

lemma cblinfun_image_INF_eq_general:
fixes V :: "'a ⇒ 'b::chilbert_space ccsubspace"
and U :: "'b ⇒⇩C⇩L'c::chilbert_space"
and Uinv :: "'c ⇒⇩C⇩L'b"
assumes UinvUUinv: "Uinv o⇩C⇩L U o⇩C⇩L Uinv = Uinv" and UUinvU: "U o⇩C⇩L Uinv o⇩C⇩L U = U"
― ‹Meaning: \<^term>‹Uinv› is a Pseudoinverse of \<^term>‹U››
and V: "⋀i. V i ≤ Uinv *⇩S top"
shows "U *⇩S (INF i. V i) = (INF i. U *⇩S V i)"
proof (rule antisym)
show "U *⇩S (INF i. V i) ≤ (INF i. U *⇩S V i)"
by (rule cblinfun_image_INF_leq)
next
define rangeU rangeUinv where "rangeU = U *⇩S top" and "rangeUinv = Uinv *⇩S top"
define INFUV INFV where INFUV_def: "INFUV = (INF i. U *⇩S V i)" and INFV_def: "INFV = (INF i. V i)"
from assms have "V i ≤ rangeUinv"
for i
unfolding rangeUinv_def by simp
moreover have "(Uinv o⇩C⇩L U) *⇩V ψ = ψ" if "ψ ∈ space_as_set rangeUinv"
for ψ
using UinvUUinv cblinfun_fixes_range rangeUinv_def that by fastforce
ultimately have "(Uinv o⇩C⇩L U) *⇩V ψ = ψ" if "ψ ∈ space_as_set (V i)"
for ψ i
using less_eq_ccsubspace.rep_eq that by blast
hence d1: "(Uinv o⇩C⇩L U) *⇩S (V i) = (V i)" for i
proof transfer
show "closure ((Uinv ∘ U) ` V i) = V i"
if "pred_fun ⊤ closed_csubspace V"
and "bounded_clinear Uinv"
and "bounded_clinear U"
and "⋀ψ i. ψ ∈ V i ⟹ (Uinv ∘ U) ψ = ψ"
for V :: "'a ⇒ 'b set"
and Uinv :: "'c ⇒ 'b"
and U :: "'b ⇒ 'c"
and i :: 'a
using that proof auto
show "x ∈ V i"
if "∀x. closed_csubspace (V x)"
and "bounded_clinear Uinv"
and "bounded_clinear U"
and "⋀ψ i. ψ ∈ V i ⟹ Uinv (U ψ) = ψ"
and "x ∈ closure (V i)"
for x :: 'b
using that
by (metis orthogonal_complement_of_closure closed_csubspace.subspace double_orthogonal_complement_id closure_is_closed_csubspace)
show "x ∈ closure (V i)"
if "∀x. closed_csubspace (V x)"
and "bounded_clinear Uinv"
and "bounded_clinear U"
and "⋀ψ i. ψ ∈ V i ⟹ Uinv (U ψ) = ψ"
and "x ∈ V i"
for x :: 'b
using that
using setdist_eq_0_sing_1 setdist_sing_in_set
by blast
qed
qed
have "U *⇩S V i ≤ rangeU" for i
hence "INFUV ≤ rangeU"
unfolding INFUV_def by (meson INF_lower UNIV_I order_trans)
moreover have "(U o⇩C⇩L Uinv) *⇩V ψ = ψ" if "ψ ∈ space_as_set rangeU" for ψ
using UUinvU cblinfun_fixes_range rangeU_def that by fastforce
ultimately have x: "(U o⇩C⇩L Uinv) *⇩V ψ = ψ" if "ψ ∈ space_as_set INFUV" for ψ
by (simp add: in_mono less_eq_ccsubspace.rep_eq that)

have "closure ((U ∘ Uinv) ` INFUV) = INFUV"
if "closed_csubspace INFUV"
and "bounded_clinear U"
and "bounded_clinear Uinv"
and "⋀ψ. ψ ∈ INFUV ⟹ (U ∘ Uinv) ψ = ψ"
for INFUV :: "'c set"
and U :: "'b ⇒ 'c"
and Uinv :: "'c ⇒ 'b"
using that proof auto
show "x ∈ INFUV"
if "closed_csubspace INFUV"
and "bounded_clinear U"
and "bounded_clinear Uinv"
and "⋀ψ. ψ ∈ INFUV ⟹ U (Uinv ψ) = ψ"
and "x ∈ closure INFUV"
for x :: 'c
using that
by (metis orthogonal_complement_of_closure closed_csubspace.subspace double_orthogonal_complement_id closure_is_closed_csubspace)
show "x ∈ closure INFUV"
if "closed_csubspace INFUV"
and "bounded_clinear U"
and "bounded_clinear Uinv"
and "⋀ψ. ψ ∈ INFUV ⟹ U (Uinv ψ) = ψ"
and "x ∈ INFUV"
for x :: 'c
using that
using setdist_eq_0_sing_1 setdist_sing_in_set
qed
hence "(U o⇩C⇩L Uinv) *⇩S INFUV = INFUV"
by (metis (mono_tags, opaque_lifting) x cblinfun_image.rep_eq cblinfun_image_id id_cblinfun_apply image_cong
space_as_set_inject)
hence "INFUV = U *⇩S Uinv *⇩S INFUV"
also have "… ≤ U *⇩S (INF i. Uinv *⇩S U *⇩S V i)"
unfolding INFUV_def
by (metis cblinfun_image_mono cblinfun_image_INF_leq)
also have "… = U *⇩S INFV"
using d1
by (metis (no_types, lifting) INFV_def cblinfun_assoc_left(2) image_cong)
finally show "INFUV ≤ U *⇩S INFV".
qed

lemma unitary_range[simp]:
assumes "unitary U"
shows "U *⇩S top = top"
using assms unfolding unitary_def apply transfer
by (metis closure_UNIV comp_apply surj_def)

assumes "isometry U"
shows "U* *⇩S top = top"
proof-
from assms have "top = U* *⇩S U *⇩S top"
also have "… ≤ U* *⇩S top"
finally show ?thesis
using top.extremum_unique by blast
qed

lemma cblinfun_image_INF_eq[simp]:
fixes V :: "'a ⇒ 'b::chilbert_space ccsubspace"
and U :: "'b ⇒⇩C⇩L 'c::chilbert_space"
assumes ‹isometry U›
shows "U *⇩S (INF i. V i) = (INF i. U *⇩S V i)"
proof -
from ‹isometry U› have "U* o⇩C⇩L U o⇩C⇩L U* = U*"
unfolding isometry_def by simp
moreover from ‹isometry U› have "U o⇩C⇩L U* o⇩C⇩L U = U"
unfolding isometry_def
by (```