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.41    unfolding setsum_addf
    1.42 -  apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
    1.43 +  apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
    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}"