# Theory Banach_Steinhaus_Missing

(*
File:   Banach_Steinhaus_Missing.thy
Author: Dominique Unruh, University of Tartu
Author: Jose Manuel Rodriguez Caballero, University of Tartu
*)
section ‹Missing results for the proof of Banach-Steinhaus theorem›

theory Banach_Steinhaus_Missing
imports
"HOL-Analysis.Infinite_Set_Sum"

begin
subsection ‹Results missing for the proof of Banach-Steinhaus theorem›
text ‹
The results proved here are preliminaries for the proof of Banach-Steinhaus theorem using Sokal's
approach, but they do not explicitly appear in Sokal's paper ~\cite{sokal2011reall}.
›

text‹Notation for the norm›
bundle notation_norm begin
notation norm ("∥_∥")
end

bundle no_notation_norm begin
no_notation norm ("∥_∥")
end

unbundle notation_norm

text‹Notation for apply bilinear function›
bundle notation_blinfun_apply begin
notation blinfun_apply (infixr "*⇩v" 70)
end

bundle no_notation_blinfun_apply begin
no_notation blinfun_apply (infixr "*⇩v" 70)
end

unbundle notation_blinfun_apply

lemma bdd_above_plus:
fixes f::‹'a ⇒ real›
assumes ‹bdd_above (f  S)› and ‹bdd_above (g  S)›
shows ‹bdd_above ((λ x. f x + g x)  S)›
text ‹
Explanation: If the images of two real-valued functions \<^term>‹f›,\<^term>‹g› are bounded above on a
set \<^term>‹S›, then the image of their sum is bounded on \<^term>‹S›.
›
proof-
obtain M where ‹⋀ x. x∈S ⟹ f x ≤ M›
using ‹bdd_above (f  S)› unfolding bdd_above_def by blast
obtain N where ‹⋀ x. x∈S ⟹ g x ≤ N›
using ‹bdd_above (g  S)› unfolding bdd_above_def by blast
have ‹⋀ x. x∈S ⟹ f x + g x ≤ M + N›
using ‹⋀x. x ∈ S ⟹ f x ≤ M› ‹⋀x. x ∈ S ⟹ g x ≤ N› by fastforce
thus ?thesis unfolding bdd_above_def by blast
qed

text‹The maximum of two functions›
definition pointwise_max:: "('a ⇒ 'b::ord) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b)" where
‹pointwise_max f g = (λx. max (f x) (g x))›

lemma max_Sup_absorb_left:
fixes f g::‹'a ⇒ real›
assumes ‹X ≠ {}› and ‹bdd_above (f  X)› and ‹bdd_above (g  X)› and ‹Sup (f  X) ≥ Sup (g  X)›
shows ‹Sup ((pointwise_max f g)  X) = Sup (f  X)›

text ‹Explanation: For real-valued functions \<^term>‹f› and \<^term>‹g›, if the supremum of \<^term>‹f› is
greater-equal the supremum of \<^term>‹g›, then the supremum of \<^term>‹max f g› equals the supremum of
\<^term>‹f›. (Under some technical conditions.)›

proof-
have y_Sup: ‹y ∈ ((λ x. max (f x) (g x))  X) ⟹ y ≤ Sup (f  X)› for y
proof-
assume ‹y ∈ ((λ x. max (f x) (g x))  X)›
then obtain x where ‹y = max (f x) (g x)› and ‹x ∈ X›
by blast
have ‹f x ≤ Sup (f  X)›
by (simp add:  ‹x ∈ X› ‹bdd_above (f  X)› cSUP_upper)
moreover have  ‹g x ≤ Sup (g  X)›
by (simp add:  ‹x ∈ X› ‹bdd_above (g  X)› cSUP_upper)
ultimately have ‹max (f x) (g x) ≤ Sup (f  X)›
using  ‹Sup (f  X) ≥ Sup (g  X)› by auto
thus ?thesis by (simp add: ‹y = max (f x) (g x)›)
qed
have y_f_X: ‹y ∈ f  X ⟹ y ≤ Sup ((λ x. max (f x) (g x))  X)› for y
proof-
assume ‹y ∈ f  X›
then obtain x where ‹x ∈ X› and ‹y = f x›
by blast
have  ‹bdd_above ((λ ξ. max (f ξ) (g ξ))  X)›
by (metis (no_types) ‹bdd_above (f  X)› ‹bdd_above (g  X)› bdd_above_image_sup sup_max)
moreover have ‹e > 0 ⟹ ∃ k ∈ (λ ξ. max (f ξ) (g ξ))  X. y ≤ k + e›
for e::real
using ‹Sup (f  X) ≥ Sup (g  X)› by (smt ‹x ∈ X› ‹y = f x› image_eqI)
ultimately show ?thesis
using ‹x ∈ X› ‹y = f x› cSUP_upper by fastforce
qed
have ‹Sup ((λ x. max (f x) (g x))  X) ≤ Sup (f  X)›
using y_Sup by (simp add: ‹X ≠ {}› cSup_least)
moreover have ‹Sup ((λ x. max (f x) (g x))  X) ≥ Sup (f  X)›
using y_f_X by (metis (mono_tags) cSup_least calculation empty_is_image)
ultimately show ?thesis unfolding pointwise_max_def by simp
qed

lemma max_Sup_absorb_right:
fixes f g::‹'a ⇒ real›
assumes ‹X ≠ {}› and ‹bdd_above (f  X)› and ‹bdd_above (g  X)› and ‹Sup (f  X) ≤ Sup (g  X)›
shows ‹Sup ((pointwise_max f g)  X) = Sup (g  X)›
text ‹
Explanation: For real-valued functions \<^term>‹f› and \<^term>‹g› and a nonempty set \<^term>‹X›, such that
the \<^term>‹f› and \<^term>‹g› are bounded above on \<^term>‹X›, if the supremum of \<^term>‹f› on \<^term>‹X› is
lower-equal the supremum of \<^term>‹g› on \<^term>‹X›, then the supremum of \<^term>‹pointwise_max f g› on \<^term>‹X›
equals the supremum of \<^term>‹g›. This is the right analog of @{text max_Sup_absorb_left}.
›
proof-
have ‹Sup ((pointwise_max g f)  X) = Sup (g  X)›
using  assms by (simp add: max_Sup_absorb_left)
moreover have ‹pointwise_max g f = pointwise_max f g›
unfolding pointwise_max_def  by auto
ultimately show ?thesis by simp
qed

lemma max_Sup:
fixes f g::‹'a ⇒ real›
assumes ‹X ≠ {}› and ‹bdd_above (f  X)› and ‹bdd_above (g  X)›
shows ‹Sup ((pointwise_max f g)  X) = max (Sup (f  X)) (Sup (g  X))›
text ‹
Explanation: Let \<^term>‹X› be a nonempty set. Two supremum over \<^term>‹X› of the maximum of two
real-value functions is equal to the maximum of their suprema over \<^term>‹X›, provided that the
functions are bounded above on \<^term>‹X›.
›
proof(cases ‹Sup (f  X) ≥ Sup (g  X)›)
case True thus ?thesis by (simp add: assms(1) assms(2) assms(3) max_Sup_absorb_left)
next
case False
have f1: "¬ 0 ≤ Sup (f  X) + - 1 * Sup (g  X)"
using False by linarith
hence "Sup (Banach_Steinhaus_Missing.pointwise_max f g  X) = Sup (g  X)"
by (simp add: assms(1) assms(2) assms(3) max_Sup_absorb_right)
thus ?thesis
using f1 by linarith
qed

lemma identity_telescopic:
fixes x :: ‹_ ⇒ 'a::real_normed_vector›
assumes ‹x ⇢ l›
shows ‹(λ N. sum (λ k. x (Suc k) - x k) {n..N}) ⇢ l - x n›
text‹
Expression of a limit as a telescopic series.
Explanation: If \<^term>‹x› converges to \<^term>‹l› then the sum \<^term>‹sum (λ k. x (Suc k) - x k) {n..N}›
converges to \<^term>‹l - x n› as \<^term>‹N› goes to infinity.
›
proof-
have ‹(λ p. x (p + Suc n)) ⇢ l›
using ‹x ⇢ l› by (rule LIMSEQ_ignore_initial_segment)
hence ‹(λ p. x (Suc n + p)) ⇢ l›
hence ‹(λ p. x (Suc (n + p))) ⇢ l›
by simp
hence ‹(λ t. (- (x n)) + (λ p.  x (Suc (n + p))) t ) ⇢ (- (x n))  + l›
using tendsto_add_const_iff by metis
hence f1: ‹(λ p. x (Suc (n + p)) - x n)⇢ l - x n›
by simp
have ‹sum (λ k. x (Suc k) - x k) {n..n+p} = x (Suc (n+p)) - x n› for p
by (simp add: sum_Suc_diff)
moreover have ‹(λ N. sum (λ k. x (Suc k) - x k) {n..N}) (n + t)
= (λ p. sum (λ k. x (Suc k) - x k) {n..n+p}) t› for t
by blast
ultimately have  ‹(λ p. (λ N. sum (λ k. x (Suc k) - x k) {n..N}) (n + p)) ⇢ l - x n›
using f1 by simp
hence ‹(λ p. (λ N. sum (λ k. x (Suc k) - x k) {n..N}) (p + n)) ⇢ l - x n›
hence  ‹(λ p. (λ N. sum (λ k. x (Suc k) - x k) {n..N}) p) ⇢ l - x n›
using Topological_Spaces.LIMSEQ_offset[where f = "(λ N. sum (λ k. x (Suc k) - x k) {n..N})"
and a = "l - x n" and k = n] by blast
hence  ‹(λ M. (λ N. sum (λ k. x (Suc k) - x k) {n..N}) M) ⇢ l - x n›
by simp
thus ?thesis by blast
qed

