Theory Banach_Steinhaus
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 norm_syntax
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 - ξ)) )›
by (metis (no_types, opaque_lifting) add.commute assms diff_diff_eq2 group_cancel.sub1
linear_cmul linear_diff of_nat_numeral real_vector_affinity_eq scaleR_2
scaleR_right_diff_distrib zero_neq_numeral)
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 norm_syntax
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 (verit) 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 ξ
by (simp add: blinfun.add_right norm_triangle_ineq)
ultimately have ‹⋀ ξ. ξ ∈ ball 0 r ⟹ ∥f *⇩v (x + ξ)∥ ≤ M›
by (simp add: blinfun.add_right norm_triangle_le)
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
image_add_ball image_image)
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
by (metis (no_types, lifting) ab_group_add_class.ab_diff_conv_add_uminus image_iff)
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 (verit))
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 norm_syntax
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 (verit) 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 (verit) 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, opaque_lifting) 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 (verit) 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 (verit) 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 (verit))
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 (verit))
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, opaque_lifting) dual_order.trans norm_eq_zero order_refl
mult_le_cancel_left_pos 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