Theory Banach_Steinhaus.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 termx and a linear operator termf,
  termnorm (f ξ) is upper bounded by the maximum of the norms
  of the shifts of termf (i.e., termf (x + ξ) and termf (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 notation_norm
  assumes r > 0
  shows "f  Sup ( (λx. f *v x) ` (ball x r) ) / r"
  text ‹
  Explanation: Let termf be a bounded operator and let termx be a point. For any termr > 0, 
  the operator norm of termf is bounded above by the supremum of $f$ applied to the open ball of 
  radius termr around termx, divided by termr.
›
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 xball 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 termf be a bounded operator, let termx be a point and let termr be a 
  positive real number. For any real number termτ < 1, there is a point termξ in the open ball 
  of radius termr around termx 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 hrange (λ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