lemma bound_Cauchy_to_lim:
assumes ‹y ⇢ x› and ‹⋀n. ∥y (Suc n) - y n∥ ≤ c^n› and ‹y 0 = 0› and ‹c < 1›
shows ‹∥x - y (Suc n)∥ ≤ (c / (1 - c)) * c ^ n›
text‹
Inequality about a sequence of approximations assuming that the sequence of differences is bounded
by a geometric progression.
Explanation: Let \<^term>‹y› be a sequence converging to \<^term>‹x›.
If \<^term>‹y› satisfies the inequality ‹∥y (Suc n) - y n∥ ≤ c ^ n› for some \<^term>‹c < 1› and
assuming \<^term>‹y 0 = 0› then the inequality ‹∥x - y (Suc n)∥ ≤ (c / (1 - c)) * c ^ n› holds.
›
proof-
have ‹c ≥ 0›
using ‹⋀ n. ∥y (Suc n) - y n∥ ≤ c^n› by (smt norm_imp_pos_and_ge power_Suc0_right)
have norm_1: ‹norm (∑k = Suc n..N. y (Suc k) - y k) ≤ (c ^ Suc n)/(1 - c)› for N
proof(cases ‹N < Suc n›)
case True
hence ‹∥sum (λk. y (Suc k) - y k) {Suc n .. N}∥ = 0›
by auto
thus ?thesis  using  ‹c ≥ 0› ‹c < 1› by auto
next
case False
hence ‹N ≥ Suc n›
by auto
have ‹c^(Suc N) ≥ 0›
using ‹c ≥ 0› by auto
have ‹1 - c > 0›
by (simp add: ‹c < 1›)
hence ‹(1 - c)/(1 - c) = 1›
by auto
have ‹∥sum (λk. y (Suc k) - y k) {Suc n .. N}∥ ≤ (sum (λk. ∥y (Suc k) - y k∥) {Suc n .. N})›
by (simp add: sum_norm_le)
hence ‹∥sum (λk. y (Suc k) - y k) {Suc n .. N}∥ ≤ (sum (power c) {Suc n .. N})›
by (simp add: assms(2) sum_norm_le)
hence ‹(1 - c) * ∥sum (λk. y (Suc k) - y k) {Suc n .. N}∥
≤ (1 - c) * (sum (power c) {Suc n .. N})›
using ‹0 < 1 - c› mult_le_cancel_iff2 by blast
also have ‹… = c^(Suc n) - c^(Suc N)›
using Set_Interval.sum_gp_multiplied ‹Suc n ≤ N› by blast
also have ‹… ≤ c^(Suc n)›
using ‹c^(Suc N) ≥ 0› by auto
finally have ‹(1 - c) * ∥∑k = Suc n..N. y (Suc k) - y k∥ ≤ c ^ Suc n›
by blast
hence ‹((1 - c) * ∥∑k = Suc n..N. y (Suc k) - y k∥)/(1 - c)
≤ (c ^ Suc n)/(1 - c)›
using ‹0 < 1 - c› by (smt divide_right_mono)
thus ‹∥∑k = Suc n..N. y (Suc k) - y k∥ ≤ (c ^ Suc n)/(1 - c)›
using ‹0 < 1 - c› by auto
qed
have ‹(λ N. (sum (λk. y (Suc k) - y k) {Suc n .. N})) ⇢ x - y (Suc n)›
by (metis (no_types) ‹y ⇢ x› identity_telescopic)
hence ‹(λ N. ∥sum (λk. y (Suc k) - y k) {Suc n .. N}∥) ⇢ ∥x - y (Suc n)∥›
using tendsto_norm by blast
hence ‹∥x - y (Suc n)∥ ≤ (c ^ Suc n)/(1 - c)›
using norm_1 Lim_bounded by blast
hence  ‹∥x - y (Suc n)∥ ≤ (c ^ Suc n)/(1 - c)›
by auto
moreover have ‹(c ^ Suc n)/(1 - c) = (c / (1 - c)) * (c ^ n)›
by (simp add: divide_inverse_commute)
ultimately show ‹∥x - y (Suc n)∥ ≤ (c / (1 - c)) * (c ^ n)› by linarith
qed

