# Theory Bounded_Linear_Operator

```section ‹Bounded Linear Operator›
theory Bounded_Linear_Operator
imports
"HOL-Analysis.Analysis"
begin

typedef (overloaded) 'a blinop = "UNIV::('a, 'a) blinfun set"
by simp

setup_lifting type_definition_blinop

lift_definition blinop_apply::"('a::real_normed_vector) blinop ⇒ 'a ⇒ 'a" is blinfun_apply .
lift_definition Blinop::"('a::real_normed_vector ⇒ 'a) ⇒ 'a blinop" is Blinfun .

no_notation vec_nth (infixl "\$" 90)
notation blinop_apply (infixl "\$" 999)
declare [[coercion "blinop_apply :: ('a::real_normed_vector) blinop ⇒ 'a ⇒ 'a"]]

instantiation blinop :: (real_normed_vector) real_normed_vector
begin

lift_definition norm_blinop :: "'a blinop ⇒ real" is norm .

lift_definition minus_blinop :: "'a blinop ⇒ 'a blinop ⇒ 'a blinop" is minus .

lift_definition dist_blinop :: "'a blinop ⇒ 'a blinop ⇒ real" is dist .

definition uniformity_blinop :: "('a blinop × 'a blinop) filter" where
"uniformity_blinop = (INF e∈{0<..}. principal {(x, y). dist x y < e})"

definition open_blinop :: "'a blinop set ⇒ bool" where
"open_blinop U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)"

lift_definition uminus_blinop :: "'a blinop ⇒ 'a blinop" is uminus .

lift_definition zero_blinop :: "'a blinop" is 0 .

lift_definition plus_blinop :: "'a blinop ⇒ 'a blinop ⇒ 'a blinop" is plus .

lift_definition scaleR_blinop::"real ⇒ 'a blinop ⇒ 'a blinop" is scaleR .

lift_definition sgn_blinop :: "'a blinop ⇒ 'a blinop" is sgn .

instance
apply standard
apply (transfer', simp add: algebra_simps sgn_div_norm open_uniformity norm_triangle_le
uniformity_blinop_def dist_norm
open_blinop_def)+
done
end

lemma bounded_bilinear_blinop_apply: "bounded_bilinear (\$)"
unfolding bounded_bilinear_def
by transfer (simp add: blinfun.bilinear_simps blinfun.bounded)

interpretation blinop: bounded_bilinear "(\$)"
by (rule bounded_bilinear_blinop_apply)

lemma blinop_eqI: "(⋀i. x \$ i = y \$ i) ⟹ x = y"
by transfer (rule blinfun_eqI)

lemmas bounded_linear_apply_blinop[intro, simp] = blinop.bounded_linear_left
declare blinop.tendsto[tendsto_intros]
declare blinop.FDERIV[derivative_intros]
declare blinop.continuous[continuous_intros]
declare blinop.continuous_on[continuous_intros]

instance blinop :: (banach) banach
apply standard
unfolding convergent_def LIMSEQ_def Cauchy_def
apply transfer
unfolding convergent_def[symmetric] LIMSEQ_def[symmetric] Cauchy_def[symmetric]
Cauchy_convergent_iff
.

instance blinop :: (euclidean_space) heine_borel
apply standard
unfolding LIMSEQ_def bounded_def
apply transfer
unfolding LIMSEQ_def[symmetric] bounded_def[symmetric]
apply (rule bounded_imp_convergent_subsequence)
.

instantiation blinop::("{real_normed_vector, perfect_space}") real_normed_algebra_1
begin

lift_definition one_blinop::"'a blinop" is id_blinfun .
lemma blinop_apply_one_blinop[simp]: "1 \$ x = x"
by transfer simp

lift_definition times_blinop :: "'a blinop ⇒ 'a blinop ⇒ 'a blinop" is blinfun_compose .

lemma blinop_apply_times_blinop[simp]: "(f * g) \$ x = f \$ (g \$ x)"
by transfer simp

instance
proof
from not_open_singleton[of "0::'a"] have "{0::'a} ≠ UNIV" by force
then obtain x :: 'a where "x ≠ 0" by auto
show "0 ≠ (1::'a blinop)"
apply transfer
apply transfer
apply (auto dest!: fun_cong[where x=x] simp: ‹x ≠ 0›)
done
qed (transfer, transfer,
simp add: o_def linear_simps onorm_compose onorm_id onorm_compose[simplified o_def])+
end

lemmas bounded_bilinear_bounded_uniform_limit_intros[uniform_limit_intros] =
bounded_bilinear.bounded_uniform_limit[OF Bounded_Linear_Operator.bounded_bilinear_blinop_apply]
bounded_bilinear.bounded_uniform_limit[OF Bounded_Linear_Function.bounded_bilinear_blinfun_apply]
bounded_bilinear.bounded_uniform_limit[OF Bounded_Linear_Operator.blinop.flip]
bounded_bilinear.bounded_uniform_limit[OF Bounded_Linear_Function.blinfun.flip]
bounded_linear.uniform_limit[OF blinop.bounded_linear_right]
bounded_linear.uniform_limit[OF blinop.bounded_linear_left]
bounded_linear.uniform_limit[OF bounded_linear_apply_blinop]

no_notation
blinop_apply (infixl "\$" 999)
notation vec_nth (infixl "\$" 90)

end
```