Session Banach_Steinhaus

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 termf,termg are bounded above on a 
  set termS, then the image of their sum is bounded on termS.
›
proof-
  obtain M where  x. xS  f x  M
    using ‹bdd_above (f ` S) unfolding bdd_above_def by blast
  obtain N where  x. xS  g x  N
    using ‹bdd_above (g ` S) unfolding bdd_above_def by blast
  have  x. xS  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 termf and termg, if the supremum of termf is 
    greater-equal the supremum of termg, then the supremum of term‹max f g equals the supremum of
    termf. (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 termf and termg and a nonempty set termX, such that 
  the termf and termg are bounded above on termX, if the supremum of termf on termX is 
  lower-equal the supremum of termg on termX, then the supremum of term‹pointwise_max f g on termX
  equals the supremum of termg. 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 termX be a nonempty set. Two supremum over termX of the maximum of two 
  real-value functions is equal to the maximum of their suprema over termX, provided that the
  functions are bounded above on termX.
›
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 termx converges to terml then the sum term‹sum (λ k. x (Suc k) - x k) {n..N}
  converges to terml - x n as termN 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   
    by (simp add: add.commute)
  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
    by (simp add: add.commute)
  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 termy be a sequence converging to termx.
  If termy satisfies the inequality ∥y (Suc n) - y n∥ ≤ c ^ n› for some termc < 1 and 
  assuming termy 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 termf be a bounded linear operator. The operator norm of termf is the
  supremum of term‹norm (f x) for termx 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 
              abs_of_nonneg add_diff_cancel_left' add_eq_if cancel_comm_monoid_add_class.diff_cancel
              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 termf is term1/r of the supremum of the norm of termf *v x for
  termx in the ball of radius termr 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 sS.  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 sS. 0  s
      using ereal_less_eq(5) by fastforce    
    thus ?case
      by (simp add: zero_ereal_def)  
  next
    case (Suc k)
    assume sS. k*e  s
    then obtain s where sS and ‹ereal (k * e)  s
      by blast
    have N. s = sum a {0..N}
      using sS 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 sS. (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. mM. nM. m > n  sum a {Suc n..m} < e
  proof(rule classical)
    assume ¬(M. mM. nM. 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. nN. (λ 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. mM. nM. m > n  sum a {0..m} - sum a {0..n} < e
    using M. mM. nM. m > n  sum a {Suc n..m} < e by smt     
  from M. mM. nM. m > n  sum a {0..m} - sum a {0..n} < e
  obtain M where mM. nM. 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. mM. nM. m > n  ¦sum a {0..m} - sum a {0..n}¦ < e
    by auto
  hence M. mM. nM. 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. mM. nM. ¦sum a {0..m} - sum a {0..n}¦ < e
    by (metis abs_minus_commute nat_le_linear)
  hence M. mM. nM. dist (sum a {0..m}) (sum a {0..n}) < e
    by (simp add: dist_real_def)      
  hence M. mM. nM. dist (sum a {0..m}) (sum a {0..n}) < e by blast
  thus N. nN. 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 terma be a real-valued sequence and let termφ be sequence in a metric space.
  If the partial sums of terma are uniformly bounded and the distance between consecutive terms of termφ
  are bounded by the sequence terma, 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. mM. nM. dist (sum a {0..m}) (sum a {0..n}) < e
    unfolding Cauchy_def using e > 0 by blast
  hence M. mM. nM. 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. mM. nM. m > n  sum a {Suc n..m} < e
    by (metis M. mM. nM. dist (sum a {0..m}) (sum a {0..n}) < e) 
  obtain M where mM. nM. 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  m1. n1. m  Suc M  n  Suc M  m > n  sum a {n..m - 1} < e
    by (metis Suc_le_D)
  hence sum_a2: M. mM. nM. m > n  sum a {n..m-1} < e
    by (meson add_leE)
  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. mM. nM. m > n  dist (φ m) (φ n) < e 
    using sum_a2 e > 0 by smt
  thus "N. nN. 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 termx and a linear operator termf,
  term‹norm (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 (smt add_diff_cancel_left' assms diff_add_cancel diff_diff_add linear_diff midpoint_def 
        midpoint_plus_self of_nat_1 of_nat_add one_add_one scaleR_half_double)
  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 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 
    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 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 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, 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