src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
 changeset 56212 3253aaf73a01 parent 56166 9a241bc276cd child 56218 1c3f1f2431f9
```     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 18 21:02:33 2014 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 18 22:11:46 2014 +0100
1.3 @@ -537,10 +537,10 @@
1.4  next
1.5    case (real r)
1.6    then show ?thesis
1.7 -    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
1.8 -    apply (subst INFI_ereal_cminus)
1.9 +    unfolding liminf_SUP_INF limsup_INF_SUP
1.10 +    apply (subst INF_ereal_cminus)
1.11      apply auto
1.12 -    apply (subst SUPR_ereal_cminus)
1.13 +    apply (subst SUP_ereal_cminus)
1.14      apply auto
1.15      done
1.16  qed (insert `c \<noteq> -\<infinity>`, simp)
1.17 @@ -874,7 +874,7 @@
1.18    unfolding summable_def
1.19    by auto
1.20
1.21 -lemma suminf_ereal_eq_SUPR:
1.22 +lemma suminf_ereal_eq_SUP:
1.23    fixes f :: "nat \<Rightarrow> ereal"
1.24    assumes "\<And>i. 0 \<le> f i"
1.25    shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
1.26 @@ -917,7 +917,7 @@
1.27    fixes f :: "nat \<Rightarrow> ereal"
1.28    assumes "\<And>n. 0 \<le> f n"
1.29    shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
1.30 -  unfolding suminf_ereal_eq_SUPR[OF assms]
1.31 +  unfolding suminf_ereal_eq_SUP [OF assms]
1.32    by (auto intro: complete_lattice_class.SUP_upper)
1.33
1.34  lemma suminf_0_le:
1.35 @@ -956,9 +956,9 @@
1.36    assumes "\<And>i. 0 \<le> f i"
1.37      and "\<And>i. 0 \<le> g i"
1.38    shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
1.39 -  apply (subst (1 2 3) suminf_ereal_eq_SUPR)
1.40 +  apply (subst (1 2 3) suminf_ereal_eq_SUP)
1.44    done
1.45
1.46  lemma suminf_cmult_ereal:
1.47 @@ -967,8 +967,8 @@
1.48      and "0 \<le> a"
1.49    shows "(\<Sum>i. a * f i) = a * suminf f"
1.50    by (auto simp: setsum_ereal_right_distrib[symmetric] assms
1.51 -       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
1.52 -       intro!: SUPR_ereal_cmult )
1.53 +       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
1.54 +       intro!: SUP_ereal_cmult)
1.55
1.56  lemma suminf_PInfty:
1.57    fixes f :: "nat \<Rightarrow> ereal"
1.58 @@ -1107,12 +1107,12 @@
1.59      fix n :: nat
1.60      have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
1.61        using assms
1.62 -      by (auto intro!: SUPR_ereal_setsum[symmetric])
1.63 +      by (auto intro!: SUP_ereal_setsum [symmetric])
1.64    }
1.65    note * = this
1.66    show ?thesis
1.67      using assms
1.68 -    apply (subst (1 2) suminf_ereal_eq_SUPR)
1.69 +    apply (subst (1 2) suminf_ereal_eq_SUP)
1.70      unfolding *
1.71      apply (auto intro!: SUP_upper2)
1.72      apply (subst SUP_commute)
1.73 @@ -1161,7 +1161,7 @@
1.74    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
1.75    shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
1.76    unfolding Liminf_def eventually_at
1.77 -proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
1.78 +proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
1.79    fix P d
1.80    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
1.81    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
1.82 @@ -1181,7 +1181,7 @@
1.83    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
1.84    shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
1.85    unfolding Limsup_def eventually_at
1.86 -proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
1.87 +proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
1.88    fix P d
1.89    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
1.90    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
```