lemma onorm_open_ball:
includes notation_norm
shows ‹∥f∥ = Sup { ∥f *⇩v x∥ | x. ∥x∥ < 1 }›
text ‹
Explanation: Let \<^term>‹f› be a bounded linear operator. The operator norm of \<^term>‹f› is the
supremum of \<^term>‹norm (f x)› for \<^term>‹x› such that \<^term>‹norm x < 1›.
›
proof(cases ‹(UNIV::'a set) = 0›)
case True
hence ‹x = 0› for x::'a
by auto
hence ‹f *⇩v x = 0› for x
by (metis (full_types) blinfun.zero_right)
hence ‹∥f∥ = 0›
by (simp add: blinfun_eqI zero_blinfun.rep_eq)
have ‹{ ∥f *⇩v x∥ | x. ∥x∥ < 1} = {0}›
by (smt Collect_cong ‹⋀x. f *⇩v x = 0› norm_zero singleton_conv)
hence ‹Sup { ∥f *⇩v x∥ | x. ∥x∥ < 1} = 0›
by simp
thus ?thesis using ‹∥f∥ = 0› by auto
next
case False
hence ‹(UNIV::'a set) ≠ 0›
by simp
have nonnegative: ‹∥f *⇩v x∥ ≥ 0› for x
by simp
have ‹∃ x::'a. x ≠ 0›
using ‹UNIV ≠ 0› by auto
then obtain x::'a where ‹x ≠ 0›
by blast
hence ‹∥x∥ ≠ 0›
by auto
define y where ‹y = x /⇩R ∥x∥›
have ‹norm y = ∥ x /⇩R ∥x∥ ∥›
unfolding y_def by auto
also have ‹… = ∥x∥ /⇩R ∥x∥›
by auto
also have ‹… = 1›
using ‹∥x∥ ≠ 0› by auto
finally have ‹∥y∥ = 1›
by blast
hence norm_1_non_empty: ‹{ ∥f *⇩v x∥ | x. ∥x∥ = 1} ≠ {}›
by blast
have norm_1_bounded: ‹bdd_above { ∥f *⇩v x∥ | x. ∥x∥ = 1}›
unfolding bdd_above_def apply auto
by (metis norm_blinfun)
have norm_less_1_non_empty: ‹{∥f *⇩v x∥ | x. ∥x∥ < 1} ≠ {}›
by (metis (mono_tags, lifting) Collect_empty_eq_bot bot_empty_eq empty_iff norm_zero
zero_less_one)
have norm_less_1_bounded: ‹bdd_above {∥f *⇩v x∥ | x. ∥x∥ < 1}›
proof-
have ‹∃r. ∥a r∥ < 1 ⟶ ∥f *⇩v (a r)∥ ≤ r› for a :: "real ⇒ 'a"
proof-
obtain r :: "('a ⇒⇩L 'b) ⇒ real" where
"⋀f x. 0 ≤ r f ∧ (bounded_linear f ⟶ ∥f *⇩v x∥ ≤ ∥x∥ * r f)"
using bounded_linear.nonneg_bounded by moura
have ‹¬ ∥f∥ < 0›
by simp
hence "(∃r. ∥f∥ * ∥a r∥ ≤ r) ∨ (∃r. ∥a r∥ < 1 ⟶ ∥f *⇩v a r∥ ≤ r)"
by (meson less_eq_real_def mult_le_cancel_left2)
thus ?thesis using dual_order.trans norm_blinfun by blast
qed
hence ‹∃ M. ∀ x. ∥x∥ < 1 ⟶ ∥f *⇩v x∥ ≤ M›
by metis
thus ?thesis by auto
qed
have Sup_non_neg: ‹Sup {∥f *⇩v x∥ |x. ∥x∥ = 1} ≥ 0›
by (smt Collect_empty_eq cSup_upper mem_Collect_eq nonnegative norm_1_bounded norm_1_non_empty)
have ‹{0::real} ≠ {}›
by simp
have ‹bdd_above {0::real}›
by simp
show ‹∥f∥ = Sup {∥f *⇩v x∥ | x. ∥x∥ < 1}›
proof(cases ‹∀x. f *⇩v x = 0›)
case True
have ‹∥f *⇩v x∥ = 0› for x
by (simp add: True)
hence ‹{∥f *⇩v x∥ | x. ∥x∥ < 1 } ⊆ {0}›
by blast
moreover have ‹{∥f *⇩v x∥ | x. ∥x∥ < 1 } ⊇ {0}›
using calculation norm_less_1_non_empty by fastforce
ultimately have ‹{∥f *⇩v x∥ | x. ∥x∥ < 1 } = {0}›
by blast
hence Sup1: ‹Sup {∥f *⇩v x∥ | x. ∥x∥ < 1 } = 0›
by simp
have ‹∥f∥ = 0›
by (simp add: True blinfun_eqI)
moreover have ‹Sup {∥f *⇩v x∥ | x. ∥x∥ < 1} = 0›
using Sup1 by blast
ultimately show ?thesis by simp
next
case False
have norm_f_eq_leq: ‹y ∈ {∥f *⇩v x∥ | x. ∥x∥ = 1} ⟹
y ≤ Sup {∥f *⇩v x∥ | x. ∥x∥ < 1}› for y
proof-
assume ‹y ∈ {∥f *⇩v x∥ | x. ∥x∥ = 1}›
hence ‹∃ x. y = ∥f *⇩v x∥ ∧ ∥x∥ = 1›
by blast
then obtain x where ‹y = ∥f *⇩v x∥› and ‹∥x∥ = 1›
by auto
define y' where ‹y' n = (1 - (inverse (real (Suc n)))) *⇩R y› for n
have ‹y' n ∈ {∥f *⇩v x∥ | x. ∥x∥ < 1}› for n
proof-
have ‹y' n = (1 - (inverse (real (Suc n)))) *⇩R ∥f *⇩v x∥›
using y'_def ‹y = ∥f *⇩v x∥› by blast
also have ‹... = ¦(1 - (inverse (real (Suc n))))¦ *⇩R ∥f *⇩v x∥›
by (metis (mono_tags, hide_lams) ‹y = ∥f *⇩v x∥› abs_1 abs_le_self_iff abs_of_nat
diff_ge_0_iff_ge eq_iff_diff_eq_0 inverse_1 inverse_le_iff_le nat.distinct(1) of_nat_0
of_nat_Suc of_nat_le_0_iff zero_less_abs_iff zero_neq_one)
also have ‹... = ∥f *⇩v ((1 - (inverse (real (Suc n)))) *⇩R  x)∥›
by (simp add: blinfun.scaleR_right)
finally have y'_1: ‹y' n = ∥f *⇩v ( (1 - (inverse (real (Suc n)))) *⇩R x)∥›
by blast
have ‹∥(1 - (inverse (Suc n))) *⇩R x∥ = (1 - (inverse (real (Suc n)))) * ∥x∥›
by (simp add: linordered_field_class.inverse_le_1_iff)
hence ‹∥(1 - (inverse (Suc n))) *⇩R x∥ < 1›
by (simp add: ‹∥x∥ = 1›)
thus ?thesis using y'_1 by blast
qed
have ‹(λn. (1 - (inverse (real (Suc n)))) ) ⇢ 1›
using Limits.LIMSEQ_inverse_real_of_nat_add_minus by simp
hence ‹(λn. (1 - (inverse (real (Suc n)))) *⇩R y) ⇢ 1 *⇩R y›
using Limits.tendsto_scaleR by blast
hence ‹(λn. (1 - (inverse (real (Suc n)))) *⇩R y) ⇢ y›
by simp
hence ‹(λn. y' n) ⇢ y›
using y'_def by simp
hence ‹y' ⇢ y›
by simp
have ‹y' n ≤ Sup {∥f *⇩v x∥ | x. ∥x∥ < 1}› for n
using cSup_upper ‹⋀n. y' n ∈ {∥f *⇩v x∥ |x. ∥x∥ < 1}› norm_less_1_bounded by blast
hence ‹y ≤ Sup {∥f *⇩v x∥ | x. ∥x∥ < 1}›
using ‹y' ⇢ y› Topological_Spaces.Sup_lim by (meson LIMSEQ_le_const2)
thus ?thesis by blast
qed
hence ‹Sup {∥f *⇩v x∥ | x. ∥x∥ = 1} ≤ Sup {∥f *⇩v x∥ | x. ∥x∥ < 1}›
by (metis (lifting) cSup_least norm_1_non_empty)
have ‹y ∈ {∥f *⇩v x∥ | x. ∥x∥ < 1} ⟹ y ≤ Sup {∥f *⇩v x∥ | x. ∥x∥ = 1}› for y
proof(cases ‹y = 0›)
case True thus ?thesis by (simp add: Sup_non_neg)
next
case False
hence ‹y ≠ 0› by blast
assume ‹y ∈ {∥f *⇩v x∥ | x. ∥x∥ < 1}›
hence ‹∃ x. y = ∥f *⇩v x∥ ∧ ∥x∥ < 1›
by blast
then obtain x where ‹y = ∥f *⇩v x∥› and ‹∥x∥ < 1›
by blast
have ‹(1/∥x∥) * y = (1/∥x∥) * ∥f x∥›
by (simp add: ‹y = ∥f *⇩v x∥›)
also have ‹... = ¦1/∥x∥¦ * ∥f *⇩v x∥›
by simp
also have ‹... = ∥(1/∥x∥) *⇩R (f *⇩v x)∥›
by simp
also have ‹... = ∥f *⇩v ((1/∥x∥) *⇩R x)∥›
by (simp add: blinfun.scaleR_right)
finally have ‹(1/∥x∥) * y  = ∥f *⇩v ((1/∥x∥) *⇩R x)∥›
by blast
have ‹x ≠ 0›
using  ‹y ≠ 0› ‹y = ∥f *⇩v x∥› blinfun.zero_right by auto
have ‹∥ (1/∥x∥) *⇩R x ∥ = ¦ (1/∥x∥) ¦ * ∥x∥›
by simp
also have ‹... = (1/∥x∥) * ∥x∥›
by simp
finally have  ‹∥(1/∥x∥) *⇩R x∥ = 1›
using ‹x ≠ 0› by simp
hence ‹(1/∥x∥) * y ∈ { ∥f *⇩v x∥ | x. ∥x∥ = 1}›
using ‹1 / ∥x∥ * y = ∥f *⇩v (1 / ∥x∥) *⇩R x∥› by blast
hence ‹(1/∥x∥) * y ≤ Sup { ∥f *⇩v x∥ | x. ∥x∥ = 1}›
by (simp add: cSup_upper norm_1_bounded)
moreover have ‹y ≤ (1/∥x∥) * y›
by (metis ‹∥x∥ < 1› ‹y = ∥f *⇩v x∥› mult_le_cancel_right1 norm_not_less_zero
order.strict_implies_order ‹x ≠ 0› less_divide_eq_1_pos zero_less_norm_iff)
ultimately show ?thesis by linarith
qed
hence ‹Sup { ∥f *⇩v x∥ | x. ∥x∥ < 1} ≤ Sup { ∥f *⇩v x∥ | x. ∥x∥ = 1}›
by (smt cSup_least norm_less_1_non_empty)
hence ‹Sup { ∥f *⇩v x∥ | x. ∥x∥ = 1} = Sup { ∥f *⇩v x∥ | x. ∥x∥ < 1}›
using ‹Sup {∥f *⇩v x∥ |x. norm x = 1} ≤ Sup { ∥f *⇩v x∥ |x. ∥x∥ < 1}› by linarith
have f1: ‹(SUP x. ∥f *⇩v x∥ / ∥x∥) = Sup { ∥f *⇩v x∥ / ∥x∥ | x. True}›
by (simp add: full_SetCompr_eq)
have ‹y ∈ { ∥f *⇩v x∥ / ∥x∥ |x. True} ⟹ y ∈ { ∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0}›
for y
proof-
assume ‹y ∈ { ∥f *⇩v x∥ / ∥x∥ |x. True}› show ?thesis
proof(cases ‹y = 0›)
case True  thus ?thesis by simp
next
case False
have ‹∃ x. y = ∥f *⇩v x∥ / ∥x∥›
using ‹y ∈ { ∥f *⇩v x∥ / ∥x∥ |x. True}› by auto
then obtain x where ‹y = ∥f *⇩v x∥ / ∥x∥›
by blast
hence ‹y = ¦(1/∥x∥)¦ * ∥ f *⇩v x ∥›
by simp
hence ‹y = ∥(1/∥x∥) *⇩R (f *⇩v x)∥›
by simp
hence ‹y = ∥f ((1/∥x∥) *⇩R x)∥›
by (simp add: blinfun.scaleR_right)
moreover have ‹∥ (1/∥x∥) *⇩R x ∥ = 1›
using False ‹y = ∥f *⇩v x∥ / ∥x∥› by auto
ultimately have ‹y ∈ {∥f *⇩v x∥ |x. ∥x∥ = 1}›
by blast
thus ?thesis by blast
qed
qed
moreover have ‹y ∈ {∥f x∥ |x. ∥x∥ = 1} ∪ {0} ⟹ y ∈ {∥f *⇩v x∥ / ∥x∥ |x. True}›
for y
proof(cases ‹y = 0›)
case True thus ?thesis by auto
next
case False
hence ‹y ∉ {0}›
by simp
moreover assume ‹y ∈ {∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0}›
ultimately have ‹y ∈ {∥f *⇩v x∥ |x. ∥x∥ = 1}›
by simp
then obtain x where ‹∥x∥ = 1› and ‹y = ∥f *⇩v x∥›
by auto
have ‹y = ∥f *⇩v x∥ / ∥x∥› using  ‹∥x∥ = 1›  ‹y = ∥f *⇩v x∥›
by simp
thus ?thesis by auto
qed
ultimately have ‹{∥f *⇩v x∥ / ∥x∥ |x. True} = {∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0}›
by blast
hence ‹Sup {∥f *⇩v x∥ / ∥x∥ |x. True} = Sup ({∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0})›
by simp
have "⋀r s. ¬ (r::real) ≤ s ∨ sup r s = s"
by (metis (lifting) sup.absorb_iff1 sup_commute)
hence ‹Sup ({∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {(0::real)})
= max (Sup {∥f *⇩v x∥ |x. ∥x∥ = 1}) (Sup {0::real})›
using ‹0 ≤ Sup {∥f *⇩v x∥ |x. ∥x∥ = 1}› ‹bdd_above {0}› ‹{0} ≠ {}› cSup_singleton
cSup_union_distrib max.absorb_iff1 sup_commute norm_1_bounded norm_1_non_empty
by (metis (no_types, lifting) )
moreover have ‹Sup {(0::real)} = (0::real)›
by simp
ultimately have ‹Sup ({∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0}) = Sup {∥f *⇩v x∥ |x. ∥x∥ = 1}›
using Sup_non_neg by linarith
moreover have ‹Sup ( {∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0})
= max (Sup {∥f *⇩v x∥ |x. ∥x∥ = 1}) (Sup {0}) ›
using Sup_non_neg  ‹Sup ({∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0})
= max (Sup {∥f *⇩v x∥ |x. ∥x∥ = 1}) (Sup {0})›
by auto
ultimately have f2: ‹Sup {∥f *⇩v x∥ / ∥x∥ | x. True} = Sup {∥f *⇩v x∥ | x. ∥x∥ = 1}›
using ‹Sup {∥f *⇩v x∥ / ∥x∥ |x. True} = Sup ({∥f *⇩v x∥ |x. ∥x∥ = 1} ∪ {0})› by linarith
have ‹(SUP x. ∥f *⇩v x∥ / ∥x∥) = Sup {∥f *⇩v x∥ | x. ∥x∥ = 1}›
using f1 f2 by linarith
hence ‹(SUP x. ∥f *⇩v x∥ / ∥x∥) = Sup {∥f *⇩v x∥ | x. ∥x∥ < 1 }›
by (simp add: ‹Sup {∥f *⇩v x∥ |x. ∥x∥ = 1} = Sup {∥f *⇩v x∥ |x. ∥x∥ < 1}›)
thus ?thesis apply transfer by (simp add: onorm_def)
qed
qed

lemma onorm_r:
includes notation_norm
assumes ‹r > 0›
shows ‹∥f∥ = Sup ((λx. ∥f *⇩v x∥)  (ball 0 r)) / r›
text ‹
Explanation: The norm of \<^term>‹f› is \<^term>‹1/r› of the supremum of the norm of \<^term>‹f *⇩v x› for
\<^term>‹x› in the ball of radius \<^term>‹r› centered at the origin.
›
proof-
have ‹∥f∥ = Sup {∥f *⇩v x∥ |x. ∥x∥ < 1}›
using onorm_open_ball by blast
moreover have ‹{∥f *⇩v x∥ |x. ∥x∥ < 1} = (λx. ∥f *⇩v x∥)  (ball 0 1)›
unfolding ball_def by auto
ultimately have onorm_f: ‹∥f∥ = Sup ((λx. ∥f *⇩v x∥)  (ball 0 1))›
by simp
have s2: ‹x ∈ (λt. r *⇩R ∥f *⇩v t∥)  ball 0 1 ⟹ x ≤ r * Sup ((λt. ∥f *⇩v t∥)  ball 0 1)› for x
proof-
assume ‹x ∈ (λt. r *⇩R ∥f *⇩v t∥)  ball 0 1›
hence ‹∃ t. x = r *⇩R ∥f *⇩v t∥ ∧ ∥t∥ < 1›
by auto
then obtain t where ‹x = r *⇩R ∥f *⇩v t∥› and ‹∥t∥ < 1›
by blast
define y where ‹y = x /⇩R r›
have ‹x = r * (inverse r * x)›
using ‹x = r *⇩R norm (f t)› by auto
hence ‹x - (r * (inverse r * x)) ≤ 0›
by linarith
hence ‹x ≤ r * (x /⇩R r)›
by auto
have ‹y ∈ (λk. ∥f *⇩v k∥)  ball 0 1›
unfolding y_def by (smt ‹x ∈ (λt. r *⇩R ∥f *⇩v t∥)  ball 0 1› assms image_iff
inverse_inverse_eq pos_le_divideR_eq positive_imp_inverse_positive)
moreover have ‹x ≤ r * y›
using ‹x ≤ r * (x /⇩R r)› y_def by blast
ultimately have y_norm_f: ‹y ∈ (λt. ∥f *⇩v t∥)  ball 0 1 ∧ x ≤ r * y›
by blast
have ‹(λt. ∥f *⇩v t∥)  ball 0 1 ≠ {}›
by simp
moreover have ‹bdd_above ((λt. ∥f *⇩v t∥)  ball 0 1)›
by (simp add: bounded_linear_image blinfun.bounded_linear_right bounded_imp_bdd_above
bounded_norm_comp)
moreover have ‹∃ y. y ∈ (λt. ∥f *⇩v t∥)  ball 0 1 ∧ x ≤ r * y›
using y_norm_f by blast
ultimately show ?thesis
by (smt ‹0 < r› cSup_upper ordered_comm_semiring_class.comm_mult_left_mono)
qed
have s3: ‹(⋀x. x ∈ (λt. r * ∥f *⇩v t∥)  ball 0 1 ⟹ x ≤ y) ⟹
r * Sup ((λt. ∥f *⇩v t∥)  ball 0 1) ≤ y› for y
proof-
assume ‹⋀x. x ∈ (λt. r * ∥f *⇩v t∥)  ball 0 1 ⟹ x ≤ y›
have x_leq: ‹x ∈ (λt. ∥f *⇩v t∥)  ball 0 1 ⟹ x ≤ y / r› for x
proof-
assume ‹x ∈ (λt. ∥f *⇩v t∥)  ball 0 1›
then obtain t where ‹t ∈ ball (0::'a) 1› and ‹x = ∥f *⇩v t∥›
by auto
define x' where ‹x' = r *⇩R x›
have ‹x' = r * ∥f *⇩v t∥›
by (simp add: ‹x = ∥f *⇩v t∥› x'_def)
hence ‹x' ∈ (λt. r * ∥f *⇩v t∥)  ball 0 1›
using ‹t ∈ ball (0::'a) 1› by auto
hence ‹x' ≤ y›
using ‹⋀x. x ∈ (λt. r * ∥f *⇩v t∥)  ball 0 1 ⟹ x ≤ y› by blast
thus ‹x ≤ y / r›
unfolding x'_def using ‹r > 0› by (simp add: mult.commute pos_le_divide_eq)
qed
have ‹(λt. ∥f *⇩v t∥)  ball 0 1 ≠ {}›
by simp
moreover have ‹bdd_above ((λt. ∥f *⇩v t∥)  ball 0 1)›
by (simp add: bounded_linear_image blinfun.bounded_linear_right bounded_imp_bdd_above
bounded_norm_comp)
ultimately have ‹Sup ((λt. ∥f *⇩v t∥)  ball 0 1) ≤ y/r›
using x_leq by (simp add: ‹bdd_above ((λt. ∥f *⇩v t∥)  ball 0 1)› cSup_least)
thus ?thesis using ‹r > 0›
by (smt divide_strict_right_mono nonzero_mult_div_cancel_left)
qed
have norm_scaleR: ‹norm ∘ ((*⇩R) r) = ((*⇩R) ¦r¦) ∘ (norm::'a ⇒ real)›
by auto
have f_x1: ‹f (r *⇩R x) = r *⇩R f x› for x
by (simp add: blinfun.scaleR_right)
have ‹ball (0::'a) r = ((*⇩R) r)  (ball 0 1)›
by (smt assms ball_scale nonzero_mult_div_cancel_left right_inverse_eq scale_zero_right)
hence ‹Sup ((λt. ∥f *⇩v t∥)  (ball 0 r)) = Sup ((λt. ∥f *⇩v t∥)  (((*⇩R) r)  (ball 0 1)))›
by simp
also have ‹… = Sup (((λt. ∥f *⇩v t∥) ∘ ((*⇩R) r))  (ball 0 1))›
using Sup.SUP_image by auto
also have ‹… = Sup ((λt. ∥f *⇩v (r *⇩R t)∥)  (ball 0 1))›
using f_x1 by (simp add: comp_assoc)
also have ‹… = Sup ((λt. ¦r¦ *⇩R ∥f *⇩v t∥)  (ball 0 1))›
using norm_scaleR f_x1 by auto
also have ‹… = Sup ((λt. r *⇩R ∥f *⇩v t∥)  (ball 0 1))›
using ‹r > 0› by auto
also have ‹… = r * Sup ((λt. ∥f *⇩v t∥)  (ball 0 1))›
apply (rule cSup_eq_non_empty) apply simp using s2 apply auto using s3 by auto
also have ‹… = r * ∥f∥›
using onorm_f by auto
finally have ‹Sup ((λt. ∥f *⇩v t∥)  ball 0 r) = r * ∥f∥›
by blast
thus ‹∥f∥ = Sup ((λx. ∥f *⇩v x∥)  (ball 0 r)) / r› using ‹r > 0› by simp
qed

text‹Pointwise convergence›
definition pointwise_convergent_to ::
‹( nat ⇒ ('a ⇒ 'b::topological_space) ) ⇒ ('a ⇒ 'b) ⇒ bool›
(‹((_)/ ─pointwise→ (_))› [60, 60] 60) where
‹pointwise_convergent_to x l = (∀ t::'a. (λ n. (x n) t) ⇢ l t)›

lemma linear_limit_linear:
fixes f :: ‹_ ⇒ ('a::real_vector ⇒ 'b::real_normed_vector)›
assumes  ‹⋀n. linear (f n)› and ‹f ─pointwise→ F›
shows ‹linear F›
text‹
Explanation: If a family of linear operators converges pointwise, then the limit is also a linear
operator.
›
proof
show "F (x + y) = F x + F y" for x y
proof-
have "∀a. F a = lim (λn. f n a)"
using ‹f ─pointwise→ F› unfolding pointwise_convergent_to_def by (metis (full_types) limI)
moreover have "∀f b c g. (lim (λn. g n + f n) = (b::'b) + c ∨ ¬ f ⇢ c) ∨ ¬ g ⇢ b"
by (metis (no_types) limI tendsto_add)
moreover have "⋀a. (λn. f n a) ⇢ F a"
using assms(2) pointwise_convergent_to_def by force
ultimately have
lim_sum: ‹lim (λ n. (f n) x + (f n) y) = lim (λ n. (f n) x) + lim (λ n. (f n) y)›
by metis
have ‹(f n) (x + y) = (f n) x + (f n) y› for n
using ‹⋀ n.  linear (f n)› unfolding linear_def using Real_Vector_Spaces.linear_iff assms(1)
by auto
hence ‹lim (λ n. (f n) (x + y)) = lim (λ n. (f n) x + (f n) y)›
by simp
hence ‹lim (λ n. (f n) (x + y)) = lim (λ n. (f n) x) + lim (λ n. (f n) y)›
using lim_sum by simp
moreover have ‹(λ n. (f n) (x + y)) ⇢ F (x + y)›
using ‹f ─pointwise→ F› unfolding pointwise_convergent_to_def by blast
moreover have ‹(λ n. (f n) x) ⇢ F x›
using ‹f ─pointwise→ F› unfolding pointwise_convergent_to_def by blast
moreover have ‹(λ n. (f n) y) ⇢ F y›
using ‹f ─pointwise→ F› unfolding pointwise_convergent_to_def by blast
ultimately show ?thesis
by (metis limI)
qed
show "F (r *⇩R x) = r *⇩R F x" for r and x
proof-
have ‹(f n) (r *⇩R x) = r *⇩R (f n) x› for n
using  ‹⋀ n.  linear (f n)›
by (simp add: Real_Vector_Spaces.linear_def real_vector.linear_scale)
hence ‹lim (λ n. (f n) (r *⇩R x)) = lim (λ n. r *⇩R (f n) x)›
by simp
have ‹convergent (λ n. (f n) x)›
by (metis assms(2) convergentI pointwise_convergent_to_def)
moreover have ‹isCont (λ t::'b. r *⇩R t) tt› for tt
by (simp add: bounded_linear_scaleR_right)
ultimately have ‹lim (λ n. r *⇩R ((f n) x)) =  r *⇩R lim (λ n. (f n) x)›
using ‹f ─pointwise→ F› unfolding pointwise_convergent_to_def
by (metis (mono_tags) isCont_tendsto_compose limI)
hence ‹lim (λ n.  (f n) (r *⇩R x)) = r *⇩R lim (λ n. (f n) x)›
using ‹lim (λ n. (f n) (r *⇩R x)) = lim (λ n. r *⇩R (f n) x)› by simp
moreover have ‹(λ n. (f n) x) ⇢ F x›
using ‹f ─pointwise→ F› unfolding pointwise_convergent_to_def by blast
moreover have ‹(λ n.  (f n) (r *⇩R x)) ⇢ F (r *⇩R x)›
using ‹f ─pointwise→ F› unfolding pointwise_convergent_to_def by blast
ultimately show ?thesis
by (metis limI)
qed
qed

lemma non_Cauchy_unbounded:
fixes a ::‹_ ⇒ real›
assumes ‹⋀n. a n ≥ 0› and ‹e > 0›
and ‹∀M. ∃m. ∃n. m ≥ M ∧ n ≥ M ∧ m > n ∧ sum a {Suc n..m} ≥ e›
shows ‹(λn. (sum a  {0..n})) ⇢ ∞›
text‹
Explanation: If the sequence of partial sums of nonnegative terms is not Cauchy, then it converges
to infinite.
›
proof-
define S::"ereal set" where ‹S = range (λn. sum a  {0..n})›
have ‹∃s∈S.  k*e ≤ s› for k::nat
proof(induction k)
case 0
from ‹∀M. ∃m. ∃n. m ≥ M ∧ n ≥ M ∧ m > n ∧ sum a {Suc n..m} ≥ e›
obtain m n where ‹m ≥ 0› and ‹n ≥ 0› and ‹m > n› and ‹sum a {Suc n..m} ≥ e› by blast
have ‹n < Suc n›
by simp
hence ‹{0..n} ∪ {Suc n..m} = {0..m}›
using Set_Interval.ivl_disj_un(7) ‹n < m› by auto
moreover have ‹finite {0..n}›
by simp
moreover have ‹finite {Suc n..m}›
by simp
moreover have ‹{0..n} ∩ {Suc n..m} = {}›
by simp
ultimately have ‹sum a {0..n} + sum a {Suc n..m} = sum a {0..m}›
by (metis sum.union_disjoint)
moreover have ‹sum a {Suc n..m} > 0›
using ‹e > 0› ‹sum a {Suc n..m} ≥ e› by linarith
moreover have ‹sum a {0..n} ≥ 0›
by (simp add: assms(1) sum_nonneg)
ultimately have ‹sum a {0..m} > 0›
by linarith
moreover have ‹sum a {0..m} ∈ S›
unfolding S_def by blast
ultimately have ‹∃s∈S. 0 ≤ s›
using ereal_less_eq(5) by fastforce
thus ?case
by (simp add: zero_ereal_def)
next
case (Suc k)
assume ‹∃s∈S. k*e ≤ s›
then obtain s where ‹s∈S› and ‹ereal (k * e) ≤ s›
by blast
have ‹∃N. s = sum a {0..N}›
using ‹s∈S› unfolding S_def by blast
then obtain N where ‹s = sum a {0..N}›
by blast
from ‹∀M. ∃m. ∃n. m ≥ M ∧ n ≥ M ∧ m > n ∧ sum a {Suc n..m} ≥ e›
obtain m n where ‹m ≥ Suc N› and ‹n ≥ Suc N› and ‹m > n› and ‹sum a {Suc n..m} ≥ e›
by blast
have ‹finite {Suc N..n}›
by simp
moreover have ‹finite {Suc n..m}›
by simp
moreover have ‹{Suc N..n} ∪ {Suc n..m} = {Suc N..m}›
using Set_Interval.ivl_disj_un
by (smt ‹Suc N ≤ n› ‹n < m› atLeastSucAtMost_greaterThanAtMost less_imp_le_nat)
moreover have ‹{} = {Suc N..n} ∩ {Suc n..m}›
by simp
ultimately have ‹sum a {Suc N..m} = sum a {Suc N..n} + sum a {Suc n..m}›
by (metis sum.union_disjoint)
moreover have ‹sum a {Suc N..n} ≥ 0›
using  ‹⋀n. a n ≥ 0› by (simp add: sum_nonneg)
ultimately have ‹sum a {Suc N..m} ≥ e›
using ‹e ≤ sum a {Suc n..m}› by linarith
have ‹finite {0..N}›
by simp
have ‹finite {Suc N..m}›
by simp
moreover have ‹{0..N} ∪ {Suc N..m} = {0..m}›
using Set_Interval.ivl_disj_un(7) ‹Suc N ≤ m› by auto
moreover have ‹{0..N} ∩ {Suc N..m} = {}›
by simp
ultimately have ‹sum a {0..N} + sum a {Suc N..m} =  sum a {0..m}›
by (metis ‹finite {0..N}› sum.union_disjoint)
hence ‹e + k * e ≤ sum a {0..m}›
using ‹ereal (real k * e) ≤ s› ‹s = ereal (sum a {0..N})› ‹e ≤ sum a {Suc N..m}› by auto
moreover have ‹e + k * e = (Suc k) * e›
by (simp add: semiring_normalization_rules(3))
ultimately have ‹(Suc k) * e ≤ sum a {0..m}›
by linarith
hence ‹ereal ((Suc k) * e) ≤ sum a {0..m}›
by auto
moreover have ‹sum a {0..m}∈S›
unfolding S_def by blast
ultimately show ?case by blast
qed
hence ‹∃s∈S. (real n) ≤ s› for n
by (meson assms(2) ereal_le_le ex_less_of_nat_mult less_le_not_le)
hence  ‹Sup S = ∞›
using Sup_le_iff Sup_subset_mono dual_order.strict_trans1 leD less_PInf_Ex_of_nat subsetI
by metis
hence Sup: ‹Sup ((range (λ n. (sum a  {0..n})))::ereal set) = ∞› using S_def
by blast
have ‹incseq (λn. (sum a  {..<n}))›
using ‹⋀n. a n ≥ 0› using Extended_Real.incseq_sumI by auto
hence ‹incseq (λn. (sum a  {..< Suc n}))›
by (meson incseq_Suc_iff)
hence ‹incseq (λn. (sum a  {0..n})::ereal)›
using incseq_ereal by (simp add: atLeast0AtMost lessThan_Suc_atMost)
hence ‹(λn. sum a  {0..n}) ⇢ Sup (range (λn. (sum a  {0..n})::ereal))›
using LIMSEQ_SUP by auto
thus ?thesis using Sup PInfty_neq_ereal by auto
qed

lemma sum_Cauchy_positive:
fixes a ::‹_ ⇒ real›
assumes ‹⋀n. a n ≥ 0› and ‹∃K. ∀n. (sum a  {0..n}) ≤ K›
shows ‹Cauchy (λn. sum a {0..n})›
text‹
Explanation: If a series of nonnegative reals is bounded, then the series is
Cauchy.
›
proof (unfold Cauchy_altdef2, rule, rule)
fix e::real
assume ‹e>0›
have ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ sum a {Suc n..m} < e›
proof(rule classical)
assume ‹¬(∃M. ∀m≥M. ∀n≥M. m > n ⟶ sum a {Suc n..m} < e)›
hence ‹∀M. ∃m. ∃n. m ≥ M ∧ n ≥ M ∧ m > n ∧ ¬(sum a {Suc n..m} < e)›
by blast
hence ‹∀M. ∃m. ∃n. m ≥ M ∧ n ≥ M ∧ m > n ∧ sum a {Suc n..m} ≥ e›
by fastforce
hence ‹(λn. (sum a  {0..n}) ) ⇢ ∞›
using non_Cauchy_unbounded ‹0 < e› assms(1) by blast
from  ‹∃K. ∀n. sum a  {0..n} ≤ K›
obtain K where  ‹∀n. sum a {0..n} ≤ K›
by blast
from  ‹(λn. sum a {0..n})  ⇢ ∞›
have ‹∀B. ∃N. ∀n≥N. (λ n. (sum a  {0..n}) ) n ≥ B›
using Lim_PInfty by simp
hence  ‹∃n. (sum a {0..n}) ≥ K+1›
using ereal_less_eq(3) by blast
thus ?thesis using  ‹∀n. (sum a  {0..n}) ≤ K› by smt
qed
have ‹sum a {Suc n..m} = sum a {0..m} - sum a {0..n}›
if "m > n" for m n
apply (simp add: that atLeast0AtMost) using sum_up_index_split
by (smt less_imp_add_positive that)
hence ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ sum a {0..m} - sum a {0..n} < e›
using ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ sum a {Suc n..m} < e› by smt
from ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ sum a {0..m} - sum a {0..n} < e›
obtain M where ‹∀m≥M. ∀n≥M. m > n ⟶ sum a {0..m} - sum a {0..n} < e›
by blast
moreover have ‹m > n ⟹ sum a {0..m} ≥ sum a {0..n}› for m n
using ‹⋀ n. a n ≥ 0› by (simp add: sum_mono2)
ultimately have ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ ¦sum a {0..m} - sum a {0..n}¦ < e›
by auto
hence ‹∃M. ∀m≥M. ∀n≥M. m ≥ n ⟶ ¦sum a {0..m} - sum a {0..n}¦ < e›
by (metis ‹0 < e› abs_zero cancel_comm_monoid_add_class.diff_cancel diff_is_0_eq'
less_irrefl_nat linorder_neqE_nat zero_less_diff)
hence ‹∃M. ∀m≥M. ∀n≥M. ¦sum a {0..m} - sum a {0..n}¦ < e›
by (metis abs_minus_commute nat_le_linear)
hence ‹∃M. ∀m≥M. ∀n≥M. dist (sum a {0..m}) (sum a {0..n}) < e›
by (simp add: dist_real_def)
hence ‹∃M. ∀m≥M. ∀n≥M. dist (sum a {0..m}) (sum a {0..n}) < e› by blast
thus ‹∃N. ∀n≥N. dist (sum a {0..n}) (sum a {0..N}) < e› by auto
qed

lemma convergent_series_Cauchy:
fixes a::‹nat ⇒ real› and φ::‹nat ⇒ 'a::metric_space›
assumes ‹∃M. ∀n. sum a {0..n} ≤ M› and ‹⋀n. dist (φ (Suc n)) (φ n) ≤ a n›
shows ‹Cauchy φ›
text‹
Explanation: Let \<^term>‹a› be a real-valued sequence and let \<^term>‹φ› be sequence in a metric space.
If the partial sums of \<^term>‹a› are uniformly bounded and the distance between consecutive terms of \<^term>‹φ›
are bounded by the sequence \<^term>‹a›, then \<^term>‹φ› is Cauchy.›
proof (unfold Cauchy_altdef2, rule, rule)
fix e::real
assume ‹e > 0›
have ‹⋀k. a k ≥ 0›
using ‹⋀n. dist (φ (Suc n)) (φ n) ≤ a n› dual_order.trans zero_le_dist by blast
hence ‹Cauchy (λk. sum a {0..k})›
using  ‹∃M. ∀n. sum a {0..n} ≤ M› sum_Cauchy_positive by blast
hence ‹∃M. ∀m≥M. ∀n≥M. dist (sum a {0..m}) (sum a {0..n}) < e›
unfolding Cauchy_def using ‹e > 0› by blast
hence ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ dist (sum a {0..m}) (sum a {0..n}) < e›
by blast
have ‹dist (sum a {0..m}) (sum a {0..n}) = sum a {Suc n..m}› if ‹n<m› for m n
proof -
have ‹n < Suc n›
by simp
have ‹finite {0..n}›
by simp
moreover have ‹finite {Suc n..m}›
by simp
moreover have ‹{0..n} ∪ {Suc n..m} = {0..m}›
using ‹n < Suc n› ‹n < m› by auto
moreover have  ‹{0..n} ∩ {Suc n..m} = {}›
by simp
ultimately have sum_plus: ‹(sum a {0..n}) + sum a {Suc n..m} = (sum a {0..m})›
by (metis sum.union_disjoint)
have ‹dist (sum a {0..m}) (sum a {0..n}) = ¦(sum a {0..m}) - (sum a {0..n})¦›
using dist_real_def by blast
moreover have ‹(sum a {0..m}) - (sum a {0..n}) = sum a {Suc n..m}›
using sum_plus by linarith
ultimately show ?thesis
by (simp add: ‹⋀k. 0 ≤ a k› sum_nonneg)
qed
hence sum_a: ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ sum a {Suc n..m} < e›
by (metis ‹∃M. ∀m≥M. ∀n≥M. dist (sum a {0..m}) (sum a {0..n}) < e›)
obtain M where ‹∀m≥M. ∀n≥M. m > n ⟶ sum a {Suc n..m} < e›
using sum_a ‹e > 0› by blast
hence  ‹∀m. ∀n. Suc m ≥ Suc M ∧ Suc n ≥ Suc M ∧ Suc m > Suc n ⟶ sum a {Suc n..Suc m - 1} < e›
by simp
hence  ‹∀m≥1. ∀n≥1. m ≥ Suc M ∧ n ≥ Suc M ∧ m > n ⟶ sum a {n..m - 1} < e›
by (metis Suc_le_D)
hence sum_a2: ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ sum a {n..m-1} < e›
have ‹dist (φ (n+p+1)) (φ n) ≤ sum a {n..n+p}› for p n :: nat
proof(induction p)
case 0 thus ?case  by (simp add: assms(2))
next
case (Suc p) thus ?case
by (smt Suc_eq_plus1 add_Suc_right add_less_same_cancel1 assms(2) dist_self dist_triangle2
gr_implies_not0 sum.cl_ivl_Suc)
qed
hence ‹m > n ⟹ dist (φ m) (φ n) ≤ sum a {n..m-1}› for m n :: nat
by (metis Suc_eq_plus1 Suc_le_D diff_Suc_1  gr0_implies_Suc less_eq_Suc_le less_imp_Suc_add
zero_less_Suc)
hence ‹∃M. ∀m≥M. ∀n≥M. m > n ⟶ dist (φ m) (φ n) < e›
using sum_a2 ‹e > 0› by smt
thus "∃N. ∀n≥N. dist (φ n) (φ N) < e"
using ‹0 < e› by fastforce
qed

unbundle notation_blinfun_apply

unbundle no_notation_norm

end


# Theory Banach_Steinhaus

(*
File:   Banach_Steinhaus.thy
Author: Dominique Unruh, University of Tartu
Author: Jose Manuel Rodriguez Caballero, University of Tartu
*)
section ‹Banach-Steinhaus theorem›

theory Banach_Steinhaus
imports Banach_Steinhaus_Missing
begin

text ‹
We formalize Banach-Steinhaus theorem as theorem @{text banach_steinhaus}. This theorem was
originally proved in Banach-Steinhaus's paper~\cite{banach1927principe}. For the proof, we follow
Sokal's approach~\cite{sokal2011really}. Furthermore, we prove as a corollary a result about
pointwise convergent sequences of bounded operators whose domain is a Banach space.
›

subsection ‹Preliminaries for Sokal's proof of Banach-Steinhaus theorem›

lemma linear_plus_norm:
includes notation_norm
assumes ‹linear f›
shows ‹∥f ξ∥ ≤ max ∥f (x + ξ)∥ ∥f (x - ξ)∥›
text ‹
Explanation: For arbitrary \<^term>‹x› and a linear operator \<^term>‹f›,
\<^term>‹norm (f ξ)› is upper bounded by the maximum of the norms
of the shifts of \<^term>‹f› (i.e., \<^term>‹f (x + ξ)› and \<^term>‹f (x - ξ)›).
›
proof-
have ‹norm (f ξ) = norm ( (inverse (of_nat 2)) *⇩R (f (x + ξ) - f (x - ξ)) )›
also have ‹… = inverse (of_nat 2) * norm (f (x + ξ) - f (x - ξ))›
using Real_Vector_Spaces.real_normed_vector_class.norm_scaleR by simp
also have ‹… ≤ inverse (of_nat 2) * (norm (f (x + ξ)) + norm (f (x - ξ)))›
by (simp add: norm_triangle_ineq4)
also have ‹… ≤  max (norm (f (x + ξ))) (norm (f (x - ξ)))›
by auto
finally show ?thesis by blast
qed

lemma onorm_Sup_on_ball:
includes notation_norm
assumes ‹r > 0›
shows "∥f∥ ≤ Sup ( (λx. ∥f *⇩v x∥)  (ball x r) ) / r"
text ‹
Explanation: Let \<^term>‹f› be a bounded operator and let \<^term>‹x› be a point. For any \<^term>‹r > 0›,
the operator norm of \<^term>‹f› is bounded above by the supremum of $f$ applied to the open ball of
radius \<^term>‹r› around \<^term>‹x›, divided by \<^term>‹r›.
›
proof-
have bdd_above_3: ‹bdd_above ((λx. ∥f *⇩v x∥)  (ball 0 r))›
proof -
obtain M where ‹⋀ ξ.  ∥f *⇩v ξ∥ ≤ M * norm ξ› and ‹M ≥ 0›
using norm_blinfun norm_ge_zero by blast
hence ‹⋀ ξ. ξ ∈ ball 0 r ⟹ ∥f *⇩v ξ∥ ≤ M * r›
using ‹r > 0› by (smt mem_ball_0 mult_left_mono)
thus ?thesis by (meson bdd_aboveI2)
qed
have bdd_above_2: ‹bdd_above ((λ ξ. ∥f *⇩v (x + ξ)∥)  (ball 0 r))›
proof-
have ‹bdd_above ((λ ξ. ∥f *⇩v x∥)  (ball 0 r))›
by auto
moreover have ‹bdd_above ((λ ξ. ∥f *⇩v ξ∥)  (ball 0 r))›
using bdd_above_3 by blast
ultimately have ‹bdd_above ((λ ξ. ∥f *⇩v x∥ + ∥f *⇩v ξ∥)  (ball 0 r))›
by (rule bdd_above_plus)
then obtain M where ‹⋀ ξ. ξ ∈ ball 0 r ⟹ ∥f *⇩v x∥ + ∥f *⇩v ξ∥ ≤ M›
unfolding bdd_above_def by (meson image_eqI)
moreover have ‹∥f *⇩v (x + ξ)∥ ≤ ∥f *⇩v x∥ + ∥f *⇩v ξ∥› for ξ
ultimately have ‹⋀ ξ. ξ ∈ ball 0 r ⟹ ∥f *⇩v (x + ξ)∥ ≤ M›
thus ?thesis by (meson bdd_aboveI2)
qed
have bdd_above_4: ‹bdd_above ((λ ξ. ∥f *⇩v (x - ξ)∥)  (ball 0 r))›
proof-
obtain K where K_def: ‹⋀ ξ. ξ ∈ ball 0 r ⟹ ∥f *⇩v (x + ξ)∥ ≤ K›
using  ‹bdd_above ((λ ξ. norm (f (x + ξ)))  (ball 0 r))› unfolding bdd_above_def
by (meson image_eqI)
have ‹ξ ∈ ball (0::'a) r ⟹ -ξ ∈ ball 0 r› for ξ
by auto
thus ?thesis by (metis K_def ab_group_add_class.ab_diff_conv_add_uminus bdd_aboveI2)
qed
have bdd_above_1: ‹bdd_above ((λ ξ. max ∥f *⇩v (x + ξ)∥  ∥f *⇩v (x - ξ)∥)  (ball 0 r))›
proof-
have ‹bdd_above ((λ ξ. ∥f *⇩v (x + ξ)∥)  (ball 0 r))›
using bdd_above_2 by blast
moreover have ‹bdd_above ((λ ξ.  ∥f *⇩v (x - ξ)∥)  (ball 0 r))›
using bdd_above_4 by blast
ultimately show ?thesis
unfolding max_def apply auto apply (meson bdd_above_Int1 bdd_above_mono image_Int_subset)
by (meson bdd_above_Int1 bdd_above_mono image_Int_subset)
qed
have bdd_above_6: ‹bdd_above ((λt. ∥f *⇩v t∥)  ball x r)›
proof-
have ‹bounded (ball x r)›
by simp
hence ‹bounded ((λt. ∥f *⇩v t∥)  ball x r)›
by (metis (no_types) add.left_neutral bdd_above_2 bdd_above_norm bounded_norm_comp
thus ?thesis
by (simp add: bounded_imp_bdd_above)
qed
have norm_1: ‹(λξ. ∥f *⇩v (x + ξ)∥)  ball 0 r = (λt. ∥f *⇩v t∥)  ball x r›
by (metis add.right_neutral ball_translation image_image)
have bdd_above_5: ‹bdd_above ((λξ. norm (f (x + ξ)))  ball 0 r)›
by (simp add: bdd_above_2)
have norm_2: ‹∥ξ∥ < r ⟹ ∥f *⇩v (x - ξ)∥ ∈ (λξ. ∥f *⇩v (x + ξ)∥)  ball 0 r› for ξ
proof-
assume ‹∥ξ∥ < r›
hence ‹ξ ∈ ball (0::'a) r›
by auto
hence ‹-ξ ∈ ball (0::'a) r›
by auto
thus ?thesis
qed
have norm_2': ‹∥ξ∥ < r ⟹ ∥f *⇩v (x + ξ)∥ ∈ (λξ. ∥f *⇩v (x - ξ)∥)  ball 0 r› for ξ
proof-
assume ‹norm ξ < r›
hence ‹ξ ∈ ball (0::'a) r›
by auto
hence ‹-ξ ∈ ball (0::'a) r›
by auto
thus ?thesis
by (metis (no_types, lifting) diff_minus_eq_add image_iff)
qed
have bdd_above_6: ‹bdd_above ((λξ. ∥f *⇩v (x - ξ)∥)  ball 0 r)›
by (simp add: bdd_above_4)
have Sup_2: ‹(SUP ξ∈ball 0 r. max ∥f *⇩v (x + ξ)∥ ∥f *⇩v (x - ξ)∥) =
max (SUP ξ∈ball 0 r. ∥f *⇩v (x + ξ)∥) (SUP ξ∈ball 0 r. ∥f *⇩v (x - ξ)∥)›
proof-
have ‹ball (0::'a) r ≠ {}›
using ‹r > 0› by auto
moreover have ‹bdd_above ((λξ. ∥f *⇩v (x + ξ)∥)  ball 0 r)›
using bdd_above_5 by blast
moreover have ‹bdd_above ((λξ. ∥f *⇩v (x - ξ)∥)  ball 0 r)›
using bdd_above_6 by blast
ultimately show ?thesis
using max_Sup
by (metis (mono_tags, lifting) Banach_Steinhaus_Missing.pointwise_max_def image_cong)
qed
have Sup_3': ‹∥ξ∥ < r ⟹ ∥f *⇩v (x + ξ)∥ ∈ (λξ. ∥f *⇩v (x - ξ)∥)  ball 0 r› for ξ::'a
by (simp add: norm_2')
have Sup_3'': ‹∥ξ∥ < r ⟹ ∥f *⇩v (x - ξ)∥ ∈ (λξ. ∥f *⇩v (x + ξ)∥)  ball 0 r› for ξ::'a
by (simp add: norm_2)
have Sup_3: ‹max (SUP ξ∈ball 0 r. ∥f *⇩v (x + ξ)∥) (SUP ξ∈ball 0 r.  ∥f *⇩v (x - ξ)∥) =
(SUP ξ∈ball 0 r. ∥f *⇩v (x + ξ)∥)›
proof-
have ‹(λξ. ∥f *⇩v (x + ξ)∥)  (ball 0 r) = (λξ. ∥f *⇩v (x - ξ)∥)  (ball 0 r)›
apply auto using Sup_3' apply auto using Sup_3'' by blast
hence ‹Sup ((λξ. ∥f *⇩v (x + ξ)∥)  (ball 0 r))=Sup ((λξ. ∥f *⇩v (x - ξ)∥)  (ball 0 r))›
by simp
thus ?thesis by simp
qed
have Sup_1: ‹Sup ((λt. ∥f *⇩v t∥)  (ball 0 r)) ≤ Sup ( (λξ. ∥f *⇩v ξ∥)  (ball x r) )›
proof-
have ‹(λt. ∥f *⇩v t∥) ξ ≤ max ∥f *⇩v (x + ξ)∥ ∥f *⇩v (x - ξ)∥› for ξ
apply(rule linear_plus_norm) apply (rule bounded_linear.linear)
by (simp add: blinfun.bounded_linear_right)
moreover have ‹bdd_above ((λ ξ. max ∥f *⇩v (x + ξ)∥  ∥f *⇩v (x - ξ)∥)  (ball 0 r))›
using bdd_above_1 by blast
moreover have ‹ball (0::'a) r ≠ {}›
using ‹r > 0› by auto
ultimately have ‹Sup ((λt. ∥f *⇩v t∥)  (ball 0 r)) ≤
Sup ((λξ. max ∥f *⇩v (x + ξ)∥ ∥f *⇩v (x - ξ)∥)  (ball 0 r))›
using cSUP_mono by smt
also have ‹… = max (Sup ((λξ.  ∥f *⇩v (x + ξ)∥)  (ball 0 r)))
(Sup ((λξ. ∥f *⇩v (x - ξ)∥)  (ball 0 r)))›
using Sup_2 by blast
also have ‹… = Sup ((λξ. ∥f *⇩v (x + ξ)∥)  (ball 0 r))›
using Sup_3 by blast
also have ‹… = Sup ((λξ. ∥f *⇩v ξ∥)  (ball x r))›
by (metis  add.right_neutral ball_translation image_image)
finally show ?thesis by blast
qed
have ‹∥f∥ = (SUP x∈ball 0 r. ∥f *⇩v x∥) / r›
using ‹0 < r› onorm_r by blast
moreover have ‹Sup ((λt. ∥f *⇩v t∥)  (ball 0 r)) / r ≤ Sup ((λξ. ∥f *⇩v ξ∥)  (ball x r)) / r›
using Sup_1 ‹0 < r› divide_right_mono by fastforce
ultimately have ‹∥f∥ ≤ Sup ((λt. ∥f *⇩v t∥)  ball x r) / r›
by simp
thus ?thesis by simp
qed

lemma onorm_Sup_on_ball':
includes notation_norm
assumes ‹r > 0› and ‹τ < 1›
shows ‹∃ξ∈ball x r.  τ * r * ∥f∥ ≤ ∥f *⇩v ξ∥›
text ‹
In the proof of Banach-Steinhaus theorem, we will use this variation of the
lemma @{text onorm_Sup_on_ball}.

Explanation: Let \<^term>‹f› be a bounded operator, let \<^term>‹x› be a point and let \<^term>‹r› be a
positive real number. For any real number \<^term>‹τ < 1›, there is a point \<^term>‹ξ› in the open ball
of radius \<^term>‹r› around \<^term>‹x› such that \<^term>‹τ * r * ∥f∥ ≤ ∥f *⇩v ξ∥›.
›
proof(cases  ‹f = 0›)
case True
thus ?thesis by (metis assms(1) centre_in_ball mult_zero_right norm_zero order_refl
zero_blinfun.rep_eq)
next
case False
have bdd_above_1: ‹bdd_above ((λt. ∥(*⇩v) f t∥)  ball x r)› for f::‹'a ⇒⇩L 'b›
using assms(1) bounded_linear_image by (simp add: bounded_linear_image
blinfun.bounded_linear_right bounded_imp_bdd_above bounded_norm_comp)
have  ‹norm f > 0›
using ‹f ≠ 0› by auto
have ‹norm f ≤  Sup ( (λξ.  ∥(*⇩v) f ξ∥)  (ball x r) ) / r›
using ‹r > 0› by (simp add: onorm_Sup_on_ball)
hence ‹r * norm f ≤  Sup ( (λξ.  ∥(*⇩v) f ξ∥)  (ball x r) )›
using ‹0 < r› by (smt divide_strict_right_mono nonzero_mult_div_cancel_left)
moreover have ‹τ * r * norm f < r * norm f›
using  ‹τ < 1› using ‹0 < norm f› ‹0 < r› by auto
ultimately have ‹τ * r * norm f < Sup ( (norm ∘ ((*⇩v) f))  (ball x r) )›
by simp
moreover have ‹(norm ∘ ( (*⇩v) f))  (ball x r) ≠ {}›
using ‹0 < r› by auto
moreover have ‹bdd_above ((norm ∘ ( (*⇩v) f))  (ball x r))›
using bdd_above_1 apply transfer by simp
ultimately have ‹∃t ∈ (norm ∘ ( (*⇩v) f))  (ball x r). τ * r * norm f < t›
by (simp add: less_cSup_iff)
thus ?thesis by (smt comp_def image_iff)
qed

subsection ‹Banach-Steinhaus theorem›

theorem banach_steinhaus:
fixes f::‹'c ⇒ ('a::banach ⇒⇩L 'b::real_normed_vector)›
assumes ‹⋀x. bounded (range (λn. (f n) *⇩v x))›
shows  ‹bounded (range f)›
text‹
This is Banach-Steinhaus Theorem.

Explanation: If a family of bounded operators on a Banach space
is pointwise bounded, then it is uniformly bounded.
›
proof(rule classical)
assume ‹¬(bounded (range f))›
have sum_1: ‹∃K. ∀n. sum (λk. inverse (real_of_nat 3^k)) {0..n} ≤ K›
proof-
have ‹summable (λn. inverse ((3::real) ^ n))›
by (simp flip: power_inverse)
hence ‹bounded (range (λn. sum (λ k. inverse (real 3 ^ k)) {0..<n}))›
using summable_imp_sums_bounded[where f = "(λn. inverse (real_of_nat 3^n))"]
lessThan_atLeast0 by auto
hence ‹∃M. ∀h∈(range (λn. sum (λ k. inverse (real 3 ^ k)) {0..<n})). norm h ≤ M›
using bounded_iff by blast
then obtain M where ‹h∈range (λn. sum (λ k. inverse (real 3 ^ k)) {0..<n}) ⟹ norm h ≤ M›
for h
by blast
have sum_2: ‹sum (λk. inverse (real_of_nat 3^k)) {0..n} ≤ M› for n
proof-
have  ‹norm (sum (λ k. inverse (real 3 ^ k)) {0..< Suc n}) ≤ M›
using ‹⋀h. h∈(range (λn. sum (λ k. inverse (real 3 ^ k)) {0..<n})) ⟹ norm h ≤ M›
by blast
hence  ‹norm (sum (λ k. inverse (real 3 ^ k)) {0..n}) ≤ M›
by (simp add: atLeastLessThanSuc_atLeastAtMost)
hence  ‹(sum (λ k. inverse (real 3 ^ k)) {0..n}) ≤ M›
by auto
thus ?thesis  by blast
qed
have ‹sum (λk. inverse (real_of_nat 3^k)) {0..n} ≤ M› for n
using sum_2 by blast
thus ?thesis  by blast
qed
have ‹of_rat 2/3 < (1::real)›
by auto
hence ‹∀g::'a ⇒⇩L 'b. ∀x. ∀r. ∃ξ. g ≠ 0 ∧ r > 0
⟶ (ξ∈ball x r ∧ (of_rat 2/3) * r * norm g ≤ norm ((*⇩v) g ξ))›
using onorm_Sup_on_ball' by blast
hence ‹∃ξ. ∀g::'a ⇒⇩L 'b. ∀x. ∀r. g ≠ 0 ∧ r > 0
⟶ ((ξ g x r)∈ball x r ∧ (of_rat 2/3) * r * norm g ≤ norm ((*⇩v) g (ξ g x r)))›
by metis
then obtain ξ where f1: ‹⟦g ≠ 0; r > 0⟧ ⟹
ξ g x r ∈ ball x r ∧  (of_rat 2/3) * r * norm g ≤ norm ((*⇩v) g (ξ g x r))›
for g::‹'a ⇒⇩L 'b› and x and r
by blast
have ‹∀n. ∃k. norm (f k) ≥ 4^n›
using ‹¬(bounded (range f))› by (metis (mono_tags, hide_lams) boundedI image_iff linear)
hence  ‹∃k. ∀n. norm (f (k n)) ≥ 4^n›
by metis
hence  ‹∃k. ∀n. norm ((f ∘ k) n) ≥ 4^n›
by simp
then obtain k where ‹norm ((f ∘ k) n) ≥ 4^n› for n
by blast
define T where ‹T = f ∘ k›
have ‹T n ∈ range f› for n
unfolding T_def by simp
have ‹norm (T n) ≥ of_nat (4^n)› for n
unfolding T_def using ‹⋀ n. norm ((f ∘ k) n) ≥ 4^n› by auto
hence ‹T n ≠ 0› for n
by (smt T_def ‹⋀n. 4 ^ n ≤ norm ((f ∘ k) n)› norm_zero power_not_zero zero_le_power)
have ‹inverse (of_nat 3^n) > (0::real)› for n
by auto
define y::‹nat ⇒ 'a› where ‹y = rec_nat 0 (λn x. ξ (T n) x (inverse (of_nat 3^n)))›
have ‹y (Suc n) ∈ ball (y n) (inverse (of_nat 3^n))› for n
using f1 ‹⋀ n. T n ≠ 0› ‹⋀ n. inverse (of_nat 3^n) > 0› unfolding y_def by auto
hence ‹norm (y (Suc n) - y n) ≤ inverse (of_nat 3^n)› for n
unfolding ball_def apply auto using dist_norm by (smt norm_minus_commute)
moreover have ‹∃K. ∀n. sum (λk. inverse (real_of_nat 3^k)) {0..n} ≤ K›
using sum_1 by blast
moreover have ‹Cauchy y›
using convergent_series_Cauchy[where a = "λn. inverse (of_nat 3^n)" and φ = y] dist_norm
by (metis calculation(1) calculation(2))
hence ‹∃ x. y ⇢ x›
by (simp add: convergent_eq_Cauchy)
then obtain x where ‹y ⇢ x›
by blast
have norm_2: ‹norm (x - y (Suc n)) ≤ (inverse (of_nat 2))*(inverse (of_nat 3^n))› for n
proof-
have ‹inverse (real_of_nat 3) < 1›
by simp
moreover have ‹y 0 = 0›
using y_def by auto
ultimately have ‹norm (x - y (Suc n))
≤ (inverse (of_nat 3)) * inverse (1 - (inverse (of_nat 3))) * ((inverse (of_nat 3)) ^ n)›
using bound_Cauchy_to_lim[where c = "inverse (of_nat 3)" and y = y and x = x]
power_inverse semiring_norm(77)  ‹y ⇢ x›
‹⋀ n. norm (y (Suc n) - y n) ≤ inverse (of_nat 3^n)› by (metis divide_inverse)
moreover have ‹inverse (real_of_nat 3) * inverse (1 - (inverse (of_nat 3)))
= inverse (of_nat 2)›
by auto
ultimately show ?thesis
by (metis power_inverse)
qed
have ‹norm (x - y (Suc n)) ≤ (inverse (of_nat 2))*(inverse (of_nat 3^n))› for n
using norm_2 by blast
have ‹∃ M. ∀ n. norm ((*⇩v) (T n) x) ≤ M›
unfolding T_def apply auto
by (metis ‹⋀x. bounded (range (λn. (*⇩v) (f n) x))› bounded_iff rangeI)
then obtain M where ‹norm ((*⇩v) (T n) x) ≤ M› for n
by blast
have norm_1: ‹norm (T n) * norm (y (Suc n) - x) + norm ((*⇩v) (T n) x)
≤ inverse (real 2) * inverse (real 3 ^ n) * norm (T n) + norm ((*⇩v) (T n) x)› for n
proof-
have ‹norm (y (Suc n) - x) ≤ (inverse (of_nat 2))*(inverse (of_nat 3^n))›
using ‹norm (x - y (Suc n)) ≤ (inverse (of_nat 2))*(inverse (of_nat 3^n))›
by (simp add: norm_minus_commute)
moreover have ‹norm (T n) ≥ 0›
by auto
ultimately have ‹norm (T n) * norm (y (Suc n) - x)
≤ (inverse (of_nat 2))*(inverse (of_nat 3^n))*norm (T n)›
by (simp add: ‹⋀n. T n ≠ 0›)
thus ?thesis by simp
qed
have inverse_2: ‹(inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)
≤ norm ((*⇩v) (T n) x)› for n
proof-
have ‹(of_rat 2/3)*(inverse (of_nat 3^n))*norm (T n) ≤ norm ((*⇩v) (T n) (y (Suc n)))›
using f1 ‹⋀ n. T n ≠ 0› ‹⋀ n. inverse (of_nat 3^n) > 0› unfolding y_def by auto
also have ‹… = norm ((*⇩v) (T n) ((y (Suc n) - x) + x))›
by auto
also have ‹… = norm ((*⇩v) (T n) (y (Suc n) - x) + (*⇩v) (T n) x)›
apply transfer apply auto by (metis diff_add_cancel linear_simps(1))
also have ‹… ≤ norm ((*⇩v) (T n) (y (Suc n) - x)) + norm ((*⇩v) (T n) x)›
by (simp add: norm_triangle_ineq)
also have ‹… ≤ norm (T n) * norm (y (Suc n) - x) + norm ((*⇩v) (T n) x)›
apply transfer apply auto using onorm by auto
also have ‹… ≤ (inverse (of_nat 2))*(inverse (of_nat 3^n))*norm (T n)
+ norm ((*⇩v) (T n) x)›
using norm_1 by blast
finally have ‹(of_rat 2/3) * inverse (real 3 ^ n) * norm (T n)
≤ inverse (real 2) * inverse (real 3 ^ n) * norm (T n)
+ norm ((*⇩v) (T n) x)›
by blast
hence ‹(of_rat 2/3) * inverse (real 3 ^ n) * norm (T n)
- inverse (real 2) * inverse (real 3 ^ n) * norm (T n) ≤ norm ((*⇩v) (T n) x)›
by linarith
moreover have ‹(of_rat 2/3) * inverse (real 3 ^ n) * norm (T n)
- inverse (real 2) * inverse (real 3 ^ n) * norm (T n)
= (inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)›
by fastforce
ultimately show ‹(inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n) ≤ norm ((*⇩v) (T n) x)›
by linarith
qed
have inverse_3: ‹(inverse (of_nat 6)) * (of_rat (4/3)^n)
≤ (inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)› for n
proof-
have ‹of_rat (4/3)^n = inverse (real 3 ^ n) * (of_nat 4^n)›
apply auto by (metis divide_inverse_commute of_rat_divide power_divide of_rat_numeral_eq)
also have ‹… ≤  inverse (real 3 ^ n) * norm (T n)›
using ‹⋀n. norm (T n) ≥ of_nat (4^n)› by simp
finally have ‹of_rat (4/3)^n ≤ inverse (real 3 ^ n) * norm (T n)›
by blast
moreover have ‹inverse (of_nat 6) > (0::real)›
by auto
ultimately show ?thesis by auto
qed
have inverse_1: ‹(inverse (of_nat 6)) * (of_rat (4/3)^n) ≤ M› for n
proof-
have ‹(inverse (of_nat 6)) * (of_rat (4/3)^n)
≤ (inverse (of_nat 6)) * inverse (real 3 ^ n) * norm (T n)›
using inverse_3 by blast
also have ‹… ≤ norm ((*⇩v) (T n) x)›
using inverse_2 by blast
finally have ‹(inverse (of_nat 6)) * (of_rat (4/3)^n) ≤ norm ((*⇩v) (T n) x)›
by auto
thus ?thesis using ‹⋀ n. norm ((*⇩v) (T n) x) ≤ M› by smt
qed
have ‹∃n. M < (inverse (of_nat 6)) * (of_rat (4/3)^n)›
using Real.real_arch_pow by auto
moreover have ‹(inverse (of_nat 6)) * (of_rat (4/3)^n) ≤ M› for n
using inverse_1 by blast
ultimately show ?thesis by smt
qed

subsection ‹A consequence of Banach-Steinhaus theorem›

corollary bounded_linear_limit_bounded_linear:
fixes f::‹nat ⇒ ('a::banach ⇒⇩L 'b::real_normed_vector)›
assumes ‹⋀x. convergent (λn. (f n) *⇩v x)›
shows  ‹∃g. (λn. (*⇩v) (f n)) ─pointwise→ (*⇩v) g›
text‹
Explanation: If a sequence of bounded operators on a Banach space converges
pointwise, then the limit is also a bounded operator.
›
proof-
have ‹∃l. (λn. (*⇩v) (f n) x) ⇢ l› for x
by (simp add:  ‹⋀x. convergent (λn. (*⇩v) (f n) x)› convergentD)
hence ‹∃F. (λn. (*⇩v) (f n)) ─pointwise→ F›
unfolding pointwise_convergent_to_def by metis
obtain F where ‹(λn. (*⇩v) (f n)) ─pointwise→ F›
using ‹∃F. (λn. (*⇩v) (f n)) ─pointwise→ F› by auto
have ‹⋀x. (λ n. (*⇩v) (f n) x) ⇢ F x›
using ‹(λn. (*⇩v) (f n)) ─pointwise→ F› apply transfer
by (simp add: pointwise_convergent_to_def)
have ‹bounded (range f)›
using ‹⋀x. convergent (λn. (*⇩v) (f n) x)› banach_steinhaus
‹⋀x. ∃l. (λn. (*⇩v) (f n) x) ⇢ l› convergent_imp_bounded by blast
have norm_f_n: ‹∃ M. ∀ n. norm (f n) ≤ M›
unfolding bounded_def
by (meson UNIV_I ‹bounded (range f)› bounded_iff image_eqI)
have ‹isCont (λ t::'b. norm t) y› for y::'b
using Limits.isCont_norm by simp
hence ‹(λ n. norm ((*⇩v) (f n) x)) ⇢ (norm (F x))› for x
using ‹⋀ x::'a. (λ n. (*⇩v) (f n) x) ⇢ F x› by (simp add: tendsto_norm)
hence norm_f_n_x: ‹∃ M. ∀ n. norm ((*⇩v) (f n) x) ≤ M› for x
using Elementary_Metric_Spaces.convergent_imp_bounded
by (metis UNIV_I ‹⋀ x::'a. (λ n. (*⇩v) (f n) x) ⇢ F x› bounded_iff image_eqI)
have norm_f: ‹∃K. ∀n. ∀x. norm ((*⇩v) (f n) x) ≤ norm x * K›
proof-
have ‹∃ M. ∀ n. norm ((*⇩v) (f n) x) ≤ M› for x
using norm_f_n_x  ‹⋀x. (λn. (*⇩v) (f n) x) ⇢ F x› by blast
hence ‹∃ M. ∀ n. norm (f n) ≤ M›
using norm_f_n by simp
then obtain M::real where ‹∃ M. ∀ n. norm (f n) ≤ M›
by blast
have ‹∀ n. ∀x. norm ((*⇩v) (f n) x) ≤ norm x * norm (f n)›
apply transfer apply auto by (metis mult.commute onorm)
thus  ?thesis using ‹∃ M. ∀ n. norm (f n) ≤ M›
by (metis (no_types, hide_lams) dual_order.trans norm_eq_zero order_refl
mult_le_cancel_iff2 vector_space_over_itself.scale_zero_left zero_less_norm_iff)
qed
have norm_F_x: ‹∃K. ∀x. norm (F x) ≤ norm x * K›
proof-
have "∃K. ∀n. ∀x. norm ((*⇩v) (f n) x) ≤ norm x * K"
using norm_f ‹⋀x. (λn. (*⇩v) (f n) x) ⇢ F x› by auto
thus ?thesis
using  ‹⋀ x::'a. (λ n. (*⇩v) (f n)  x) ⇢ F x› apply transfer
by (metis Lim_bounded tendsto_norm)
qed
have ‹linear F›
proof(rule linear_limit_linear)
show ‹linear ((*⇩v) (f n))› for n
apply transfer apply auto by (simp add: bounded_linear.linear)
show ‹f ─pointwise→ F›
using ‹(λn. (*⇩v) (f n)) ─pointwise→ F› by auto
qed
moreover have ‹bounded_linear_axioms F›
using norm_F_x by (simp add: ‹⋀x. (λn. (*⇩v) (f n) x) ⇢ F x› bounded_linear_axioms_def)
ultimately have ‹bounded_linear F›
unfolding bounded_linear_def by blast
hence ‹∃g. (*⇩v) g = F›
using bounded_linear_Blinfun_apply by auto
thus ?thesis using ‹(λn. (*⇩v) (f n)) ─pointwise→ F› apply transfer by auto
qed

end
`