Theory Banach_Steinhaus_Missing

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

theory Banach_Steinhaus_Missing
  imports
    "HOL-Analysis.Bounded_Linear_Function"
    "HOL-Analysis.Line_Segment"

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

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 termmax 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 (verit, best) x  X y = f x imageI)
    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 termpointwise_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 termsum (λ 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 (metis dual_order.trans norm_ge_zero power_one_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_left_pos 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 divide_le_cancel by fastforce
    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 termnorm (f x) for termx such that termnorm 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 (verit, ccfv_SIG) 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)"
        by (metis mult.commute norm_blinfun norm_ge_zero)
      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 (metis (mono_tags, lifting) y = 1 cSup_upper2 mem_Collect_eq norm_1_bounded norm_ge_zero)
  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, opaque_lifting) 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 (verit, del_insts) less_cSupD 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 t: x = r *R f *v t 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 using assms t * by fastforce 
    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 (meson assms cSup_upper dual_order.trans mult_le_cancel_left_pos)
  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 (simp add: mult.commute pos_le_divide_eq)
  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 (metis Suc N  n n < m atLeastSucAtMost_greaterThanAtMost order_less_imp_le)
    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 (verit, best))
  qed
  have sum a {Suc n..m} = sum a {0..m} - sum a {0..n}
    if "m > n" for m n
    by (metis add_diff_cancel_left' atLeast0AtMost less_imp_add_positive sum_up_index_split 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 presburger
  then 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(verit, ccfv_SIG) 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