# 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.Bounded_Linear_Function"
"HOL-Analysis.Line_Segment"

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

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›
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
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})›
hence ‹∥sum (λk. y (Suc k) - y k) {Suc n .. N}∥ ≤ (sum (power c) {Suc n .. N})›
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)›
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›
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
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›
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, opaque_lifting) ‹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)∥›
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∥›
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›
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)∥›
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}›
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}›
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)∥›
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
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"
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)›
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
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›
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
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›
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
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›
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
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
```