Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
--- a/src/HOL/Analysis/Change_Of_Vars.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Tue May 24 16:21:49 2022 +0100
@@ -3388,7 +3388,7 @@
integral S (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x))) = (vec b :: real ^ 1)
\<longleftrightarrow> (\<lambda>x. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) \<and>
integral (g ` S) (\<lambda>x. vec (f x)) = (vec b :: real ^ 1)"
- using assms unfolding has_field_derivative_iff_has_vector_derivative
+ using assms unfolding has_real_derivative_iff_has_vector_derivative
by (intro has_absolute_integral_change_of_variables_1 assms) auto
thus ?thesis
by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue May 24 16:21:49 2022 +0100
@@ -3830,7 +3830,7 @@
have "(f has_integral F b - F a) {a..b}"
by (intro fundamental_theorem_of_calculus)
- (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
+ (auto simp: has_real_derivative_iff_has_vector_derivative[symmetric]
intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
unfolding indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a]
@@ -3881,7 +3881,7 @@
and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
proof -
have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
- unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+ unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
using deriv by (auto intro: DERIV_subset)
have 2: "continuous_on {a .. b} f"
using cont by (intro continuous_at_imp_continuous_on) auto
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue May 24 16:21:49 2022 +0100
@@ -795,6 +795,11 @@
using has_integral_eq[of s f g] has_integral_eq[of s g f] assms
by auto
+lemma integrable_cong:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
+ shows "f integrable_on A \<longleftrightarrow> g integrable_on A"
+ using has_integral_cong [OF assms] by fast
+
lemma integral_cong:
assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
shows "integral s f = integral s g"
@@ -2712,6 +2717,13 @@
qed
qed
+lemma has_complex_derivative_imp_has_vector_derivative:
+ fixes f :: "complex \<Rightarrow> complex"
+ assumes "(f has_field_derivative f') (at (of_real a) within (cbox (of_real x) (of_real y)))"
+ shows "((f o of_real) has_vector_derivative f') (at a within {x..y})"
+ using has_derivative_in_compose[of of_real of_real a "{x..y}" f "(*) f'"] assms
+ by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def o_def cbox_complex_of_real)
+
lemma ident_has_integral:
fixes a::real
assumes "a \<le> b"
@@ -2742,7 +2754,7 @@
have "(sin has_integral (- cos b - - cos a)) {a..b}"
proof (rule fundamental_theorem_of_calculus)
show "((\<lambda>a. - cos a) has_vector_derivative sin x) (at x within {a..b})" for x
- unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+ unfolding has_real_derivative_iff_has_vector_derivative [symmetric]
by (rule derivative_eq_intros | force)+
qed (use assms in auto)
then show ?thesis
@@ -2756,13 +2768,20 @@
have "(cos has_integral (sin b - sin a)) {a..b}"
proof (rule fundamental_theorem_of_calculus)
show "(sin has_vector_derivative cos x) (at x within {a..b})" for x
- unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+ unfolding has_real_derivative_iff_has_vector_derivative [symmetric]
by (rule derivative_eq_intros | force)+
qed (use assms in auto)
then show ?thesis
by (simp add: integral_unique)
qed
+lemma integral_exp [simp]:
+ fixes a::real
+ assumes "a \<le> b" shows "integral {a..b} exp = exp b - exp a"
+ by (meson DERIV_exp assms fundamental_theorem_of_calculus has_real_derivative_iff_has_vector_derivative
+ has_vector_derivative_at_within integral_unique)
+
+
lemma has_integral_sin_nx: "((\<lambda>x. sin(real_of_int n * x)) has_integral 0) {-pi..pi}"
proof (cases "n = 0")
case False
@@ -3265,7 +3284,7 @@
assumes "t \<in> {a..b}"
shows "((\<lambda>x. integral {a..x} g) has_real_derivative g t) (at t within {a..b})"
using integral_has_vector_derivative[of a b g t] assms
- by (auto simp: has_field_derivative_iff_has_vector_derivative)
+ by (auto simp: has_real_derivative_iff_has_vector_derivative)
lemma antiderivative_continuous:
fixes q b :: real
@@ -3533,6 +3552,11 @@
using assms has_integral_cmul[of f I A c]
has_integral_cmul[of "\<lambda>x. c *\<^sub>R f x" "c *\<^sub>R I" A "inverse c"] by (auto simp: field_simps)
+lemma has_integral_cmul_iff':
+ assumes "c \<noteq> 0"
+ shows "((\<lambda>x. c *\<^sub>R f x) has_integral I) A \<longleftrightarrow> (f has_integral I /\<^sub>R c) A"
+ using assms by (metis divideR_right has_integral_cmul_iff)
+
lemma has_integral_affinity':
fixes a :: "'a::euclidean_space"
assumes "(f has_integral i) (cbox a b)" and "m > 0"
@@ -4369,7 +4393,7 @@
assumes "t \<in> {a..b}"
shows "((\<lambda>x. integral {x..b} g) has_real_derivative -g t) (at t within {a..b})"
using integral_has_vector_derivative'[OF assms]
- by (auto simp: has_field_derivative_iff_has_vector_derivative)
+ by (auto simp: has_real_derivative_iff_has_vector_derivative)
subsection \<open>This doesn't directly involve integration, but that gives an easy proof\<close>
@@ -4990,6 +5014,21 @@
shows "integral(box a b) f = integral(cbox a b) f"
by (metis has_integral_integrable_integral has_integral_open_interval not_integrable_integral)
+lemma has_integral_Icc_iff_Ioo:
+ fixes f :: "real \<Rightarrow> 'a :: banach"
+ shows "(f has_integral I) {a..b} \<longleftrightarrow> (f has_integral I) {a<..<b}"
+proof (rule has_integral_spike_set_eq)
+ show "negligible {x \<in> {a..b} - {a<..<b}. f x \<noteq> 0}"
+ by (rule negligible_subset [of "{a,b}"]) auto
+ show "negligible {x \<in> {a<..<b} - {a..b}. f x \<noteq> 0}"
+ by (rule negligible_subset [of "{}"]) auto
+qed
+
+lemma integrable_on_Icc_iff_Ioo:
+ fixes f :: "real \<Rightarrow> 'a :: banach"
+ shows "f integrable_on {a..b} \<longleftrightarrow> f integrable_on {a<..<b}"
+ using has_integral_Icc_iff_Ioo by blast
+
subsection \<open>More lemmas that are useful later\<close>
@@ -6458,7 +6497,7 @@
have M': "M' \<ge> a" "M' \<ge> M" unfolding M'_def by linarith+
have int_g: "(g has_integral (G (real n) - G (real m))) {real m..real n}"
using 1 M' by (intro fundamental_theorem_of_calculus)
- (auto simp: has_field_derivative_iff_has_vector_derivative [symmetric]
+ (auto simp: has_real_derivative_iff_has_vector_derivative [symmetric]
intro!: DERIV_subset[OF deriv])
have int_f: "f x integrable_on {a'..real n}" if "a' \<ge> a" for a'
using that 1 by (cases "a' \<le> real n") (auto intro: integrable)
@@ -6907,7 +6946,7 @@
(at x within {a..b})" if "x \<in> {a..b} - s" for x
proof (rule has_vector_derivative_eq_rhs [OF vector_diff_chain_within refl])
show "(g has_vector_derivative g' x) (at x within {a..b})"
- using deriv has_field_derivative_iff_has_vector_derivative that by blast
+ using deriv has_real_derivative_iff_has_vector_derivative that by blast
show "((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x))
(at (g x) within g ` {a..b})"
using that le subset
@@ -7320,7 +7359,7 @@
have "((\<lambda>x. exp (-a*x)) has_integral (-exp (-a*real k)/a - (-exp (-a*c)/a))) {c..real k}"
by (intro fundamental_theorem_of_calculus)
(auto intro!: derivative_eq_intros
- simp: has_field_derivative_iff_has_vector_derivative [symmetric])
+ simp: has_real_derivative_iff_has_vector_derivative [symmetric])
hence "(f k has_integral (exp (-a*c)/a - exp (-a*real k)/a)) {c..}" unfolding f_def
by (subst has_integral_restrict) simp_all
} note has_integral_f = this
@@ -7409,7 +7448,7 @@
inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}"
using True a by (intro fundamental_theorem_of_calculus)
(auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const
- simp: has_field_derivative_iff_has_vector_derivative [symmetric])
+ simp: has_real_derivative_iff_has_vector_derivative [symmetric])
with True show ?thesis unfolding f_def F_def by (subst has_integral_restrict) simp_all
next
case False
@@ -7494,7 +7533,7 @@
proof -
from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
- simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
+ simp: has_real_derivative_iff_has_vector_derivative [symmetric] F_def)
hence "(f n has_integral (F n - F a)) {a..n}"
by (rule has_integral_eq [rotated]) (simp add: f_def)
thus "(f n has_integral (F n - F a)) {a..}"
--- a/src/HOL/Analysis/Infinite_Sum.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy Tue May 24 16:21:49 2022 +0100
@@ -696,11 +696,45 @@
shows \<open>infsum f (A \<union> B) = infsum f A + infsum f B\<close>
by (intro infsumI has_sum_Un_disjoint has_sum_infsum assms)
-(* TODO move *)
-lemma (in uniform_space) cauchy_filter_complete_converges:
- assumes "cauchy_filter F" "complete A" "F \<le> principal A" "F \<noteq> bot"
- shows "\<exists>c. F \<le> nhds c"
- using assms unfolding complete_uniform by blast
+lemma norm_summable_imp_has_sum:
+ fixes f :: "nat \<Rightarrow> 'a :: banach"
+ assumes "summable (\<lambda>n. norm (f n))" and "f sums S"
+ shows "has_sum f (UNIV :: nat set) S"
+ unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top
+proof (safe, goal_cases)
+ case (1 \<epsilon>)
+ from assms(1) obtain S' where S': "(\<lambda>n. norm (f n)) sums S'"
+ by (auto simp: summable_def)
+ with 1 obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> \<bar>S' - (\<Sum>i<n. norm (f i))\<bar> < \<epsilon>"
+ by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute)
+
+ show ?case
+ proof (rule exI[of _ "{..<N}"], safe, goal_cases)
+ case (2 Y)
+ from 2 have "(\<lambda>n. if n \<in> Y then 0 else f n) sums (S - sum f Y)"
+ by (intro sums_If_finite_set'[OF \<open>f sums S\<close>]) (auto simp: sum_negf)
+ hence "S - sum f Y = (\<Sum>n. if n \<in> Y then 0 else f n)"
+ by (simp add: sums_iff)
+ also have "norm \<dots> \<le> (\<Sum>n. norm (if n \<in> Y then 0 else f n))"
+ by (rule summable_norm[OF summable_comparison_test'[OF assms(1)]]) auto
+ also have "\<dots> \<le> (\<Sum>n. if n < N then 0 else norm (f n))"
+ using 2 by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto
+ also have "(\<lambda>n. if n \<in> {..<N} then 0 else norm (f n)) sums (S' - (\<Sum>i<N. norm (f i)))"
+ by (intro sums_If_finite_set'[OF S']) (auto simp: sum_negf)
+ hence "(\<Sum>n. if n < N then 0 else norm (f n)) = S' - (\<Sum>i<N. norm (f i))"
+ by (simp add: sums_iff)
+ also have "S' - (\<Sum>i<N. norm (f i)) \<le> \<bar>S' - (\<Sum>i<N. norm (f i))\<bar>" by simp
+ also have "\<dots> < \<epsilon>" by (rule N) auto
+ finally show ?case by (simp add: dist_norm norm_minus_commute)
+ qed auto
+qed
+
+lemma norm_summable_imp_summable_on:
+ fixes f :: "nat \<Rightarrow> 'a :: banach"
+ assumes "summable (\<lambda>n. norm (f n))"
+ shows "f summable_on UNIV"
+ using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms
+ by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel)
text \<open>The following lemma indeed needs a complete space (as formalized by the premise \<^term>\<open>complete UNIV\<close>).
The following two counterexamples show this:
--- a/src/HOL/Analysis/Interval_Integral.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Tue May 24 16:21:49 2022 +0100
@@ -653,7 +653,7 @@
have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
using assms approx apply (intro interval_integral_FTC_finite)
apply (auto simp: less_imp_le min_def max_def
- has_field_derivative_iff_has_vector_derivative[symmetric])
+ has_real_derivative_iff_has_vector_derivative[symmetric])
apply (rule continuous_at_imp_continuous_on, auto intro!: f)
by (rule DERIV_subset [OF F], auto)
have 1: "\<And>i. set_integrable lborel {l i..u i} f"
@@ -807,7 +807,7 @@
shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
proof-
have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
- using derivg unfolding has_field_derivative_iff_has_vector_derivative .
+ using derivg unfolding has_real_derivative_iff_has_vector_derivative .
then have contg [simp]: "continuous_on {a..b} g"
by (rule continuous_on_vector_derivative) auto
have 1: "\<exists>x\<in>{a..b}. u = g x" if "min (g a) (g b) \<le> u" "u \<le> max (g a) (g b)" for u
@@ -920,7 +920,7 @@
(* finally, the main argument *)
have eq1: "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
- unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+ unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
apply (auto intro!: continuous_at_imp_continuous_on contf contg')
done
have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
@@ -1023,7 +1023,7 @@
proof -
have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
- unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+ unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
apply (auto simp: less_imp_le intro!: continuous_at_imp_continuous_on contf contg')
done
then show ?thesis
@@ -1124,6 +1124,6 @@
(* TODO: should we have a library of facts like these? *)
lemma integral_cos: "t \<noteq> 0 \<Longrightarrow> LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t"
apply (intro interval_integral_FTC_finite continuous_intros)
- by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric])
+ by (auto intro!: derivative_eq_intros simp: has_real_derivative_iff_has_vector_derivative[symmetric])
end
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Tue May 24 16:21:49 2022 +0100
@@ -30,7 +30,7 @@
Mg': "set_borel_measurable borel {a..b} g'"
by (simp_all only: set_measurable_continuous_on_ivl)
from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
- by (simp only: has_field_derivative_iff_has_vector_derivative)
+ by (simp only: has_real_derivative_iff_has_vector_derivative)
have real_ind[simp]: "\<And>A x. enn2real (indicator A x) = indicator A x"
by (auto split: split_indicator)
@@ -73,7 +73,7 @@
hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow>
(g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
by (simp only: u'v' max_absorb2 min_absorb1)
- (auto simp: has_field_derivative_iff_has_vector_derivative)
+ (auto simp: has_real_derivative_iff_has_vector_derivative)
have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue May 24 16:21:49 2022 +0100
@@ -815,6 +815,14 @@
"x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
+lemma cbox_complex_of_real: "cbox (complex_of_real x) (complex_of_real y) = complex_of_real ` {x..y}"
+proof -
+ have "(x \<le> Re z \<and> Re z \<le> y \<and> Im z = 0) = (z \<in> complex_of_real ` {x..y})" for z
+ by (cases z) (simp add: complex_eq_cancel_iff2 image_iff)
+ then show ?thesis
+ by (auto simp: in_cbox_complex_iff)
+qed
+
lemma box_Complex_eq:
"box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
@@ -823,6 +831,9 @@
"x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
+lemma box_complex_of_real [simp]: "box (complex_of_real x) (complex_of_real y) = {}"
+ by (auto simp: in_box_complex_iff)
+
lemma Int_interval:
fixes a :: "'a::euclidean_space"
shows "cbox a b \<inter> cbox c d =
--- a/src/HOL/Deriv.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Deriv.thy Tue May 24 16:21:49 2022 +0100
@@ -841,14 +841,15 @@
subsection \<open>Vector derivative\<close>
-lemma has_field_derivative_iff_has_vector_derivative:
- "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
+text \<open>It's for real derivatives only, and not obviously generalisable to field derivatives\<close>
+lemma has_real_derivative_iff_has_vector_derivative:
+ "(f has_real_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
lemma has_field_derivative_subset:
"(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
(f has_field_derivative y) (at x within t)"
- unfolding has_field_derivative_def by (rule has_derivative_subset)
+ by (fact DERIV_subset)
lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
by (auto simp: has_vector_derivative_def)
@@ -903,7 +904,7 @@
lemma has_vector_derivative_scaleR[derivative_intros]:
"(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)"
- unfolding has_field_derivative_iff_has_vector_derivative
+ unfolding has_real_derivative_iff_has_vector_derivative
by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR])
lemma has_vector_derivative_mult[derivative_intros]:
@@ -915,7 +916,7 @@
lemma has_vector_derivative_of_real[derivative_intros]:
"(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F"
by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
- (simp add: has_field_derivative_iff_has_vector_derivative)
+ (simp add: has_real_derivative_iff_has_vector_derivative)
lemma has_vector_derivative_real_field:
"(f has_field_derivative f') (at (of_real a)) \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
--- a/src/HOL/Library/Landau_Symbols.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy Tue May 24 16:21:49 2022 +0100
@@ -508,6 +508,16 @@
end
+lemma summable_comparison_test_bigo:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes "summable (\<lambda>n. norm (g n))" "f \<in> O(g)"
+ shows "summable f"
+proof -
+ from \<open>f \<in> O(g)\<close> obtain C where C: "eventually (\<lambda>x. norm (f x) \<le> C * norm (g x)) at_top"
+ by (auto elim: landau_o.bigE)
+ thus ?thesis
+ by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
+qed
lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"
proof
--- a/src/HOL/Probability/Characteristic_Functions.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy Tue May 24 16:21:49 2022 +0100
@@ -238,7 +238,7 @@
have "LBINT s=0..x. (x - s)^n = ?F x - ?F 0"
unfolding zero_ereal_def
by (intro interval_integral_FTC_finite continuous_at_imp_continuous_on
- has_field_derivative_iff_has_vector_derivative[THEN iffD1])
+ has_real_derivative_iff_has_vector_derivative[THEN iffD1])
(auto simp del: power_Suc intro!: derivative_eq_intros simp add: add_nonneg_eq_0_iff)
also have "\<dots> = x ^ (Suc n) / (Suc n)" by simp
finally show ?thesis .
--- a/src/HOL/Probability/Sinc_Integral.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy Tue May 24 16:21:49 2022 +0100
@@ -48,7 +48,7 @@
proof (subst interval_integral_FTC_finite)
show "(?F has_vector_derivative exp (- (u * x)) * sin x) (at x within {min 0 t..max 0 t})" for x
by (auto intro!: derivative_eq_intros
- simp: has_field_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
+ simp: has_real_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
(simp_all add: field_simps add_nonneg_eq_0_iff)
qed (auto intro: continuous_at_imp_continuous_on)
@@ -197,7 +197,7 @@
ultimately show ?thesis
using interval_integral_FTC2[of "min 0 (x - 1)" 0 "max 0 (x + 1)" sinc x]
by (auto simp: continuous_at_imp_continuous_on isCont_sinc Si_alt_def[abs_def] zero_ereal_def
- has_field_derivative_iff_has_vector_derivative
+ has_real_derivative_iff_has_vector_derivative
split del: if_split)
qed
--- a/src/HOL/Topological_Spaces.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue May 24 16:21:49 2022 +0100
@@ -3415,6 +3415,11 @@
where complete_uniform: "complete S \<longleftrightarrow>
(\<forall>F \<le> principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x))"
+lemma (in uniform_space) cauchy_filter_complete_converges:
+ assumes "cauchy_filter F" "complete A" "F \<le> principal A" "F \<noteq> bot"
+ shows "\<exists>c. F \<le> nhds c"
+ using assms unfolding complete_uniform by blast
+
end
subsubsection \<open>Uniformly continuous functions\<close>