src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy

 (*  Title:      HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
     Author:     Fabian Immler, TU München
 *)
 
-section {* Bounded Linear Function *}
+section \<open>Bounded Linear Function\<close>
 
 theory Bounded_Linear_Function
 imports
   Topology_Euclidean_Space
   Operator_Norm
 begin
 
-subsection {* Intro rules for @{term bounded_linear} *}
+subsection \<open>Intro rules for @{term bounded_linear}\<close>
 
 named_theorems bounded_linear_intros
 
 lemma onorm_inner_left:
   assumes "bounded_linear r"

       assume "norm x \<le> 1"
       have "Cauchy (\<lambda>n. X n x)"
       proof (rule CauchyI)
         fix e::real
         assume "0 < e"
-        from CauchyD[OF `Cauchy X` `0 < e`] obtain M
+        from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
           where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
           by auto
         show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m x - X n x) < e"
         proof (safe intro!: exI[where x=M])
           fix m n

           have "norm (X m x - X n x) = norm ((X m - X n) x)"
             by (simp add: blinfun.bilinear_simps)
           also have "\<dots> \<le> norm (X m - X n) * norm x"
              by (rule norm_blinfun)
           also have "\<dots> \<le> norm (X m - X n) * 1"
-            using `norm x \<le> 1` norm_ge_zero by (rule mult_left_mono)
+            using \<open>norm x \<le> 1\<close> norm_ge_zero by (rule mult_left_mono)
           also have "\<dots> = norm (X m - X n)" by simp
           also have "\<dots> < e" using le by fact
           finally show "norm (X m x - X n x) < e" .
         qed
       qed

 
   have "Cauchy (\<lambda>n. norm (X n))"
   proof (rule CauchyI)
     fix e::real
     assume "e > 0"
-    from CauchyD[OF `Cauchy X` `0 < e`] obtain M
+    from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
       where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
       by auto
     show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (norm (X m) - norm (X n)) < e"
     proof (safe intro!: exI[where x=M])
       fix m n assume mn: "m \<ge> M" "n \<ge> M"

 
   have "X \<longlonglongrightarrow> Blinfun v"
   proof (rule LIMSEQ_I)
     fix r::real assume "r > 0"
     def r' \<equiv> "r / 2"
-    have "0 < r'" "r' < r" using `r > 0` by (simp_all add: r'_def)
-    from CauchyD[OF `Cauchy X` `r' > 0`]
+    have "0 < r'" "r' < r" using \<open>r > 0\<close> by (simp_all add: r'_def)
+    from CauchyD[OF \<open>Cauchy X\<close> \<open>r' > 0\<close>]
     obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
       by metis
     show "\<exists>no. \<forall>n\<ge>no. norm (X n - Blinfun v) < r"
     proof (safe intro!: exI[where x=M])
       fix n assume n: "M \<le> n"

         qed
         have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) \<longlonglongrightarrow> norm (X n x - Blinfun v x)"
           by (auto intro!: tendsto_intros Bv)
         show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
           by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
-      qed (simp add: `0 < r'` less_imp_le)
+      qed (simp add: \<open>0 < r'\<close> less_imp_le)
       thus "norm (X n - Blinfun v) < r"
-        by (metis `r' < r` le_less_trans)
+        by (metis \<open>r' < r\<close> le_less_trans)
     qed
   qed
   thus "convergent X"
     by (rule convergentI)
 qed
 
-subsection {* On Euclidean Space *}
+subsection \<open>On Euclidean Space\<close>
 
 lemma Zfun_setsum:
   assumes "finite s"
   assumes f: "\<And>i. i \<in> s \<Longrightarrow> Zfun (f i) F"
   shows "Zfun (\<lambda>x. setsum (\<lambda>i. f i x) s) F"

 
 lemma mult_if_delta:
   "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
   by auto
 
-text {* TODO: generalize this and @{thm compact_lemma}?! *}
+text \<open>TODO: generalize this and @{thm compact_lemma}?!\<close>
 lemma compact_blinfun_lemma:
   fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   assumes "bounded (range f)"
   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
     subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"

   next
     case (insert k d)
     have k[intro]: "k \<in> Basis"
       using insert by auto
     have s': "bounded ((\<lambda>x. blinfun_apply x k) ` range f)"
-      using `bounded (range f)`
+      using \<open>bounded (range f)\<close>
       by (auto intro!: bounded_linear_image bounded_linear_intros)
     obtain l1::"'a \<Rightarrow>\<^sub>L 'b" and r1 where r1: "subseq r1"
       and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
       using insert(3) using insert(4) by auto
     have f': "\<forall>n. f (r1 n) k \<in> (\<lambda>x. blinfun_apply x k) ` range f"

     moreover
     def l \<equiv> "blinfun_of_matrix (\<lambda>i j. if j = k then l2 \<bullet> i else l1 j \<bullet> i)::'a \<Rightarrow>\<^sub>L 'b"
     {
       fix e::real
       assume "e > 0"
-      from lr1 `e > 0` have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
+      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
         by blast
-      from lr2 `e > 0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
+      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
         by (rule tendstoD)
       from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n))  i) (l1  i) < e) sequentially"
         by (rule eventually_subseq)
       have l2: "l k = l2"
         using insert.prems

   apply (subst (2) euclidean_representation[symmetric, where 'a='a])
   apply (subst (1) euclidean_representation[symmetric, where 'a='a])
   apply (simp add: blinfun.bilinear_simps)
   done
 
-text {* TODO: generalize (via @{thm compact_cball})? *}
+text \<open>TODO: generalize (via @{thm compact_cball})?\<close>
 instance blinfun :: (euclidean_space, euclidean_space) heine_borel
 proof
   fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   assume f: "bounded (range f)"
   then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "subseq r"