--- a/src/HOL/Analysis/Binary_Product_Measure.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Fri Feb 23 15:17:51 2018 +0100
@@ -759,18 +759,20 @@
with A B have fin_Pair: "\<And>x. finite (Pair x -` X)"
by (intro finite_subset[OF _ B]) auto
have fin_X: "finite X" using X_subset by (rule finite_subset) (auto simp: A B)
- have pos_card: "(0::ennreal) < of_nat (card (Pair x -` X)) \<longleftrightarrow> Pair x -` X \<noteq> {}" for x
- by (auto simp: card_eq_0_iff fin_Pair) blast
-
- show "emeasure ?P X = emeasure ?C X"
- using X_subset A fin_Pair fin_X
- apply (subst B.emeasure_pair_measure_alt[OF X])
+ have card: "0 < card (Pair a -` X)" if "(a, b) \<in> X" for a b
+ using card_gt_0_iff fin_Pair that by auto
+ then have "emeasure ?P X = \<integral>\<^sup>+ x. emeasure (count_space B) (Pair x -` X)
+ \<partial>count_space A"
+ by (simp add: B.emeasure_pair_measure_alt X)
+ also have "... = emeasure ?C X"
apply (subst emeasure_count_space)
- apply (auto simp add: emeasure_count_space nn_integral_count_space
- pos_card of_nat_sum[symmetric] card_SigmaI[symmetric]
- simp del: of_nat_sum card_SigmaI
+ using card X_subset A fin_Pair fin_X
+ apply (auto simp add: nn_integral_count_space
+ of_nat_sum[symmetric] card_SigmaI[symmetric]
+ simp del: card_SigmaI
intro!: arg_cong[where f=card])
done
+ finally show "emeasure ?P X = emeasure ?C X" .
qed
--- a/src/HOL/Analysis/Borel_Space.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Fri Feb 23 15:17:51 2018 +0100
@@ -242,6 +242,11 @@
shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
+lemma closed_subset_contains_Sup:
+ fixes A C :: "real set"
+ shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
+ by (metis closure_contains_Sup closure_minimal subset_eq)
+
lemma deriv_nonneg_imp_mono:
assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Fri Feb 23 15:17:51 2018 +0100
@@ -8,8 +8,35 @@
imports
Topology_Euclidean_Space
Operator_Norm
+ Uniform_Limit
begin
+lemma onorm_componentwise:
+ assumes "bounded_linear f"
+ shows "onorm f \<le> (\<Sum>i\<in>Basis. norm (f i))"
+proof -
+ {
+ fix i::'a
+ assume "i \<in> Basis"
+ hence "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> onorm (\<lambda>x. (x \<bullet> i)) * norm (f i)"
+ by (auto intro!: onorm_scaleR_left_lemma bounded_linear_inner_left)
+ also have "\<dots> \<le> norm i * norm (f i)"
+ by (rule mult_right_mono)
+ (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
+ finally have "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> norm (f i)" using \<open>i \<in> Basis\<close>
+ by simp
+ } hence "onorm (\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<le> (\<Sum>i\<in>Basis. norm (f i))"
+ by (auto intro!: order_trans[OF onorm_sum_le] bounded_linear_scaleR_const
+ sum_mono bounded_linear_inner_left)
+ also have "(\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) = (\<lambda>x. f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i))"
+ by (simp add: linear_sum bounded_linear.linear assms linear_simps)
+ also have "\<dots> = f"
+ by (simp add: euclidean_representation)
+ finally show ?thesis .
+qed
+
+lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
+
subsection \<open>Intro rules for @{term bounded_linear}\<close>
named_theorems bounded_linear_intros
@@ -447,6 +474,15 @@
shows "continuous F f"
using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
+lemma
+ continuous_on_blinfun_componentwise:
+ fixes f:: "'d::t2_space \<Rightarrow> 'e::euclidean_space \<Rightarrow>\<^sub>L 'f::real_normed_vector"
+ assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on s (\<lambda>x. f x i)"
+ shows "continuous_on s f"
+ using assms
+ by (auto intro!: continuous_at_imp_continuous_on intro!: tendsto_componentwise1
+ simp: continuous_on_eq_continuous_within continuous_def)
+
lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
by (auto intro!: bounded_linearI' bounded_linear_intros)
@@ -692,4 +728,9 @@
lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
+lemmas bounded_linear_function_uniform_limit_intros[uniform_limit_intros] =
+ bounded_linear.uniform_limit[OF bounded_linear_apply_blinfun]
+ bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
+ bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
+
end
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Fri Feb 23 15:17:51 2018 +0100
@@ -1,7 +1,7 @@
section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
theory Cartesian_Euclidean_Space
-imports Finite_Cartesian_Product Derivative
+imports Finite_Cartesian_Product Derivative
begin
lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
@@ -277,14 +277,22 @@
by (simp add: vec_eq_iff)
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
+
+lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
+ by (simp add: inner_axis' norm_eq_1)
+
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
by vector
+
lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
+
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
+
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)"
by (metis vector_mul_lcancel)
+
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
by (metis vector_mul_rcancel)
@@ -563,7 +571,7 @@
lemma transpose_mat [simp]: "transpose (mat n) = mat n"
by (vector transpose_def mat_def)
-lemma transpose_transpose: "transpose(transpose A) = A"
+lemma transpose_transpose [simp]: "transpose(transpose A) = A"
by (vector transpose_def)
lemma row_transpose [simp]:
@@ -576,10 +584,10 @@
shows "column i (transpose A) = row i A"
by (simp add: row_def column_def transpose_def vec_eq_iff)
-lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
+lemma rows_transpose [simp]: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
-lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
+lemma columns_transpose [simp]: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
by (metis transpose_transpose rows_transpose)
lemma matrix_mult_transpose_dot_column:
@@ -642,6 +650,12 @@
by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
field_simps sum_distrib_left sum.distrib)
+lemma
+ fixes A :: "real^'n^'m"
+ shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
+ and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
+ by (simp_all add: linear_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear)
+
lemma matrix_vector_mult_add_distrib [algebra_simps]:
fixes A :: "real^'n^'m"
shows "A *v (x + y) = A *v x + A *v y"
@@ -682,6 +696,8 @@
lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))"
by (simp add: ext matrix_works)
+declare matrix_vector_mul [symmetric, simp]
+
lemma matrix_of_matrix_vector_mul [simp]: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
@@ -1455,4 +1471,9 @@
unfolding vec_lambda_beta
by auto
+lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
+ bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
+ bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
+ bounded_linear.uniform_limit[OF bounded_linear_component_cart]
+
end
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Feb 23 15:17:51 2018 +0100
@@ -1199,7 +1199,7 @@
lemma vector_derivative_linepath_within:
"x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a"
- apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified])
+ apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified])
apply (auto simp: has_vector_derivative_linepath_within)
done
@@ -2695,7 +2695,7 @@
then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
by (simp add: Lim_at dist_norm inverse_eq_divide)
show ?thesis
- apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
+ apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
apply (rule Lim_transform [OF * Lim_eventually])
apply (simp add: inverse_eq_divide [symmetric] eventually_at)
using \<open>open s\<close> x
@@ -3573,7 +3573,7 @@
if "x \<in> {0..1} - S" for x
proof -
have "vector_derivative (uminus \<circ> \<gamma>) (at x within cbox 0 1) = - vector_derivative \<gamma> (at x within cbox 0 1)"
- apply (rule vector_derivative_within_closed_interval)
+ apply (rule vector_derivative_within_cbox)
using that
apply (auto simp: o_def)
apply (rule has_vector_derivative_minus)
--- a/src/HOL/Analysis/Connected.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Fri Feb 23 15:17:51 2018 +0100
@@ -1095,6 +1095,43 @@
qed
qed
+text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
+
+lemma distance_attains_sup:
+ assumes "compact s" "s \<noteq> {}"
+ shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
+proof (rule continuous_attains_sup [OF assms])
+ {
+ fix x
+ assume "x\<in>s"
+ have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
+ by (intro tendsto_dist tendsto_const tendsto_ident_at)
+ }
+ then show "continuous_on s (dist a)"
+ unfolding continuous_on ..
+qed
+
+text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
+
+lemma distance_attains_inf:
+ fixes a :: "'a::heine_borel"
+ assumes "closed s" and "s \<noteq> {}"
+ obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
+proof -
+ from assms obtain b where "b \<in> s" by auto
+ let ?B = "s \<inter> cball a (dist b a)"
+ have "?B \<noteq> {}" using \<open>b \<in> s\<close>
+ by (auto simp: dist_commute)
+ moreover have "continuous_on ?B (dist a)"
+ by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
+ moreover have "compact ?B"
+ by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
+ ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
+ by (metis continuous_attains_inf)
+ with that show ?thesis by fastforce
+qed
+
+
subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
lemma summable_imp_bounded:
@@ -1353,6 +1390,24 @@
shows "infdist x S > 0"
using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
+lemma
+ infdist_attains_inf:
+ fixes X::"'a::heine_borel set"
+ assumes "closed X"
+ assumes "X \<noteq> {}"
+ obtains x where "x \<in> X" "infdist y X = dist y x"
+proof -
+ have "bdd_below (dist y ` X)"
+ by auto
+ from distance_attains_inf[OF assms, of y]
+ obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
+ have "infdist y X = dist y x"
+ by (auto simp: infdist_def assms
+ intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
+ with \<open>x \<in> X\<close> show ?thesis ..
+qed
+
+
text \<open>Every metric space is a T4 space:\<close>
instance metric_space \<subseteq> t4_space
@@ -1423,6 +1478,36 @@
shows "continuous F (\<lambda>x. infdist (f x) A)"
using assms unfolding continuous_def by (rule tendsto_infdist)
+lemma compact_infdist_le:
+ fixes A::"'a::heine_borel set"
+ assumes "A \<noteq> {}"
+ assumes "compact A"
+ assumes "e > 0"
+ shows "compact {x. infdist x A \<le> e}"
+proof -
+ from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
+ continuous_infdist[OF continuous_ident, of _ UNIV A]
+ have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
+ moreover
+ from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
+ by (auto simp: compact_eq_bounded_closed bounded_def)
+ {
+ fix y
+ assume le: "infdist y A \<le> e"
+ from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
+ obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
+ have "dist x0 y \<le> dist y z + dist x0 z"
+ by (metis dist_commute dist_triangle)
+ also have "dist y z \<le> e" using le z by simp
+ also have "dist x0 z \<le> b" using b z by simp
+ finally have "dist x0 y \<le> b + e" by arith
+ } then
+ have "bounded {x. infdist x A \<le> e}"
+ by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
+ ultimately show "compact {x. infdist x A \<le> e}"
+ by (simp add: compact_eq_bounded_closed)
+qed
+
subsection \<open>Equality of continuous functions on closure and related results.\<close>
lemma continuous_closedin_preimage_constant:
@@ -2209,6 +2294,13 @@
by (metis assms continuous_open_vimage vimage_def)
qed
+lemma open_neg_translation:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "open s"
+ shows "open((\<lambda>x. a - x) ` s)"
+ using open_translation[OF open_negations[OF assms], of a]
+ by (auto simp: image_image)
+
lemma open_affinity:
fixes S :: "'a::real_normed_vector set"
assumes "open S" "c \<noteq> 0"
@@ -2392,42 +2484,6 @@
(\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"
unfolding continuous_on_iff dist_norm by simp
-text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
-
-lemma distance_attains_sup:
- assumes "compact s" "s \<noteq> {}"
- shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
-proof (rule continuous_attains_sup [OF assms])
- {
- fix x
- assume "x\<in>s"
- have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
- by (intro tendsto_dist tendsto_const tendsto_ident_at)
- }
- then show "continuous_on s (dist a)"
- unfolding continuous_on ..
-qed
-
-text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
-
-lemma distance_attains_inf:
- fixes a :: "'a::heine_borel"
- assumes "closed s" and "s \<noteq> {}"
- obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
-proof -
- from assms obtain b where "b \<in> s" by auto
- let ?B = "s \<inter> cball a (dist b a)"
- have "?B \<noteq> {}" using \<open>b \<in> s\<close>
- by (auto simp: dist_commute)
- moreover have "continuous_on ?B (dist a)"
- by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
- moreover have "compact ?B"
- by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
- ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
- by (metis continuous_attains_inf)
- with that show ?thesis by fastforce
-qed
-
subsection \<open>Cartesian products\<close>
@@ -2911,6 +2967,38 @@
using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
qed
+lemma compact_in_open_separated:
+ fixes A::"'a::heine_borel set"
+ assumes "A \<noteq> {}"
+ assumes "compact A"
+ assumes "open B"
+ assumes "A \<subseteq> B"
+ obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
+proof atomize_elim
+ have "closed (- B)" "compact A" "- B \<inter> A = {}"
+ using assms by (auto simp: open_Diff compact_eq_bounded_closed)
+ from separate_closed_compact[OF this]
+ obtain d'::real where d': "d'>0" "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d' \<le> dist x y"
+ by auto
+ define d where "d = d' / 2"
+ hence "d>0" "d < d'" using d' by auto
+ with d' have d: "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d < dist x y"
+ by force
+ show "\<exists>e>0. {x. infdist x A \<le> e} \<subseteq> B"
+ proof (rule ccontr)
+ assume "\<nexists>e. 0 < e \<and> {x. infdist x A \<le> e} \<subseteq> B"
+ with \<open>d > 0\<close> obtain x where x: "infdist x A \<le> d" "x \<notin> B"
+ by auto
+ from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)
+ from infdist_attains_inf[OF this]
+ obtain y where y: "y \<in> A" "infdist x A = dist x y"
+ by auto
+ have "dist x y \<le> d" using x y by simp
+ also have "\<dots> < dist x y" using y d x by auto
+ finally show False by simp
+ qed
+qed
+
subsection \<open>Compact sets and the closure operation.\<close>
@@ -4221,6 +4309,14 @@
using \<open>x\<in>s\<close> by blast
qed
+lemma banach_fix_type:
+ fixes f::"'a::complete_space\<Rightarrow>'a"
+ assumes c:"0 \<le> c" "c < 1"
+ and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"
+ shows "\<exists>!x. (f x = x)"
+ using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
+ by auto
+
subsection \<open>Edelstein fixed point theorem\<close>
@@ -4687,6 +4783,21 @@
by (simp add: \<open>countable \<F>'\<close> countable_subset)
qed
+lemma countable_disjoint_nonempty_interior_subsets:
+ fixes \<F> :: "'a::euclidean_space set set"
+ assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
+ shows "countable \<F>"
+proof (rule countable_image_inj_on)
+ have "disjoint (interior ` \<F>)"
+ using pw by (simp add: disjoint_image_subset interior_subset)
+ then show "countable (interior ` \<F>)"
+ by (auto intro: countable_disjoint_open_subsets)
+ show "inj_on interior \<F>"
+ using pw apply (clarsimp simp: inj_on_def pairwise_def)
+ apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
+ done
+qed
+
lemma closedin_compact:
"\<lbrakk>compact S; closedin (subtopology euclidean S) T\<rbrakk> \<Longrightarrow> compact T"
by (metis closedin_closed compact_Int_closed)
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Feb 23 15:17:51 2018 +0100
@@ -6659,9 +6659,13 @@
subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
-lemma is_interval_1:
- "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
- unfolding is_interval_def by auto
+lemma mem_is_interval_1_I:
+ fixes a b c::real
+ assumes "is_interval S"
+ assumes "a \<in> S" "c \<in> S"
+ assumes "a \<le> b" "b \<le> c"
+ shows "b \<in> S"
+ using assms is_interval_1 by blast
lemma is_interval_connected_1:
fixes s :: "real set"
@@ -6708,6 +6712,9 @@
shows "is_interval s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)
+lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
+ by (metis connected_ball is_interval_connected_1)
+
lemma connected_compact_interval_1:
"connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
@@ -6731,6 +6738,10 @@
by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
qed
+lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
+ by (auto simp: is_interval_convex_1 convex_cball)
+
+
subsection \<open>Another intermediate value theorem formulation\<close>
lemma ivt_increasing_component_on_1:
--- a/src/HOL/Analysis/Derivative.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy Fri Feb 23 15:17:51 2018 +0100
@@ -48,18 +48,6 @@
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
-text \<open>These are the only cases we'll care about, probably.\<close>
-
-lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
- bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
- unfolding has_derivative_def Lim
- by (auto simp add: netlimit_within field_simps)
-
-lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
- bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
- using has_derivative_within [of f f' x UNIV]
- by simp
-
text \<open>More explicit epsilon-delta forms.\<close>
lemma has_derivative_within':
@@ -131,27 +119,6 @@
by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
qed
-subsubsection \<open>Limit transformation for derivatives\<close>
-
-lemma has_derivative_transform_within:
- assumes "(f has_derivative f') (at x within s)"
- and "0 < d"
- and "x \<in> s"
- and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
- shows "(g has_derivative f') (at x within s)"
- using assms
- unfolding has_derivative_within
- by (force simp add: intro: Lim_transform_within)
-
-lemma has_derivative_transform_within_open:
- assumes "(f has_derivative f') (at x)"
- and "open s"
- and "x \<in> s"
- and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
- shows "(g has_derivative f') (at x)"
- using assms unfolding has_derivative_at
- by (force simp add: intro: Lim_transform_within_open)
-
subsection \<open>Differentiability\<close>
definition
@@ -304,6 +271,10 @@
unfolding differentiable_on_def
by auto
+lemma has_derivative_continuous_on:
+ "(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
+ by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)
+
text \<open>Results about neighborhoods filter.\<close>
lemma eventually_nhds_metric_le:
@@ -1143,6 +1114,20 @@
by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
qed
+lemma vector_differentiable_bound_linearization:
+ fixes f::"real \<Rightarrow> 'b::real_normed_vector"
+ assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
+ assumes "closed_segment a b \<subseteq> S"
+ assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
+ assumes "x0 \<in> S"
+ shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
+ using assms
+ by (intro differentiable_bound_linearization[of a b S f "\<lambda>x h. h *\<^sub>R f' x" x0 B])
+ (force simp: closed_segment_real_eq has_vector_derivative_def
+ scaleR_diff_right[symmetric] mult.commute[of B]
+ intro!: onorm_le mult_left_mono)+
+
+
text \<open>In particular.\<close>
lemma has_derivative_zero_constant:
@@ -1169,6 +1154,14 @@
using assms(2)[of x] by (simp add: has_field_derivative_def A)
qed fact
+lemma
+ has_vector_derivative_zero_constant:
+ assumes "convex s"
+ assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative 0) (at x within s)"
+ obtains c where "\<And>x. x \<in> s \<Longrightarrow> f x = c"
+ using has_derivative_zero_constant[of s f] assms
+ by (auto simp: has_vector_derivative_def)
+
lemma has_derivative_zero_unique:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "convex s"
@@ -2510,7 +2503,7 @@
apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
done
-lemma vector_derivative_within_closed_interval:
+lemma vector_derivative_within_cbox:
assumes ab: "a < b" "x \<in> cbox a b"
assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
shows "vector_derivative f (at x within cbox a b) = f'"
@@ -2518,6 +2511,14 @@
vector_derivative_works[THEN iffD1] differentiableI_vector)
fact
+lemma vector_derivative_within_closed_interval:
+ fixes f::"real \<Rightarrow> 'a::euclidean_space"
+ assumes "a < b" and "x \<in> {a .. b}"
+ assumes "(f has_vector_derivative f') (at x within {a .. b})"
+ shows "vector_derivative f (at x within {a .. b}) = f'"
+ using assms vector_derivative_within_cbox
+ by fastforce
+
lemma has_vector_derivative_within_subset:
"(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
@@ -2561,6 +2562,14 @@
unfolding has_vector_derivative_def
by (rule has_derivative_transform_within_open)
+lemma has_vector_derivative_transform:
+ assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+ assumes f': "(f has_vector_derivative f') (at x within s)"
+ shows "(g has_vector_derivative f') (at x within s)"
+ using assms
+ unfolding has_vector_derivative_def
+ by (rule has_derivative_transform)
+
lemma vector_diff_chain_at:
assumes "(f has_vector_derivative f') (at x)"
and "(g has_vector_derivative g') (at (f x))"
@@ -2589,7 +2598,7 @@
lemma vector_derivative_at_within_ivl:
"(f has_vector_derivative f') (at x) \<Longrightarrow>
a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
-using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
+ using has_vector_derivative_at_within vector_derivative_within_cbox by fastforce
lemma vector_derivative_chain_at:
assumes "f differentiable at x" "(g differentiable at (f x))"
@@ -2917,21 +2926,19 @@
qed
lemma has_derivative_partialsI:
- assumes fx: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_derivative blinfun_apply (fx x y)) (at x within X)"
+ fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
+ assumes fx: "((\<lambda>x. f x y) has_derivative fx) (at x within X)"
assumes fy: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)"
- assumes fx_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fx x y)"
- assumes fy_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fy x y)"
- assumes "x \<in> X" "y \<in> Y"
- assumes "convex X" "convex Y"
- shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X \<times> Y)"
+ assumes fy_cont[unfolded continuous_within]: "continuous (at (x, y) within X \<times> Y) (\<lambda>(x, y). fy x y)"
+ assumes "y \<in> Y" "convex Y"
+ shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx tx + fy x y ty)) (at (x, y) within X \<times> Y)"
proof (safe intro!: has_derivativeI tendstoI, goal_cases)
case (2 e')
+ interpret fx: bounded_linear "fx" using fx by (rule has_derivative_bounded_linear)
define e where "e = e' / 9"
have "e > 0" using \<open>e' > 0\<close> by (simp add: e_def)
- have "(x, y) \<in> X \<times> Y" using assms by auto
- from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this,
- unfolded continuous_within, THEN tendstoD, OF \<open>e > 0\<close>]
+ from fy_cont[THEN tendstoD, OF \<open>e > 0\<close>]
have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. dist (fy x' y') (fy x y) < e"
by (auto simp: split_beta')
from this[unfolded eventually_at] obtain d' where
@@ -2971,12 +2978,12 @@
} note onorm = this
have ev_mem: "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. (x', y') \<in> X \<times> Y"
- using \<open>x \<in> X\<close> \<open>y \<in> Y\<close>
+ using \<open>y \<in> Y\<close>
by (auto simp: eventually_at intro!: zero_less_one)
moreover
have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
using eventually_at_ball[OF that]
- by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
+ by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True)
note ev_dist[OF \<open>0 < d\<close>]
ultimately
have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
@@ -2997,32 +3004,31 @@
have "\<dots> \<subseteq> ball y d \<inter> Y"
using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
- (auto simp: dist_commute)
+ (auto simp: dist_commute mem_ball)
finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
} note seg = this
have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
- by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
+ by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: mem_ball dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
by (rule differentiable_bound_linearization[where S="?S"])
(auto intro!: \<open>0 < d\<close> \<open>y \<in> Y\<close>)
qed
moreover
- let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx x y) (x' - x)) \<le> norm (x' - x) * e"
- from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
+ let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
+ from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
have "\<forall>\<^sub>F x' in at x within X. ?le x'"
by eventually_elim
- (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
+ (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
by (rule eventually_at_Pair_within_TimesI1)
- (simp add: blinfun.bilinear_simps)
+ (simp add: blinfun.bilinear_simps fx.zero)
moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
unfolding norm_eq_zero right_minus_eq
by (auto simp: eventually_at intro!: zero_less_one)
moreover
- from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>],
- unfolded continuous_within, THEN tendstoD, OF \<open>0 < e\<close>]
+ from fy_cont[THEN tendstoD, OF \<open>0 < e\<close>]
have "\<forall>\<^sub>F x' in at x within X. norm (fy x' y - fy x y) < e"
unfolding eventually_at
using \<open>y \<in> Y\<close>
@@ -3032,22 +3038,22 @@
(simp add: blinfun.bilinear_simps \<open>0 < e\<close>)
ultimately
have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
- norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R
+ norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R
norm ((x', y') - (x, y)))
< e'"
apply eventually_elim
proof safe
fix x' y'
- have "norm (f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) \<le>
+ have "norm (f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) \<le>
norm (f x' y' - f x' y - fy x' y (y' - y)) +
norm (fy x y (y' - y) - fy x' y (y' - y)) +
- norm (f x' y - f x y - fx x y (x' - x))"
+ norm (f x' y - f x y - fx (x' - x))"
by norm
also
assume nz: "norm ((x', y') - (x, y)) \<noteq> 0"
and nfy: "norm (fy x' y - fy x y) < e"
assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
- also assume "norm (f x' y - f x y - blinfun_apply (fx x y) (x' - x)) \<le> norm (x' - x) * e"
+ also assume "norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
also
have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) \<le> norm ((fy x y) - (fy x' y)) * norm (y' - y)"
by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun)
@@ -3070,11 +3076,80 @@
also have "\<dots> < norm ((x', y') - (x, y)) * e'"
using \<open>0 < e'\<close> nz
by (auto simp: e_def)
- finally show "norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
+ finally show "norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
by (auto simp: divide_simps dist_norm mult.commute)
qed
then show ?case
by eventually_elim (auto simp: dist_norm field_simps)
-qed (auto intro!: bounded_linear_intros simp: split_beta')
+next
+ from has_derivative_bounded_linear[OF fx]
+ obtain fxb where "fx = blinfun_apply fxb"
+ by (metis bounded_linear_Blinfun_apply)
+ then show "bounded_linear (\<lambda>(tx, ty). fx tx + blinfun_apply (fy x y) ty)"
+ by (auto intro!: bounded_linear_intros simp: split_beta')
+qed
+
+
+subsection \<open>Differentiable case distinction\<close>
+
+lemma has_derivative_within_If_eq:
+ "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
+ (bounded_linear f' \<and>
+ ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
+ else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
+ \<longlongrightarrow> 0) (at x within s))"
+ (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
+proof -
+ have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
+ ((if P y then f y else g y) -
+ ((if P x then f x else g x) + f' (y - x)))) = ?if"
+ by (auto simp: inverse_eq_divide)
+ thus ?thesis by (auto simp: has_derivative_within)
+qed
+
+lemma has_derivative_If_within_closures:
+ assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+ assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+ assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+ assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+ assumes x_in: "x \<in> s \<union> t"
+ shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
+ (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
+proof -
+ from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
+ by (auto simp add: has_derivative_within)
+ from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
+ by (auto simp add: has_derivative_within)
+ have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
+ using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
+ by (unfold_locales; force)
+ show ?thesis
+ using f' g' closure_subset[of t] closure_subset[of s]
+ unfolding has_derivative_within_If_eq
+ by (intro conjI bl tendsto_If_within_closures x_in)
+ (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
+qed
+
+lemma has_vector_derivative_If_within_closures:
+ assumes x_in: "x \<in> s \<union> t"
+ assumes "u = s \<union> t"
+ assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+ assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+ assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+ assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+ shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
+ (if x \<in> s then f' x else g' x)) (at x within u)"
+ unfolding has_vector_derivative_def assms
+ using x_in
+ apply (intro has_derivative_If_within_closures[where
+ ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
+ THEN has_derivative_eq_rhs])
+ subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
+ subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
+ by (auto simp: assms)
end
--- a/src/HOL/Analysis/Determinants.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy Fri Feb 23 15:17:51 2018 +0100
@@ -929,7 +929,7 @@
by auto
qed
-text \<open>Orthogonality of a transformation and matrix.\<close>
+subsection \<open>Orthogonality of a transformation and matrix.\<close>
definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
@@ -945,6 +945,51 @@
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
+lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
+ by (simp add: linear_iff orthogonal_transformation_def)
+
+lemma orthogonal_orthogonal_transformation:
+ "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
+ by (simp add: orthogonal_def orthogonal_transformation_def)
+
+lemma orthogonal_transformation_compose:
+ "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
+ by (simp add: orthogonal_transformation_def linear_compose)
+
+lemma orthogonal_transformation_neg:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
+ by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
+
+lemma orthogonal_transformation_linear:
+ "orthogonal_transformation f \<Longrightarrow> linear f"
+ by (simp add: orthogonal_transformation_def)
+
+lemma orthogonal_transformation_inj:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> inj f"
+ unfolding orthogonal_transformation_def inj_on_def by (metis euclidean_eqI)
+
+lemma orthogonal_transformation_surj:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> surj f"
+ by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
+
+lemma orthogonal_transformation_bij:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> bij f"
+ by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
+
+lemma orthogonal_transformation_inv:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
+ by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
+
+lemma orthogonal_transformation_norm:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
+ by (metis orthogonal_transformation)
+
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
by (metis matrix_left_right_inverse orthogonal_matrix_def)
@@ -1038,7 +1083,13 @@
then show ?thesis unfolding th .
qed
-text \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
+lemma orthogonal_transformation_det [simp]:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
+ using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
+
+
+subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
lemma scaling_linear:
fixes f :: "real ^'n \<Rightarrow> real ^'n"
@@ -1071,20 +1122,138 @@
lemma orthogonal_transformation_isometry:
"orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
unfolding orthogonal_transformation
- apply (rule iffI)
- apply clarify
- apply (clarsimp simp add: linear_0 linear_diff[symmetric] dist_norm)
- apply (rule conjI)
- apply (rule isometry_linear)
- apply simp
- apply simp
- apply clarify
- apply (erule_tac x=v in allE)
- apply (erule_tac x=0 in allE)
- apply (simp add: dist_norm)
- done
+ apply (auto simp: linear_0 isometry_linear)
+ apply (metis (no_types, hide_lams) dist_norm linear_diff)
+ by (metis dist_0_norm)
+
+
+lemma image_orthogonal_transformation_ball:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ assumes "orthogonal_transformation f"
+ shows "f ` ball x r = ball (f x) r"
+proof (intro equalityI subsetI)
+ fix y assume "y \<in> f ` ball x r"
+ with assms show "y \<in> ball (f x) r"
+ by (auto simp: orthogonal_transformation_isometry)
+next
+ fix y assume y: "y \<in> ball (f x) r"
+ then obtain z where z: "y = f z"
+ using assms orthogonal_transformation_surj by blast
+ with y assms show "y \<in> f ` ball x r"
+ by (auto simp: orthogonal_transformation_isometry)
+qed
+
+lemma image_orthogonal_transformation_cball:
+ fixes f :: "real^'n \<Rightarrow> real^'n"
+ assumes "orthogonal_transformation f"
+ shows "f ` cball x r = cball (f x) r"
+proof (intro equalityI subsetI)
+ fix y assume "y \<in> f ` cball x r"
+ with assms show "y \<in> cball (f x) r"
+ by (auto simp: orthogonal_transformation_isometry)
+next
+ fix y assume y: "y \<in> cball (f x) r"
+ then obtain z where z: "y = f z"
+ using assms orthogonal_transformation_surj by blast
+ with y assms show "y \<in> f ` cball x r"
+ by (auto simp: orthogonal_transformation_isometry)
+qed
+
+subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
+
+lemma orthogonal_matrix_transpose [simp]:
+ "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
+ by (auto simp: orthogonal_matrix_def)
+
+lemma orthogonal_matrix_orthonormal_columns:
+ fixes A :: "real^'n^'n"
+ shows "orthogonal_matrix A \<longleftrightarrow>
+ (\<forall>i. norm(column i A) = 1) \<and>
+ (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
+ by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
+
+lemma orthogonal_matrix_orthonormal_rows:
+ fixes A :: "real^'n^'n"
+ shows "orthogonal_matrix A \<longleftrightarrow>
+ (\<forall>i. norm(row i A) = 1) \<and>
+ (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
+ using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
-text \<open>Can extend an isometry from unit sphere.\<close>
+lemma orthogonal_matrix_exists_basis:
+ fixes a :: "real^'n"
+ assumes "norm a = 1"
+ obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
+proof -
+ obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+ and "independent S" "card S = CARD('n)" "span S = UNIV"
+ using vector_in_orthonormal_basis assms by force
+ with independent_imp_finite obtain f0 where "bij_betw f0 (UNIV::'n set) S"
+ by (metis finite_class.finite_UNIV finite_same_card_bij)
+ then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
+ using bij_swap_iff [of k "inv f0 a" f0]
+ by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply1)
+ show thesis
+ proof
+ have [simp]: "\<And>i. norm (f i) = 1"
+ using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
+ have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
+ using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
+ by (auto simp: pairwise_def bij_betw_def inj_on_def)
+ show "orthogonal_matrix (\<chi> i j. f j $ i)"
+ by (simp add: orthogonal_matrix_orthonormal_columns column_def)
+ show "(\<chi> i j. f j $ i) *v axis k 1 = a"
+ by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
+ qed
+qed
+
+lemma orthogonal_transformation_exists_1:
+ fixes a b :: "real^'n"
+ assumes "norm a = 1" "norm b = 1"
+ obtains f where "orthogonal_transformation f" "f a = b"
+proof -
+ obtain k::'n where True
+ by simp
+ obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+ using orthogonal_matrix_exists_basis assms by metis
+ let ?f = "\<lambda>x. (B ** transpose A) *v x"
+ show thesis
+ proof
+ show "orthogonal_transformation ?f"
+ by (simp add: AB orthogonal_matrix_mul matrix_vector_mul_linear orthogonal_transformation_matrix)
+ next
+ show "?f a = b"
+ using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
+ by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+ qed
+qed
+
+lemma orthogonal_transformation_exists:
+ fixes a b :: "real^'n"
+ assumes "norm a = norm b"
+ obtains f where "orthogonal_transformation f" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+ case True
+ with assms show ?thesis
+ using orthogonal_transformation_isometry that by fastforce
+next
+ case False
+ then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
+ by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
+ show ?thesis
+ proof
+ have "linear f"
+ using f by (simp add: orthogonal_transformation_linear)
+ then have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
+ by (simp add: linear_cmul [of f])
+ also have "\<dots> = b /\<^sub>R norm a"
+ by (simp add: eq assms [symmetric])
+ finally show "f a = b"
+ using False by auto
+ qed (use f in auto)
+qed
+
+
+subsection \<open>Can extend an isometry from unit sphere.\<close>
lemma isometry_sphere_extend:
fixes f:: "real ^'n \<Rightarrow> real ^'n"
@@ -1182,7 +1351,7 @@
done
qed
-text \<open>Rotation, reflection, rotoinversion.\<close>
+subsection \<open>Rotation, reflection, rotoinversion.\<close>
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
@@ -1238,4 +1407,111 @@
by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
qed
+text\<open> Slightly stronger results giving rotation, but only in two or more dimensions.\<close>
+
+lemma rotation_matrix_exists_basis:
+ fixes a :: "real^'n"
+ assumes 2: "2 \<le> CARD('n)" and "norm a = 1"
+ obtains A where "rotation_matrix A" "A *v (axis k 1) = a"
+proof -
+ obtain A where "orthogonal_matrix A" and A: "A *v (axis k 1) = a"
+ using orthogonal_matrix_exists_basis assms by metis
+ with orthogonal_rotation_or_rotoinversion
+ consider "rotation_matrix A" | "rotoinversion_matrix A"
+ by metis
+ then show thesis
+ proof cases
+ assume "rotation_matrix A"
+ then show ?thesis
+ using \<open>A *v axis k 1 = a\<close> that by auto
+ next
+ obtain j where "j \<noteq> k"
+ by (metis (full_types) 2 card_2_exists ex_card)
+ let ?TA = "transpose A"
+ let ?A = "\<chi> i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i"
+ assume "rotoinversion_matrix A"
+ then have [simp]: "det A = -1"
+ by (simp add: rotoinversion_matrix_def)
+ show ?thesis
+ proof
+ have [simp]: "row i (\<chi> i. if i = j then - 1 *\<^sub>R ?TA $ i else ?TA $ i) = (if i = j then - row i ?TA else row i ?TA)" for i
+ by (auto simp: row_def)
+ have "orthogonal_matrix ?A"
+ unfolding orthogonal_matrix_orthonormal_rows
+ using \<open>orthogonal_matrix A\<close> by (auto simp: orthogonal_matrix_orthonormal_columns orthogonal_clauses)
+ then show "rotation_matrix (transpose ?A)"
+ unfolding rotation_matrix_def
+ by (simp add: det_row_mul[of j _ "\<lambda>i. ?TA $ i", unfolded scalar_mult_eq_scaleR])
+ show "transpose ?A *v axis k 1 = a"
+ using \<open>j \<noteq> k\<close> A by (simp add: matrix_vector_column axis_def scalar_mult_eq_scaleR if_distrib [of "\<lambda>z. z *\<^sub>R c" for c] cong: if_cong)
+ qed
+ qed
+qed
+
+lemma rotation_exists_1:
+ fixes a :: "real^'n"
+ assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1"
+ obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof -
+ obtain k::'n where True
+ by simp
+ obtain A B where AB: "rotation_matrix A" "rotation_matrix B"
+ and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
+ using rotation_matrix_exists_basis assms by metis
+ let ?f = "\<lambda>x. (B ** transpose A) *v x"
+ show thesis
+ proof
+ show "orthogonal_transformation ?f"
+ using AB orthogonal_matrix_mul orthogonal_transformation_matrix rotation_matrix_def matrix_vector_mul_linear by force
+ show "det (matrix ?f) = 1"
+ using AB by (auto simp: det_mul rotation_matrix_def)
+ show "?f a = b"
+ using AB unfolding orthogonal_matrix_def rotation_matrix_def
+ by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
+ qed
+qed
+
+lemma rotation_exists:
+ fixes a :: "real^'n"
+ assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b"
+ obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
+proof (cases "a = 0 \<or> b = 0")
+ case True
+ with assms have "a = 0" "b = 0"
+ by auto
+ then show ?thesis
+ by (metis eq_id_iff matrix_id orthogonal_transformation_id that)
+next
+ case False
+ with that show thesis
+ by (auto simp: eq linear_cmul orthogonal_transformation_def
+ intro: rotation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b", OF 2])
+qed
+
+lemma rotation_rightward_line:
+ fixes a :: "real^'n"
+ obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1"
+ "f(norm a *\<^sub>R axis k 1) = a"
+proof (cases "CARD('n) = 1")
+ case True
+ obtain f where "orthogonal_transformation f" "f (norm a *\<^sub>R axis k (1::real)) = a"
+ proof (rule orthogonal_transformation_exists)
+ show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+ by simp
+ qed auto
+ then show thesis
+ using True that by auto
+next
+ case False
+ obtain f where "orthogonal_transformation f" "det(matrix f) = 1" "f (norm a *\<^sub>R axis k 1) = a"
+ proof (rule rotation_exists)
+ show "2 \<le> CARD('n)"
+ using False one_le_card_finite [where 'a='n] by linarith
+ show "norm (norm a *\<^sub>R axis k (1::real)) = norm a"
+ by simp
+ qed auto
+ then show thesis
+ using that by blast
+qed
+
end
--- a/src/HOL/Analysis/Euclidean_Space.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Fri Feb 23 15:17:51 2018 +0100
@@ -84,6 +84,10 @@
lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
unfolding euclidean_representation_sum by simp
+lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))"
+ by (subst (1 2) euclidean_representation [symmetric])
+ (simp add: inner_sum_right inner_Basis ac_simps)
+
lemma (in euclidean_space) choice_Basis_iff:
fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Feb 23 15:17:51 2018 +0100
@@ -20,9 +20,19 @@
declare vec_lambda_inject [simplified, simp]
+bundle vec_syntax begin
notation
vec_nth (infixl "$" 90) and
vec_lambda (binder "\<chi>" 10)
+end
+
+bundle no_vec_syntax begin
+no_notation
+ vec_nth (infixl "$" 90) and
+ vec_lambda (binder "\<chi>" 10)
+end
+
+unbundle vec_syntax
(*
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
@@ -134,6 +144,28 @@
qed
qed (simp_all add: infinite_UNIV_vec)
+lemma countable_vector:
+ fixes B:: "'n::finite \<Rightarrow> 'a set"
+ assumes "\<And>i. countable (B i)"
+ shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}"
+proof -
+ have "f \<in> ($) ` {V. \<forall>i. V $ i \<in> B i}" if "f \<in> Pi\<^sub>E UNIV B" for f
+ proof -
+ have "\<exists>W. (\<forall>i. W $ i \<in> B i) \<and> ($) W = f"
+ by (metis that PiE_iff UNIV_I vec_lambda_inverse)
+ then show "f \<in> ($) ` {v. \<forall>i. v $ i \<in> B i}"
+ by blast
+ qed
+ then have "Pi\<^sub>E UNIV B = vec_nth ` {V. \<forall>i::'n. V $ i \<in> B i}"
+ by blast
+ then have "countable (vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+ by (metis finite_class.finite_UNIV countable_PiE assms)
+ then have "countable (vec_lambda ` vec_nth ` {V. \<forall>i. V $ i \<in> B i})"
+ by auto
+ then show ?thesis
+ by (simp add: image_comp o_def vec_nth_inverse)
+qed
+
subsection \<open>Group operations and class instances\<close>
instantiation vec :: (zero, finite) zero
@@ -591,6 +623,9 @@
apply (simp add: axis_def)
done
+lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
+ by (simp add: inner_axis inner_commute)
+
instantiation vec :: (euclidean_space, finite) euclidean_space
begin
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Feb 23 15:17:51 2018 +0100
@@ -621,6 +621,11 @@
with False show ?thesis by (simp add: not_integrable_integral)
qed
+lemma integral_mult:
+ fixes K::real
+ shows "f integrable_on X \<Longrightarrow> K * integral X f = integral X (\<lambda>x. K * f x)"
+ unfolding real_scaleR_def[symmetric] integral_cmul ..
+
lemma integral_neg [simp]: "integral S (\<lambda>x. - f x) = - integral S f"
proof (cases "f integrable_on S")
case True then show ?thesis
@@ -2549,6 +2554,13 @@
lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
+lemma integrable_continuous_closed_segment:
+ fixes f :: "real \<Rightarrow> 'a::banach"
+ assumes "continuous_on (closed_segment a b) f"
+ shows "f integrable_on (closed_segment a b)"
+ using assms
+ by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
+
subsection \<open>Specialization of additivity to one dimension.\<close>
@@ -2722,6 +2734,32 @@
subsection \<open>Taylor series expansion\<close>
+lemma mvt_integral:
+ fixes f::"'a::real_normed_vector\<Rightarrow>'b::banach"
+ assumes f'[derivative_intros]:
+ "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
+ assumes line_in: "\<And>t. t \<in> {0..1} \<Longrightarrow> x + t *\<^sub>R y \<in> S"
+ shows "f (x + y) - f x = integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) y)" (is ?th1)
+proof -
+ from assms have subset: "(\<lambda>xa. x + xa *\<^sub>R y) ` {0..1} \<subseteq> S" by auto
+ note [derivative_intros] =
+ has_derivative_subset[OF _ subset]
+ has_derivative_in_compose[where f="(\<lambda>xa. x + xa *\<^sub>R y)" and g = f]
+ note [continuous_intros] =
+ continuous_on_compose2[where f="(\<lambda>xa. x + xa *\<^sub>R y)"]
+ continuous_on_subset[OF _ subset]
+ have "\<And>t. t \<in> {0..1} \<Longrightarrow>
+ ((\<lambda>t. f (x + t *\<^sub>R y)) has_vector_derivative f' (x + t *\<^sub>R y) y)
+ (at t within {0..1})"
+ using assms
+ by (auto simp: has_vector_derivative_def
+ linear_cmul[OF has_derivative_linear[OF f'], symmetric]
+ intro!: derivative_eq_intros)
+ from fundamental_theorem_of_calculus[rule_format, OF _ this]
+ show ?th1
+ by (auto intro!: integral_unique[symmetric])
+qed
+
lemma (in bounded_bilinear) sum_prod_derivatives_has_vector_derivative:
assumes "p>0"
and f0: "Df 0 = f"
@@ -2835,7 +2873,6 @@
qed
-
subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
proposition division_of_nontrivial:
@@ -3024,6 +3061,21 @@
unfolding integrable_on_def
by (auto intro!: has_integral_combine)
+lemma integral_minus_sets:
+ fixes f::"real \<Rightarrow> 'a::banach"
+ shows "c \<le> a \<Longrightarrow> c \<le> b \<Longrightarrow> f integrable_on {c .. max a b} \<Longrightarrow>
+ integral {c .. a} f - integral {c .. b} f =
+ (if a \<le> b then - integral {a .. b} f else integral {b .. a} f)"
+ using integral_combine[of c a b f] integral_combine[of c b a f]
+ by (auto simp: algebra_simps max_def)
+
+lemma integral_minus_sets':
+ fixes f::"real \<Rightarrow> 'a::banach"
+ shows "c \<ge> a \<Longrightarrow> c \<ge> b \<Longrightarrow> f integrable_on {min a b .. c} \<Longrightarrow>
+ integral {a .. c} f - integral {b .. c} f =
+ (if a \<le> b then integral {a .. b} f else - integral {b .. a} f)"
+ using integral_combine[of b a c f] integral_combine[of a b c f]
+ by (auto simp: algebra_simps min_def)
subsection \<open>Reduce integrability to "local" integrability.\<close>
@@ -3129,13 +3181,19 @@
using assms integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]
by (fastforce simp: continuous_on_eq_continuous_within)
+lemma integral_has_real_derivative:
+ assumes "continuous_on {a..b} g"
+ 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)
+
lemma antiderivative_continuous:
fixes q b :: real
assumes "continuous_on {a..b} f"
obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
using integral_has_vector_derivative[OF assms] by auto
-
subsection \<open>Combined fundamental theorem of calculus.\<close>
lemma antiderivative_integral_continuous:
@@ -3149,7 +3207,8 @@
have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
proof -
have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
- by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
+ by (metis atLeastAtMost_iff atLeastatMost_subset_iff box_real(2) g
+ has_vector_derivative_within_subset subsetCE that(1,2))
then show ?thesis
by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
qed
@@ -4125,6 +4184,28 @@
by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous_1 assms)
qed
+theorem integral_has_vector_derivative':
+ fixes f :: "real \<Rightarrow> 'b::banach"
+ assumes "continuous_on {a..b} f"
+ and "x \<in> {a..b}"
+ shows "((\<lambda>u. integral {u..b} f) has_vector_derivative - f x) (at x within {a..b})"
+proof -
+ have *: "integral {x..b} f = integral {a .. b} f - integral {a .. x} f" if "a \<le> x" "x \<le> b" for x
+ using integral_combine[of a x b for x, OF that integrable_continuous_real[OF assms(1)]]
+ by (simp add: algebra_simps)
+ show ?thesis
+ using \<open>x \<in> _\<close> *
+ by (rule has_vector_derivative_transform)
+ (auto intro!: derivative_eq_intros assms integral_has_vector_derivative)
+qed
+
+lemma integral_has_real_derivative':
+ assumes "continuous_on {a..b} g"
+ 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)
+
subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
@@ -4661,6 +4742,10 @@
shows "f integrable_on S \<longleftrightarrow> f integrable_on T"
by (blast intro: integrable_spike_set assms negligible_subset)
+lemma integrable_on_insert_iff: "f integrable_on (insert x X) \<longleftrightarrow> f integrable_on X"
+ for f::"_ \<Rightarrow> 'a::banach"
+ by (rule integrable_spike_set_eq) (auto simp: insert_Diff_if)
+
lemma has_integral_interior:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
@@ -5136,7 +5221,7 @@
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes \<T>: "finite \<T>"
and int: "\<And>S. S \<in> \<T> \<Longrightarrow> (f has_integral (i S)) S"
- and neg: "\<And>S S'. \<lbrakk>S \<in> \<T>; S' \<in> \<T>; S \<noteq> S'\<rbrakk> \<Longrightarrow> negligible (S \<inter> S')"
+ and neg: "pairwise (\<lambda>S S'. negligible (S \<inter> S')) \<T>"
shows "(f has_integral (sum i \<T>)) (\<Union>\<T>)"
proof -
let ?\<U> = "((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> \<T> \<and> b \<in> {y. y \<in> \<T> \<and> a \<noteq> y}})"
@@ -5151,7 +5236,7 @@
ultimately show "finite ?\<U>"
by (blast intro: finite_subset[of _ "\<T> \<times> \<T>"])
show "\<And>t. t \<in> ?\<U> \<Longrightarrow> negligible t"
- using neg by auto
+ using neg unfolding pairwise_def by auto
qed
next
show "(if x \<in> \<Union>\<T> then f x else 0) = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
@@ -5162,7 +5247,7 @@
using that by blast
ultimately show "f x = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
by (simp add: sum.delta[OF \<T>])
- qed
+ qed
next
show "((\<lambda>x. \<Sum>A\<in>\<T>. if x \<in> A then f x else 0) has_integral (\<Sum>A\<in>\<T>. i A)) UNIV"
apply (rule has_integral_sum [OF \<T>])
@@ -5192,7 +5277,7 @@
qed
show ?thesis
unfolding \<D>(6)[symmetric]
- by (auto intro: \<D> neg assms has_integral_Union)
+ by (auto intro: \<D> neg assms has_integral_Union pairwiseI)
qed
lemma integral_combine_division_bottomup:
@@ -6049,6 +6134,26 @@
qed
qed
+lemma continuous_on_imp_absolutely_integrable_on:
+ fixes f::"real \<Rightarrow> 'a::banach"
+ shows "continuous_on {a..b} f \<Longrightarrow>
+ norm (integral {a..b} f) \<le> integral {a..b} (\<lambda>x. norm (f x))"
+ by (intro integral_norm_bound_integral integrable_continuous_real continuous_on_norm) auto
+
+lemma integral_bound:
+ fixes f::"real \<Rightarrow> 'a::banach"
+ assumes "a \<le> b"
+ assumes "continuous_on {a .. b} f"
+ assumes "\<And>t. t \<in> {a .. b} \<Longrightarrow> norm (f t) \<le> B"
+ shows "norm (integral {a .. b} f) \<le> B * (b - a)"
+proof -
+ note continuous_on_imp_absolutely_integrable_on[OF assms(2)]
+ also have "integral {a..b} (\<lambda>x. norm (f x)) \<le> integral {a..b} (\<lambda>_. B)"
+ by (rule integral_le)
+ (auto intro!: integrable_continuous_real continuous_intros assms)
+ also have "\<dots> = B * (b - a)" using assms by simp
+ finally show ?thesis .
+qed
lemma integral_norm_bound_integral_component:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
--- a/src/HOL/Analysis/L2_Norm.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy Fri Feb 23 15:17:51 2018 +0100
@@ -98,13 +98,6 @@
qed
qed
-lemma sqrt_sum_squares_le_sum:
- "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
- apply (rule power2_le_imp_le)
- apply (simp add: power2_sum)
- apply simp
- done
-
lemma L2_set_le_sum [rule_format]:
"(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
apply (cases "finite A")
--- a/src/HOL/Analysis/Linear_Algebra.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Fri Feb 23 15:17:51 2018 +0100
@@ -2987,10 +2987,6 @@
lemma infnorm_le_norm: "infnorm x \<le> norm x"
by (simp add: Basis_le_norm infnorm_Max)
-lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
- by (subst (1 2) euclidean_representation [symmetric])
- (simp add: inner_sum_right inner_Basis ac_simps)
-
lemma norm_le_infnorm:
fixes x :: "'a::euclidean_space"
shows "norm x \<le> sqrt DIM('a) * infnorm x"
--- a/src/HOL/Analysis/Operator_Norm.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Operator_Norm.thy Fri Feb 23 15:17:51 2018 +0100
@@ -235,4 +235,13 @@
shows "onorm (\<lambda>x. f x + g x) < e"
using assms by (rule onorm_triangle [THEN order_le_less_trans])
+lemma onorm_sum:
+ assumes "finite S"
+ assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
+ shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
+ using assms
+ by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
+
+lemmas onorm_sum_le = onorm_sum[THEN order_trans]
+
end
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Fri Feb 23 15:17:51 2018 +0100
@@ -214,9 +214,20 @@
using image_smult_cbox[of m a b]
by (simp add: cbox_interval)
-lemma is_interval_closed_interval [simp]:
- "is_interval {a .. (b::'a::ordered_euclidean_space)}"
- by (metis cbox_interval is_interval_cbox)
+lemma [simp]:
+ fixes a b::"'a::ordered_euclidean_space" and r s::real
+ shows is_interval_io: "is_interval {..<r}"
+ and is_interval_ic: "is_interval {..a}"
+ and is_interval_oi: "is_interval {r<..}"
+ and is_interval_ci: "is_interval {a..}"
+ and is_interval_oo: "is_interval {r<..<s}"
+ and is_interval_oc: "is_interval {r<..s}"
+ and is_interval_co: "is_interval {r..<s}"
+ and is_interval_cc: "is_interval {b..a}"
+ by (force simp: is_interval_def eucl_le[where 'a='a])+
+
+lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
+ by (auto simp: real_atLeastGreaterThan_eq)
lemma compact_interval [simp]:
fixes a b::"'a::ordered_euclidean_space"
--- a/src/HOL/Analysis/Product_Vector.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy Fri Feb 23 15:17:51 2018 +0100
@@ -306,6 +306,11 @@
by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
qed simp
+lemma differentiable_Pair [simp, derivative_intros]:
+ "f differentiable at x within s \<Longrightarrow> g differentiable at x within s \<Longrightarrow>
+ (\<lambda>x. (f x, g x)) differentiable at x within s"
+ unfolding differentiable_def by (blast intro: has_derivative_Pair)
+
lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
@@ -313,6 +318,17 @@
"((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
unfolding split_beta' .
+
+subsubsection \<open>Vector derivatives involving pairs\<close>
+
+lemma has_vector_derivative_Pair[derivative_intros]:
+ assumes "(f has_vector_derivative f') (at x within s)"
+ "(g has_vector_derivative g') (at x within s)"
+ shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
+ using assms
+ by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
+
+
subsection \<open>Product is an inner product space\<close>
instantiation prod :: (real_inner, real_inner) real_inner
@@ -368,4 +384,9 @@
lemma norm_snd_le: "norm y \<le> norm (x,y)"
by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
+lemma norm_Pair_le:
+ shows "norm (x, y) \<le> norm x + norm y"
+ unfolding norm_Pair
+ by (metis norm_ge_zero sqrt_sum_squares_le_sum)
+
end
--- a/src/HOL/Analysis/Riemann_Mapping.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Fri Feb 23 15:17:51 2018 +0100
@@ -489,7 +489,7 @@
let ?g = "\<lambda>z. (SOME g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = a \<and> pathfinish g = z)"
show "((\<lambda>z. contour_integral (?g z) f) has_field_derivative f x)
(at x)"
- proof (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right, rule Lim_transform)
+ proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
show "(\<lambda>y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \<midarrow>x\<rightarrow> 0"
proof (clarsimp simp add: Lim_at)
fix e::real assume "e > 0"
--- a/src/HOL/Analysis/Starlike.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Fri Feb 23 15:17:51 2018 +0100
@@ -13,9 +13,87 @@
begin
+subsection \<open>Midpoint\<close>
+
definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
+lemma midpoint_idem [simp]: "midpoint x x = x"
+ unfolding midpoint_def
+ unfolding scaleR_right_distrib
+ unfolding scaleR_left_distrib[symmetric]
+ by auto
+
+lemma midpoint_sym: "midpoint a b = midpoint b a"
+ unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
+
+lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
+proof -
+ have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
+ by simp
+ then show ?thesis
+ unfolding midpoint_def scaleR_2 [symmetric] by simp
+qed
+
+lemma
+ fixes a::real
+ assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
+ and le_midpoint_1: "midpoint a b \<le> b"
+ by (simp_all add: midpoint_def assms)
+
+lemma dist_midpoint:
+ fixes a b :: "'a::real_normed_vector" shows
+ "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
+ "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
+ "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
+ "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
+proof -
+ have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
+ unfolding equation_minus_iff by auto
+ have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2"
+ by auto
+ note scaleR_right_distrib [simp]
+ show ?t1
+ unfolding midpoint_def dist_norm
+ apply (rule **)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t2
+ unfolding midpoint_def dist_norm
+ apply (rule *)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t3
+ unfolding midpoint_def dist_norm
+ apply (rule *)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t4
+ unfolding midpoint_def dist_norm
+ apply (rule **)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+qed
+
+lemma midpoint_eq_endpoint [simp]:
+ "midpoint a b = a \<longleftrightarrow> a = b"
+ "midpoint a b = b \<longleftrightarrow> a = b"
+ unfolding midpoint_eq_iff by auto
+
+lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
+ using midpoint_eq_iff by metis
+
+lemma midpoint_linear_image:
+ "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
+by (simp add: linear_iff midpoint_def)
+
+
+subsection \<open>Line segments\<close>
+
definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
@@ -106,86 +184,6 @@
apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
using of_real_eq_iff by fastforce
-lemma midpoint_idem [simp]: "midpoint x x = x"
- unfolding midpoint_def
- unfolding scaleR_right_distrib
- unfolding scaleR_left_distrib[symmetric]
- by auto
-
-lemma midpoint_sym: "midpoint a b = midpoint b a"
- unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
-
-lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
-proof -
- have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
- by simp
- then show ?thesis
- unfolding midpoint_def scaleR_2 [symmetric] by simp
-qed
-
-lemma
- fixes a::real
- assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
- and le_midpoint_1: "midpoint a b \<le> b"
- by (simp_all add: midpoint_def assms)
-
-lemma dist_midpoint:
- fixes a b :: "'a::real_normed_vector" shows
- "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
- "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
- "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
- "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
-proof -
- have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
- unfolding equation_minus_iff by auto
- have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2"
- by auto
- note scaleR_right_distrib [simp]
- show ?t1
- unfolding midpoint_def dist_norm
- apply (rule **)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t2
- unfolding midpoint_def dist_norm
- apply (rule *)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t3
- unfolding midpoint_def dist_norm
- apply (rule *)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t4
- unfolding midpoint_def dist_norm
- apply (rule **)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
-qed
-
-lemma midpoint_eq_endpoint [simp]:
- "midpoint a b = a \<longleftrightarrow> a = b"
- "midpoint a b = b \<longleftrightarrow> a = b"
- unfolding midpoint_eq_iff by auto
-
-lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
- using midpoint_eq_iff by metis
-
-lemma midpoint_linear_image:
- "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
-by (simp add: linear_iff midpoint_def)
-
-subsection\<open>Starlike sets\<close>
-
-definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
-
-lemma starlike_UNIV [simp]: "starlike UNIV"
- by (simp add: starlike_def)
-
lemma convex_contains_segment:
"convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
unfolding convex_alt closed_segment_def by auto
@@ -197,10 +195,6 @@
"\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
using convex_contains_segment by blast
-lemma convex_imp_starlike:
- "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
- unfolding convex_contains_segment starlike_def by auto
-
lemma segment_convex_hull:
"closed_segment a b = convex hull {a,b}"
proof -
@@ -349,7 +343,7 @@
proof -
have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
using \<open>u \<le> 1\<close> by force
- then show ?thesis
+ then show ?thesis
by (simp add: dist_norm real_vector.scale_right_diff_distrib)
qed
also have "... \<le> dist a b"
@@ -581,7 +575,6 @@
by (metis image_comp convex_translation)
qed
-
lemmas convex_segment = convex_closed_segment convex_open_segment
lemma connected_segment [iff]:
@@ -589,6 +582,33 @@
shows "connected (closed_segment x y)"
by (simp add: convex_connected)
+lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
+ by (auto simp: is_interval_convex_1)
+
+lemma IVT'_closed_segment_real:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "y \<in> closed_segment (f a) (f b)"
+ assumes "continuous_on (closed_segment a b) f"
+ shows "\<exists>x \<in> closed_segment a b. f x = y"
+ using IVT'[of f a y b]
+ IVT'[of "-f" a "-y" b]
+ IVT'[of f b y a]
+ IVT'[of "-f" b "-y" a] assms
+ by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
+
+
+subsection\<open>Starlike sets\<close>
+
+definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+
+lemma starlike_UNIV [simp]: "starlike UNIV"
+ by (simp add: starlike_def)
+
+lemma convex_imp_starlike:
+ "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
+ unfolding convex_contains_segment starlike_def by auto
+
+
lemma affine_hull_closed_segment [simp]:
"affine hull (closed_segment a b) = affine hull {a,b}"
by (simp add: segment_convex_hull)
@@ -7261,6 +7281,66 @@
with assms show ?thesis by auto
qed
+lemma vector_in_orthogonal_spanningset:
+ fixes a :: "'a::euclidean_space"
+ obtains S where "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+ by (metis UNIV_I Un_iff empty_iff insert_subset orthogonal_extension pairwise_def pairwise_orthogonal_insert span_UNIV subsetI subset_antisym)
+
+lemma vector_in_orthogonal_basis:
+ fixes a :: "'a::euclidean_space"
+ assumes "a \<noteq> 0"
+ obtains S where "a \<in> S" "0 \<notin> S" "pairwise orthogonal S" "independent S" "finite S"
+ "span S = UNIV" "card S = DIM('a)"
+proof -
+ obtain S where S: "a \<in> S" "pairwise orthogonal S" "span S = UNIV"
+ using vector_in_orthogonal_spanningset .
+ show thesis
+ proof
+ show "pairwise orthogonal (S - {0})"
+ using pairwise_mono S(2) by blast
+ show "independent (S - {0})"
+ by (simp add: \<open>pairwise orthogonal (S - {0})\<close> pairwise_orthogonal_independent)
+ show "finite (S - {0})"
+ using \<open>independent (S - {0})\<close> independent_finite by blast
+ show "card (S - {0}) = DIM('a)"
+ using span_delete_0 [of S] S
+ by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span)
+ qed (use S \<open>a \<noteq> 0\<close> in auto)
+qed
+
+lemma vector_in_orthonormal_basis:
+ fixes a :: "'a::euclidean_space"
+ assumes "norm a = 1"
+ obtains S where "a \<in> S" "pairwise orthogonal S" "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
+ "independent S" "card S = DIM('a)" "span S = UNIV"
+proof -
+ have "a \<noteq> 0"
+ using assms by auto
+ then obtain S where "a \<in> S" "0 \<notin> S" "finite S"
+ and S: "pairwise orthogonal S" "independent S" "span S = UNIV" "card S = DIM('a)"
+ by (metis vector_in_orthogonal_basis)
+ let ?S = "(\<lambda>x. x /\<^sub>R norm x) ` S"
+ show thesis
+ proof
+ show "a \<in> ?S"
+ using \<open>a \<in> S\<close> assms image_iff by fastforce
+ next
+ show "pairwise orthogonal ?S"
+ using \<open>pairwise orthogonal S\<close> by (auto simp: pairwise_def orthogonal_def)
+ show "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` S \<Longrightarrow> norm x = 1"
+ using \<open>0 \<notin> S\<close> by (auto simp: divide_simps)
+ then show "independent ?S"
+ by (metis \<open>pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` S)\<close> norm_zero pairwise_orthogonal_independent zero_neq_one)
+ have "inj_on (\<lambda>x. x /\<^sub>R norm x) S"
+ unfolding inj_on_def
+ by (metis (full_types) S(1) \<open>0 \<notin> S\<close> inverse_nonzero_iff_nonzero norm_eq_zero orthogonal_scaleR orthogonal_self pairwise_def)
+ then show "card ?S = DIM('a)"
+ by (simp add: card_image S)
+ show "span ?S = UNIV"
+ by (metis (no_types) \<open>0 \<notin> S\<close> \<open>finite S\<close> \<open>span S = UNIV\<close> field_class.field_inverse_zero inverse_inverse_eq less_irrefl span_image_scale zero_less_norm_iff)
+ qed
+qed
+
proposition dim_orthogonal_sum:
fixes A :: "'a::euclidean_space set"
assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Feb 23 15:17:51 2018 +0100
@@ -7,7 +7,7 @@
section \<open>Elementary topology in Euclidean space.\<close>
theory Topology_Euclidean_Space
-imports
+imports
"HOL-Library.Indicator_Function"
"HOL-Library.Countable_Set"
"HOL-Library.FuncSet"
@@ -1112,6 +1112,9 @@
lemma ball_subset_cball [simp, intro]: "ball x e \<subseteq> cball x e"
by (simp add: subset_eq)
+lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
+ by (auto simp: mem_ball mem_cball)
+
lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
by force
@@ -1124,6 +1127,22 @@
lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
by (simp add: subset_eq)
+lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
+ by (auto simp: mem_ball mem_cball)
+
+lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
+ by (auto simp: mem_ball mem_cball)
+
+lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
+ unfolding mem_cball
+proof -
+ have "dist z x \<le> dist z y + dist y x"
+ by (rule dist_triangle)
+ also assume "dist z y \<le> b"
+ also assume "dist y x \<le> a"
+ finally show "dist z x \<le> b + a" by arith
+qed
+
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
by (simp add: set_eq_iff) arith
@@ -1253,6 +1272,17 @@
unfolding dist_norm norm_eq_sqrt_inner L2_set_def
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
+lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
+proof -
+ have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
+ by simp
+ also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
+ by (intro sum_mono2) (auto simp: that)
+ finally show ?thesis
+ unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
+ by (auto intro!: real_le_rsqrt)
+qed
+
lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
by (rule eventually_nhds_in_open) simp_all
@@ -1262,6 +1292,20 @@
lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
+lemma at_within_ball: "e > 0 \<Longrightarrow> dist x y < e \<Longrightarrow> at y within ball x e = at y"
+ by (subst at_within_open) auto
+
+lemma atLeastAtMost_eq_cball:
+ fixes a b::real
+ shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
+ by (auto simp: dist_real_def field_simps mem_cball)
+
+lemma greaterThanLessThan_eq_ball:
+ fixes a b::real
+ shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
+ by (auto simp: dist_real_def field_simps mem_ball)
+
+
subsection \<open>Boxes\<close>
abbreviation One :: "'a::euclidean_space"
@@ -1834,6 +1878,14 @@
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
+lemma is_interval_1:
+ "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
+ unfolding is_interval_def by auto
+
+lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
+ unfolding is_interval_def
+ by blast
+
lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
@@ -1916,6 +1968,88 @@
by blast
qed
+lemma is_real_interval_union:
+ "is_interval (X \<union> Y)"
+ if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
+ for X Y::"real set"
+proof -
+ consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
+ then show ?thesis
+ proof cases
+ case 1
+ then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
+ by blast
+ then show ?thesis
+ using I 1 X Y unfolding is_interval_1
+ by (metis (full_types) Un_iff le_cases)
+ qed (use that in auto)
+qed
+
+lemma is_interval_translationI:
+ assumes "is_interval X"
+ shows "is_interval ((+) x ` X)"
+ unfolding is_interval_def
+proof safe
+ fix b d e
+ assume "b \<in> X" "d \<in> X"
+ "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
+ (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
+ hence "e - x \<in> X"
+ by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
+ (auto simp: algebra_simps)
+ thus "e \<in> (+) x ` X" by force
+qed
+
+lemma is_interval_uminusI:
+ assumes "is_interval X"
+ shows "is_interval (uminus ` X)"
+ unfolding is_interval_def
+proof safe
+ fix b d e
+ assume "b \<in> X" "d \<in> X"
+ "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
+ (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
+ hence "- e \<in> X"
+ by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
+ (auto simp: algebra_simps)
+ thus "e \<in> uminus ` X" by force
+qed
+
+lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
+ using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
+ by (auto simp: image_image)
+
+lemma is_interval_neg_translationI:
+ assumes "is_interval X"
+ shows "is_interval ((-) x ` X)"
+proof -
+ have "(-) x ` X = (+) x ` uminus ` X"
+ by (force simp: algebra_simps)
+ also have "is_interval \<dots>"
+ by (metis is_interval_uminusI is_interval_translationI assms)
+ finally show ?thesis .
+qed
+
+lemma is_interval_translation[simp]:
+ "is_interval ((+) x ` X) = is_interval X"
+ using is_interval_neg_translationI[of "(+) x ` X" x]
+ by (auto intro!: is_interval_translationI simp: image_image)
+
+lemma is_interval_minus_translation[simp]:
+ shows "is_interval ((-) x ` X) = is_interval X"
+proof -
+ have "(-) x ` X = (+) x ` uminus ` X"
+ by (force simp: algebra_simps)
+ also have "is_interval \<dots> = is_interval X"
+ by simp
+ finally show ?thesis .
+qed
+
+lemma is_interval_minus_translation'[simp]:
+ shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
+ using is_interval_translation[of "-c" X]
+ by (metis image_cong uminus_add_conv_diff)
+
subsection \<open>Limit points\<close>
@@ -2629,6 +2763,15 @@
lemma not_trivial_limit_within: "\<not> trivial_limit (at x within S) = (x \<in> closure (S - {x}))"
using islimpt_in_closure by (metis trivial_limit_within)
+lemma not_in_closure_trivial_limitI:
+ "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
+ using not_trivial_limit_within[of x s]
+ by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
+
+lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
+ if "x \<in> closure s \<Longrightarrow> filterlim f l (at x within s)"
+ by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
+
lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
using not_trivial_limit_within[of c A] by blast
@@ -3229,6 +3372,28 @@
qed
qed
+lemma tendsto_If_within_closures:
+ assumes f: "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (f \<longlongrightarrow> l x) (at x within s \<union> (closure s \<inter> closure t))"
+ assumes g: "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (g \<longlongrightarrow> l x) (at x within t \<union> (closure s \<inter> closure t))"
+ assumes "x \<in> s \<union> t"
+ shows "((\<lambda>x. if x \<in> s then f x else g x) \<longlongrightarrow> l x) (at x within s \<union> t)"
+proof -
+ have *: "(s \<union> t) \<inter> {x. x \<in> s} = s" "(s \<union> t) \<inter> {x. x \<notin> s} = t - s"
+ by auto
+ have "(f \<longlongrightarrow> l x) (at x within s)"
+ by (rule filterlim_at_within_closure_implies_filterlim)
+ (use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
+ moreover
+ have "(g \<longlongrightarrow> l x) (at x within t - s)"
+ by (rule filterlim_at_within_closure_implies_filterlim)
+ (use \<open>x \<in> _\<close> in
+ \<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
+ ultimately show ?thesis
+ by (intro filterlim_at_within_If) (simp_all only: *)
+qed
+
subsection \<open>Boundedness\<close>
@@ -3487,12 +3652,26 @@
using assms by (fastforce simp: bounded_iff)
qed
+lemma bounded_plus:
+ fixes S ::"'a::real_normed_vector set"
+ assumes "bounded S" "bounded T"
+ shows "bounded ((\<lambda>(x,y). x + y) ` (S \<times> T))"
+ using bounded_plus_comp [of fst "S \<times> T" snd] assms
+ by (auto simp: split_def split: if_split_asm)
+
lemma bounded_minus_comp:
"bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
for f g::"'a \<Rightarrow> 'b::real_normed_vector"
using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
by auto
+lemma bounded_minus:
+ fixes S ::"'a::real_normed_vector set"
+ assumes "bounded S" "bounded T"
+ shows "bounded ((\<lambda>(x,y). x - y) ` (S \<times> T))"
+ using bounded_minus_comp [of fst "S \<times> T" snd] assms
+ by (auto simp: split_def split: if_split_asm)
+
subsection \<open>Compactness\<close>
@@ -3849,7 +4028,6 @@
\<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
by (metis Int_Diff open_delete openin_open)
-
text\<open>Compactness expressed with filters\<close>
lemma closure_iff_nhds_not_empty:
@@ -4478,6 +4656,27 @@
shows "~ compact (UNIV::'a set)"
by (simp add: compact_eq_bounded_closed)
+text\<open>Representing sets as the union of a chain of compact sets.\<close>
+lemma closed_Union_compact_subsets:
+ fixes S :: "'a::{heine_borel,real_normed_vector} set"
+ assumes "closed S"
+ obtains F where "\<And>n. compact(F n)" "\<And>n. F n \<subseteq> S" "\<And>n. F n \<subseteq> F(Suc n)"
+ "(\<Union>n. F n) = S" "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. K \<subseteq> F n"
+proof
+ show "compact (S \<inter> cball 0 (of_nat n))" for n
+ using assms compact_eq_bounded_closed by auto
+next
+ show "(\<Union>n. S \<inter> cball 0 (real n)) = S"
+ by (auto simp: real_arch_simple)
+next
+ fix K :: "'a set"
+ assume "compact K" "K \<subseteq> S"
+ then obtain N where "K \<subseteq> cball 0 N"
+ by (meson bounded_pos mem_cball_0 compact_imp_bounded subsetI)
+ then show "\<exists>N. \<forall>n\<ge>N. K \<subseteq> S \<inter> cball 0 (real n)"
+ by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
+qed auto
+
instance real :: heine_borel
proof
fix f :: "nat \<Rightarrow> real"
@@ -4897,10 +5096,7 @@
lemma continuous_within_eps_delta:
"continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)"
- unfolding continuous_within and Lim_within
- apply auto
- apply (metis dist_nz dist_self, blast)
- done
+ unfolding continuous_within and Lim_within by fastforce
corollary continuous_at_eps_delta:
"continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
--- a/src/HOL/Analysis/Uniform_Limit.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Fri Feb 23 15:17:51 2018 +0100
@@ -438,6 +438,7 @@
bounded_linear.uniform_limit[OF bounded_linear_mult_right]
bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
+
lemmas uniform_limit_uminus[uniform_limit_intros] =
bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
@@ -728,5 +729,7 @@
apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
using sm sums_unique by fastforce
+lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
+
end
--- a/src/HOL/Deriv.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Deriv.thy Fri Feb 23 15:17:51 2018 +0100
@@ -26,6 +26,13 @@
most cases @{term s} is either a variable or @{term UNIV}.
\<close>
+text \<open>These are the only cases we'll care about, probably.\<close>
+
+lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
+ bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
+ unfolding has_derivative_def tendsto_iff
+ by (subst eventually_Lim_ident_at) (auto simp add: field_simps)
+
lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
by simp
@@ -189,6 +196,52 @@
lemmas has_derivative_within_subset = has_derivative_subset
+lemma has_derivative_within_singleton_iff:
+ "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g"
+ by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)
+
+
+subsubsection \<open>Limit transformation for derivatives\<close>
+
+lemma has_derivative_transform_within:
+ assumes "(f has_derivative f') (at x within s)"
+ and "0 < d"
+ and "x \<in> s"
+ and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
+ shows "(g has_derivative f') (at x within s)"
+ using assms
+ unfolding has_derivative_within
+ by (force simp add: intro: Lim_transform_within)
+
+lemma has_derivative_transform_within_open:
+ assumes "(f has_derivative f') (at x within t)"
+ and "open s"
+ and "x \<in> s"
+ and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
+ shows "(g has_derivative f') (at x within t)"
+ using assms unfolding has_derivative_within
+ by (force simp add: intro: Lim_transform_within_open)
+
+lemma has_derivative_transform:
+ assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+ assumes "(f has_derivative f') (at x within s)"
+ shows "(g has_derivative f') (at x within s)"
+ using assms
+ by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto
+
+lemma has_derivative_transform_eventually:
+ assumes "(f has_derivative f') (at x within s)"
+ "(\<forall>\<^sub>F x' in at x within s. f x' = g x')"
+ assumes "f x = g x" "x \<in> s"
+ shows "(g has_derivative f') (at x within s)"
+ using assms
+proof -
+ from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'"
+ by (force simp: eventually_at)
+ from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)]
+ show ?thesis .
+qed
+
subsection \<open>Continuity\<close>
@@ -295,6 +348,14 @@
((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
by (blast intro: has_derivative_in_compose has_derivative_subset)
+lemma has_derivative_in_compose2:
+ assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
+ assumes "f ` s \<subseteq> t" "x \<in> s"
+ assumes "(f has_derivative f') (at x within s)"
+ shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)"
+ using assms
+ by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g])
+
lemma (in bounded_bilinear) FDERIV:
assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
@@ -467,6 +528,10 @@
all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>.
\<close>
+lemma has_derivative_at2: "(f has_derivative f') (at x) \<longleftrightarrow>
+ bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
+ using has_derivative_within [of f f' x UNIV]
+ by simp
lemma has_derivative_zero_unique:
assumes "((\<lambda>x. 0) has_derivative F) (at x)"
shows "F = (\<lambda>h. 0)"
@@ -542,10 +607,19 @@
(\<lambda>x. f (g x)) differentiable (at x within s)"
by (blast intro: differentiable_in_compose differentiable_subset)
-lemma differentiable_sum [simp, derivative_intros]:
+lemma differentiable_add [simp, derivative_intros]:
"f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_add)
+lemma differentiable_sum[simp, derivative_intros]:
+ assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
+ shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net"
+proof -
+ from bchoice[OF assms(2)[unfolded differentiable_def]]
+ show ?thesis
+ by (auto intro!: has_derivative_sum simp: differentiable_def)
+qed
+
lemma differentiable_minus [simp, derivative_intros]:
"f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_minus)
@@ -651,6 +725,14 @@
for c :: "'a::ab_semigroup_mult"
by (simp add: fun_eq_iff mult.commute)
+lemma DERIV_compose_FDERIV:
+ fixes f::"real\<Rightarrow>real"
+ assumes "DERIV f (g x) :> f'"
+ assumes "(g has_derivative g') (at x within s)"
+ shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
+ using assms has_derivative_compose[of g g' x s f "( * ) f'"]
+ by (auto simp: has_field_derivative_def ac_simps)
+
subsection \<open>Vector derivative\<close>
@@ -998,6 +1080,8 @@
by eventually_elim auto
qed
+lemmas has_derivative_floor[derivative_intros] =
+ floor_has_real_derivative[THEN DERIV_compose_FDERIV]
text \<open>Caratheodory formulation of derivative at a point\<close>
--- a/src/HOL/Groups_Big.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Groups_Big.thy Fri Feb 23 15:17:51 2018 +0100
@@ -332,34 +332,6 @@
by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
qed
-lemma delta [simp]:
- assumes fS: "finite S"
- shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
-proof -
- let ?f = "(\<lambda>k. if k = a then b k else \<^bold>1)"
- show ?thesis
- proof (cases "a \<in> S")
- case False
- then have "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
- with False show ?thesis by simp
- next
- case True
- let ?A = "S - {a}"
- let ?B = "{a}"
- from True have eq: "S = ?A \<union> ?B" by blast
- have dj: "?A \<inter> ?B = {}" by simp
- from fS have fAB: "finite ?A" "finite ?B" by auto
- have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
- using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
- with True show ?thesis by simp
- qed
-qed
-
-lemma delta' [simp]:
- assumes fin: "finite S"
- shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
- using delta [OF fin, of a b, symmetric] by (auto intro: cong)
-
lemma delta_remove:
assumes fS: "finite S"
shows "F (\<lambda>k. if k = a then b k else c k) S = (if a \<in> S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))"
@@ -384,6 +356,16 @@
qed
qed
+lemma delta [simp]:
+ assumes fS: "finite S"
+ shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+ by (simp add: delta_remove [OF assms])
+
+lemma delta' [simp]:
+ assumes fin: "finite S"
+ shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
+ using delta [OF fin, of a b, symmetric] by (auto intro: cong)
+
lemma If_cases:
fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
assumes fin: "finite A"
--- a/src/HOL/Library/Extended_Nat.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Fri Feb 23 15:17:51 2018 +0100
@@ -383,6 +383,8 @@
by (simp split: enat.splits)
show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat
by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto
+ show "a < b \<Longrightarrow> a + 1 < b + 1"
+ by (metis add_right_mono eSuc_minus_1 eSuc_plus_1 less_le)
qed (simp add: zero_enat_def one_enat_def)
(* BH: These equations are already proven generally for any type in
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Feb 23 15:17:51 2018 +0100
@@ -11,7 +11,7 @@
lemma ereal_ineq_diff_add:
assumes "b \<noteq> (-\<infinity>::ereal)" "a \<ge> b"
shows "a = b + (a-b)"
-by (metis add.commute assms(1) assms(2) ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
+by (metis add.commute assms ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
lemma Limsup_const_add:
fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
@@ -345,7 +345,11 @@
(transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
instance ennreal :: linordered_nonzero_semiring
- proof qed (transfer; simp)
+proof
+ fix a b::ennreal
+ show "a < b \<Longrightarrow> a + 1 < b + 1"
+ by transfer (simp add: add_right_mono ereal_add_cancel_right less_le)
+qed (transfer; simp)
instance ennreal :: strict_ordered_ab_semigroup_add
proof
--- a/src/HOL/Library/Extended_Real.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Feb 23 15:17:51 2018 +0100
@@ -1800,8 +1800,176 @@
lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
by (metis max_bot2 bot_ereal_def)
-
-subsubsection "Topological space"
+subsection \<open>Extended real intervals\<close>
+
+lemma real_greaterThanLessThan_infinity_eq:
+ "real_of_ereal ` {N::ereal<..<\<infinity>} =
+ (if N = \<infinity> then {} else if N = -\<infinity> then UNIV else {real_of_ereal N<..})"
+proof -
+ {
+ fix x::real
+ have "x \<in> real_of_ereal ` {- \<infinity><..<\<infinity>::ereal}"
+ by (auto intro!: image_eqI[where x="ereal x"])
+ } moreover {
+ fix x::ereal
+ assume "N \<noteq> - \<infinity>" "N < x" "x \<noteq> \<infinity>"
+ then have "real_of_ereal N < real_of_ereal x"
+ by (cases N; cases x; simp)
+ } moreover {
+ fix x::real
+ assume "N \<noteq> \<infinity>" "real_of_ereal N < x"
+ then have "x \<in> real_of_ereal ` {N<..<\<infinity>}"
+ by (cases N) (auto intro!: image_eqI[where x="ereal x"])
+ } ultimately show ?thesis by auto
+qed
+
+lemma real_greaterThanLessThan_minus_infinity_eq:
+ "real_of_ereal ` {-\<infinity><..<N::ereal} =
+ (if N = \<infinity> then UNIV else if N = -\<infinity> then {} else {..<real_of_ereal N})"
+proof -
+ have "real_of_ereal ` {-\<infinity><..<N::ereal} = uminus ` real_of_ereal ` {-N<..<\<infinity>}"
+ by (auto simp: ereal_uminus_less_reorder intro!: image_eqI[where x="-x" for x])
+ also note real_greaterThanLessThan_infinity_eq
+ finally show ?thesis by (auto intro!: image_eqI[where x="-x" for x])
+qed
+
+lemma real_greaterThanLessThan_inter:
+ "real_of_ereal ` {N<..<M::ereal} = real_of_ereal ` {-\<infinity><..<M} \<inter> real_of_ereal ` {N<..<\<infinity>}"
+ apply safe
+ subgoal by force
+ subgoal by force
+ subgoal for x y z
+ by (cases y; cases z) (auto intro!: image_eqI[where x=z] simp: )
+ done
+
+lemma real_atLeastGreaterThan_eq: "real_of_ereal ` {N<..<M::ereal} =
+ (if N = \<infinity> then {} else
+ if N = -\<infinity> then
+ (if M = \<infinity> then UNIV
+ else if M = -\<infinity> then {}
+ else {..< real_of_ereal M})
+ else if M = - \<infinity> then {}
+ else if M = \<infinity> then {real_of_ereal N<..}
+ else {real_of_ereal N <..< real_of_ereal M})"
+ apply (subst real_greaterThanLessThan_inter)
+ apply (subst real_greaterThanLessThan_minus_infinity_eq)
+ apply (subst real_greaterThanLessThan_infinity_eq)
+ apply auto
+ done
+
+lemma real_image_ereal_ivl:
+ fixes a b::ereal
+ shows
+ "real_of_ereal ` {a<..<b} =
+ (if a < b then (if a = - \<infinity> then if b = \<infinity> then UNIV else {..<real_of_ereal b}
+ else if b = \<infinity> then {real_of_ereal a<..} else {real_of_ereal a <..< real_of_ereal b}) else {})"
+ by (cases a; cases b; simp add: real_atLeastGreaterThan_eq not_less)
+
+lemma fixes a b c::ereal
+ shows not_inftyI: "a < b \<Longrightarrow> b < c \<Longrightarrow> abs b \<noteq> \<infinity>"
+ by force
+
+lemma
+ interval_neqs:
+ fixes r s t::real
+ shows "{r<..<s} \<noteq> {t<..}"
+ and "{r<..<s} \<noteq> {..<t}"
+ and "{r<..<ra} \<noteq> UNIV"
+ and "{r<..} \<noteq> {..<s}"
+ and "{r<..} \<noteq> UNIV"
+ and "{..<r} \<noteq> UNIV"
+ and "{} \<noteq> {r<..}"
+ and "{} \<noteq> {..<r}"
+ subgoal
+ by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
+ subgoal
+ by (metis (no_types, hide_lams) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
+ lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
+ subgoal by force
+ subgoal
+ by (metis greaterThanLessThan_empty_iff greaterThanLessThan_eq greaterThan_iff inf.idem
+ lessThan_iff lessThan_non_empty less_irrefl not_le)
+ subgoal by force
+ subgoal by force
+ subgoal using greaterThan_non_empty by blast
+ subgoal using lessThan_non_empty by blast
+ done
+
+lemma greaterThanLessThan_eq_iff:
+ fixes r s t u::real
+ shows "({r<..<s} = {t<..<u}) = (r \<ge> s \<and> u \<le> t \<or> r = t \<and> s = u)"
+ by (metis cInf_greaterThanLessThan cSup_greaterThanLessThan greaterThanLessThan_empty_iff not_le)
+
+lemma real_of_ereal_image_greaterThanLessThan_iff:
+ "real_of_ereal ` {a <..< b} = real_of_ereal ` {c <..< d} \<longleftrightarrow> (a \<ge> b \<and> c \<ge> d \<or> a = c \<and> b = d)"
+ unfolding real_atLeastGreaterThan_eq
+ by (cases a; cases b; cases c; cases d;
+ simp add: greaterThanLessThan_eq_iff interval_neqs interval_neqs[symmetric])
+
+lemma uminus_image_real_of_ereal_image_greaterThanLessThan:
+ "uminus ` real_of_ereal ` {l <..< u} = real_of_ereal ` {-u <..< -l}"
+ by (force simp: algebra_simps ereal_less_uminus_reorder
+ ereal_uminus_less_reorder intro: image_eqI[where x="-x" for x])
+
+lemma add_image_real_of_ereal_image_greaterThanLessThan:
+ "(+) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c + l <..< c + u}"
+ apply safe
+ subgoal for x
+ using ereal_less_add[of c]
+ by (force simp: real_of_ereal_add add.commute)
+ subgoal for _ x
+ by (force simp: add.commute real_of_ereal_minus ereal_minus_less ereal_less_minus
+ intro: image_eqI[where x="x - c"])
+ done
+
+lemma add2_image_real_of_ereal_image_greaterThanLessThan:
+ "(\<lambda>x. x + c) ` real_of_ereal ` {l <..< u} = real_of_ereal ` {l + c <..< u + c}"
+ using add_image_real_of_ereal_image_greaterThanLessThan[of c l u]
+ by (metis add.commute image_cong)
+
+lemma minus_image_real_of_ereal_image_greaterThanLessThan:
+ "(-) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c - u <..< c - l}"
+ (is "?l = ?r")
+proof -
+ have "?l = (+) c ` uminus ` real_of_ereal ` {l <..< u}" by auto
+ also note uminus_image_real_of_ereal_image_greaterThanLessThan
+ also note add_image_real_of_ereal_image_greaterThanLessThan
+ finally show ?thesis by (simp add: minus_ereal_def)
+qed
+
+lemma real_ereal_bound_lemma_up:
+ assumes "s \<in> real_of_ereal ` {a<..<b}"
+ assumes "t \<notin> real_of_ereal ` {a<..<b}"
+ assumes "s \<le> t"
+ shows "b \<noteq> \<infinity>"
+ using assms
+ apply (cases b)
+ subgoal by force
+ subgoal by (metis PInfty_neq_ereal(2) assms dual_order.strict_trans1 ereal_infty_less(1)
+ ereal_less_ereal_Ex greaterThanLessThan_empty_iff greaterThanLessThan_iff greaterThan_iff
+ image_eqI less_imp_le linordered_field_no_ub not_less order_trans
+ real_greaterThanLessThan_infinity_eq real_image_ereal_ivl real_of_ereal.simps(1))
+ subgoal by force
+ done
+
+lemma real_ereal_bound_lemma_down:
+ assumes "s \<in> real_of_ereal ` {a<..<b}"
+ assumes "t \<notin> real_of_ereal ` {a<..<b}"
+ assumes "t \<le> s"
+ shows "a \<noteq> - \<infinity>"
+ using assms
+ apply (cases b)
+ subgoal
+ apply safe
+ using assms(1)
+ apply (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+ done
+ subgoal by (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+ subgoal by auto
+ done
+
+
+subsection "Topological space"
instantiation ereal :: linear_continuum_topology
begin
@@ -2469,6 +2637,21 @@
by auto
qed (auto simp add: image_Union image_Int)
+lemma open_image_real_of_ereal:
+ fixes X::"ereal set"
+ assumes "open X"
+ assumes "\<infinity> \<notin> X"
+ assumes "-\<infinity> \<notin> X"
+ shows "open (real_of_ereal ` X)"
+proof -
+ have "real_of_ereal ` X = ereal -` X"
+ apply safe
+ subgoal by (metis assms(2) assms(3) real_of_ereal.elims vimageI)
+ subgoal using image_iff by fastforce
+ done
+ thus ?thesis
+ by (auto intro!: open_ereal_vimage assms)
+qed
lemma eventually_finite:
fixes x :: ereal
--- a/src/HOL/Library/Indicator_Function.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Fri Feb 23 15:17:51 2018 +0100
@@ -10,6 +10,9 @@
definition "indicator S x = (if x \<in> S then 1 else 0)"
+text\<open>Type constrained version\<close>
+abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
+
lemma indicator_simps[simp]:
"x \<in> S \<Longrightarrow> indicator S x = 1"
"x \<notin> S \<Longrightarrow> indicator S x = 0"
--- a/src/HOL/Limits.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Limits.thy Fri Feb 23 15:17:51 2018 +0100
@@ -52,6 +52,9 @@
for f :: "_ \<Rightarrow> real"
by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
+lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
+ by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)
+
lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially"
by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
@@ -1256,6 +1259,20 @@
for a :: real
unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
+lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)"
+ for a :: "'a::real_normed_vector"
+ using filtermap_at_shift[of "-a" 0] by simp
+
+lemma filterlim_at_to_0:
+ "filterlim f F (at a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at 0)"
+ for a :: "'a::real_normed_vector"
+ unfolding filterlim_def filtermap_filtermap at_to_0[of a] ..
+
+lemma eventually_at_to_0:
+ "eventually P (at a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at 0)"
+ for a :: "'a::real_normed_vector"
+ unfolding at_to_0[of a] by (simp add: eventually_filtermap)
+
lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a)"
for a :: "'a::real_normed_vector"
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
@@ -1268,6 +1285,7 @@
for a :: real
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
+
lemma filterlim_at_left_to_right:
"filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
for a :: real
@@ -1486,6 +1504,36 @@
for c :: nat
by (rule filterlim_subseq) (auto simp: strict_mono_def)
+lemma filterlim_times_pos:
+ "LIM x F1. c * f x :> at_right l"
+ if "filterlim f (at_right p) F1" "0 < c" "l = c * p"
+ for c::"'a::{linordered_field, linorder_topology}"
+ unfolding filterlim_iff
+proof safe
+ fix P
+ assume "\<forall>\<^sub>F x in at_right l. P x"
+ then obtain d where "c * p < d" "\<And>y. y > c * p \<Longrightarrow> y < d \<Longrightarrow> P y"
+ unfolding \<open>l = _ \<close> eventually_at_right_field
+ by auto
+ then have "\<forall>\<^sub>F a in at_right p. P (c * a)"
+ by (auto simp: eventually_at_right_field \<open>0 < c\<close> field_simps intro!: exI[where x="d/c"])
+ from that(1)[unfolded filterlim_iff, rule_format, OF this]
+ show "\<forall>\<^sub>F x in F1. P (c * f x)" .
+qed
+
+lemma filtermap_nhds_times: "c \<noteq> 0 \<Longrightarrow> filtermap (times c) (nhds a) = nhds (c * a)"
+ for a c :: "'a::real_normed_field"
+ by (rule filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+ (auto intro!: tendsto_eq_intros filterlim_ident)
+
+lemma filtermap_times_pos_at_right:
+ fixes c::"'a::{linordered_field, linorder_topology}"
+ assumes "c > 0"
+ shows "filtermap (times c) (at_right p) = at_right (c * p)"
+ using assms
+ by (intro filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+ (auto intro!: filterlim_ident filterlim_times_pos)
+
lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
proof (rule antisym)
have "(inverse \<longlongrightarrow> (0::'a)) at_infinity"
@@ -1936,6 +1984,10 @@
lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
using lim_1_over_n by (simp add: inverse_eq_divide)
+lemma lim_inverse_n': "((\<lambda>n. 1 / n) \<longlongrightarrow> 0) sequentially"
+ using lim_inverse_n
+ by (simp add: inverse_eq_divide)
+
lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
--- a/src/HOL/List.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/List.thy Fri Feb 23 15:17:51 2018 +0100
@@ -388,6 +388,10 @@
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)"
+definition stable_sort_key :: "(('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list) \<Rightarrow> bool" where
+"stable_sort_key sk =
+ (\<forall>f xs k. filter (\<lambda>y. f y = k) (sk f xs) = filter (\<lambda>y. f y = k) xs)"
+
end
@@ -5375,61 +5379,35 @@
lemma sorted_enumerate [simp]: "sorted (map fst (enumerate n xs))"
by (simp add: enumerate_eq_zip)
-text \<open>Stability of function @{const sort_key}:\<close>
-
-lemma sort_key_stable:
- "x \<in> set xs \<Longrightarrow> [y <- sort_key f xs. f y = f x] = [y <- xs. f y = f x]"
-proof (induction xs arbitrary: x)
+text \<open>Stability of @{const sort_key}:\<close>
+
+lemma sort_key_stable: "[y <- sort_key f xs. f y = k] = [y <- xs. f y = k]"
+proof (induction xs)
case Nil thus ?case by simp
next
case (Cons a xs)
thus ?case
- proof (cases "x \<in> set xs")
+ proof (cases "f a = k")
+ case False thus ?thesis
+ using Cons.IH by (metis (mono_tags) filter.simps(2) filter_sort)
+ next
case True
- thus ?thesis
- proof (cases "f a = f x")
- case False thus ?thesis
- using Cons.IH by (metis (mono_tags) True filter.simps(2) filter_sort)
- next
- case True
- hence ler: "[y <- (a # xs). f y = f x] = a # [y <- xs. f y = f a]" by simp
- have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
- hence "insort_key f a (sort_key f [y <- xs. f y = f a])
- = a # (sort_key f [y <- xs. f y = f a])"
- by (simp add: insort_is_Cons)
- hence lel: "[y <- sort_key f (a # xs). f y = f x] = a # [y <- sort_key f xs. f y = f a]"
- by (metis True filter_sort ler sort_key_simps(2))
- from lel ler show ?thesis using Cons.IH \<open>x \<in> set xs\<close> by (metis True filter_sort)
- qed
- next
- case False
- from Cons.prems have "x = a" by (metis False set_ConsD)
- have ler: "[y <- (a # xs). f y = f a] = a # [y <- xs. f y = f a]" by simp
+ hence ler: "[y <- (a # xs). f y = k] = a # [y <- xs. f y = f a]" by simp
have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
hence "insort_key f a (sort_key f [y <- xs. f y = f a])
- = a # (sort_key f [y <- xs. f y = f a])"
+ = a # (sort_key f [y <- xs. f y = f a])"
by (simp add: insort_is_Cons)
- hence lel: "[y <- sort_key f (a # xs). f y = f a] = a # [y <- sort_key f xs. f y = f a]"
- by (metis (mono_tags) filter.simps(2) filter_sort sort_key_simps(2))
- show ?thesis (is "?l = ?r")
- proof (cases "f a \<in> set (map f xs)")
- case False
- hence "\<forall>y \<in> set xs. f y \<noteq> f a" by (metis image_eqI set_map)
- hence R: "?r = [a]" using ler \<open>x=a\<close> by simp
- have L: "?l = [a]" using lel \<open>x=a\<close> by (metis R filter_sort insort_key.simps(1) sort_key_simps)
- from L R show ?thesis ..
- next
- case True
- then obtain z where Z: "z \<in> set xs \<and> f z = f a" by auto
- hence L: "[y <- sort_key f xs. f y = f z] = [y <- sort_key f xs. f y = f a]" by simp
- from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp
- from L R Z show ?thesis using Cons.IH ler lel \<open>x=a\<close> by metis
- qed
+ hence lel: "[y <- sort_key f (a # xs). f y = k] = a # [y <- sort_key f xs. f y = f a]"
+ by (metis True filter_sort ler sort_key_simps(2))
+ from lel ler show ?thesis using Cons.IH True by (auto)
qed
qed
+corollary stable_sort_key_sort_key: "stable_sort_key sort_key"
+by(simp add: stable_sort_key_def sort_key_stable)
+
lemma sort_key_const: "sort_key (\<lambda>x. c) xs = xs"
-by (metis (mono_tags) filter_False filter_True sort_key_simps(1) sort_key_stable)
+by (metis (mono_tags) filter_True sort_key_stable)
subsubsection \<open>@{const transpose} on sorted lists\<close>
--- a/src/HOL/Nat.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Nat.thy Fri Feb 23 15:17:51 2018 +0100
@@ -1774,7 +1774,7 @@
class ring_char_0 = ring_1 + semiring_char_0
-context linordered_semidom
+context linordered_nonzero_semiring
begin
lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
@@ -1783,8 +1783,21 @@
lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
by (simp add: not_less)
+lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
+ by (auto simp: le_iff_add intro!: add_increasing2)
+
lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
- by (induct m n rule: diff_induct) (simp_all add: add_pos_nonneg)
+proof(induct m n rule: diff_induct)
+ case (1 m) then show ?case
+ by auto
+next
+ case (2 n) then show ?case
+ by (simp add: add_pos_nonneg)
+next
+ case (3 m n)
+ then show ?case
+ by (auto simp: add_commute [of 1] add_mono1 not_less add_right_mono leD)
+qed
lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
by (simp add: not_less [symmetric] linorder_not_less [symmetric])
@@ -1795,7 +1808,7 @@
lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
by simp
-text \<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
+text \<open>Every \<open>linordered_nonzero_semiring\<close> has characteristic zero.\<close>
subclass semiring_char_0
by standard (auto intro!: injI simp add: eq_iff)
@@ -1810,6 +1823,14 @@
end
+
+context linordered_semidom
+begin
+subclass linordered_nonzero_semiring ..
+subclass semiring_char_0 ..
+end
+
+
context linordered_idom
begin
--- a/src/HOL/NthRoot.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/NthRoot.thy Fri Feb 23 15:17:51 2018 +0100
@@ -480,6 +480,9 @@
lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
by (meson not_le real_less_rsqrt)
+lemma sqrt_ge_absD: "\<bar>x\<bar> \<le> sqrt y \<Longrightarrow> x\<^sup>2 \<le> y"
+ using real_sqrt_le_iff[of "x\<^sup>2"] by simp
+
lemma sqrt_even_pow2:
assumes n: "even n"
shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
@@ -538,6 +541,8 @@
DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
+lemmas has_derivative_real_sqrt[derivative_intros] = DERIV_real_sqrt[THEN DERIV_compose_FDERIV]
+
lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0"
for x :: real
apply auto
@@ -658,6 +663,13 @@
lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
by (simp add: power2_eq_square [symmetric])
+lemma sqrt_sum_squares_le_sum:
+ "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply simp
+ done
+
lemma real_sqrt_sum_squares_triangle_ineq:
"sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
apply (rule power2_le_imp_le)
--- a/src/HOL/Rings.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Rings.thy Fri Feb 23 15:17:51 2018 +0100
@@ -2245,7 +2245,8 @@
end
-class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
+class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one +
+ assumes add_mono1: "a < b \<Longrightarrow> a + 1 < b + 1"
begin
subclass zero_neq_one
@@ -2278,7 +2279,15 @@
assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
begin
-subclass linordered_nonzero_semiring ..
+subclass linordered_nonzero_semiring
+proof
+ show "a + 1 < b + 1" if "a < b" for a b
+ proof (rule ccontr, simp add: not_less)
+ assume "b \<le> a"
+ with that show False
+ by (simp add: )
+ qed
+qed
text \<open>Addition is the inverse of subtraction.\<close>
--- a/src/HOL/Set_Interval.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Set_Interval.thy Fri Feb 23 15:17:51 2018 +0100
@@ -222,6 +222,10 @@
"{a..<b} = {a..b} - {b}"
by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
+lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff:
+ "{a<..b} = {a..b} - {a}"
+ by (auto simp add: greaterThanAtMost_def atLeastAtMost_def)
+
end
subsubsection\<open>Emptyness, singletons, subset\<close>
@@ -869,6 +873,19 @@
context linordered_semidom
begin
+lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}"
+proof -
+ have "n = k + (n - k)" if "i + k \<le> n" for n
+ proof -
+ have "n = (n - (k + i)) + (k + i)" using that
+ by (metis add_commute le_add_diff_inverse)
+ then show "n = k + (n - k)"
+ by (metis local.add_diff_cancel_left' add_assoc add_commute)
+ qed
+ then show ?thesis
+ by (fastforce simp: add_le_imp_le_diff add.commute)
+qed
+
lemma image_add_atLeastAtMost [simp]:
"plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
proof
@@ -911,112 +928,11 @@
"(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
by (simp add: add.commute [of _ k])
+lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}"
+ by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps)
+
end
-lemma image_Suc_atLeastAtMost [simp]:
- "Suc ` {i..j} = {Suc i..Suc j}"
- using image_add_atLeastAtMost [of 1 i j]
- by (simp only: plus_1_eq_Suc) simp
-
-lemma image_Suc_atLeastLessThan [simp]:
- "Suc ` {i..<j} = {Suc i..<Suc j}"
- using image_add_atLeastLessThan [of 1 i j]
- by (simp only: plus_1_eq_Suc) simp
-
-corollary image_Suc_atMost:
- "Suc ` {..n} = {1..Suc n}"
- by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-
-corollary image_Suc_lessThan:
- "Suc ` {..<n} = {1..n}"
- by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-
-lemma image_diff_atLeastAtMost [simp]:
- fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
- apply auto
- apply (rule_tac x="d-x" in rev_image_eqI, auto)
- done
-
-lemma image_mult_atLeastAtMost [simp]:
- fixes d::"'a::linordered_field"
- assumes "d>0" shows "(( * ) d ` {a..b}) = {d*a..d*b}"
- using assms
- by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
-
-lemma image_affinity_atLeastAtMost:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {m*a + c .. m *b + c}
- else {m*b + c .. m*a + c})"
- apply (case_tac "m=0", auto simp: mult_le_cancel_left)
- apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
- apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
- done
-
-lemma image_affinity_atLeastAtMost_diff:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {m*a - c .. m*b - c}
- else {m*b - c .. m*a - c})"
- using image_affinity_atLeastAtMost [of m "-c" a b]
- by simp
-
-lemma image_affinity_atLeastAtMost_div:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {a/m + c .. b/m + c}
- else {b/m + c .. a/m + c})"
- using image_affinity_atLeastAtMost [of "inverse m" c a b]
- by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma image_affinity_atLeastAtMost_div_diff:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {a/m - c .. b/m - c}
- else {b/m - c .. a/m - c})"
- using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
- by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma atLeast1_lessThan_eq_remove0:
- "{Suc 0..<n} = {..<n} - {0}"
- by auto
-
-lemma atLeast1_atMost_eq_remove0:
- "{Suc 0..n} = {..n} - {0}"
- by auto
-
-lemma image_add_int_atLeastLessThan:
- "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
- apply (auto simp add: image_def)
- apply (rule_tac x = "x - l" in bexI)
- apply auto
- done
-
-lemma image_minus_const_atLeastLessThan_nat:
- fixes c :: nat
- shows "(\<lambda>i. i - c) ` {x ..< y} =
- (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
- (is "_ = ?right")
-proof safe
- fix a assume a: "a \<in> ?right"
- show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
- proof cases
- assume "c < y" with a show ?thesis
- by (auto intro!: image_eqI[of _ _ "a + c"])
- next
- assume "\<not> c < y" with a show ?thesis
- by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
- qed
-qed auto
-
-lemma image_int_atLeastLessThan:
- "int ` {a..<b} = {int a..<int b}"
- by (auto intro!: image_eqI [where x = "nat x" for x])
-
-lemma image_int_atLeastAtMost:
- "int ` {a..b} = {int a..int b}"
- by (auto intro!: image_eqI [where x = "nat x" for x])
-
context ordered_ab_group_add
begin
@@ -1057,8 +973,184 @@
and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
+
+lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}"
+ by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps)
+
end
+lemma image_Suc_atLeastAtMost [simp]:
+ "Suc ` {i..j} = {Suc i..Suc j}"
+ using image_add_atLeastAtMost [of 1 i j]
+ by (simp only: plus_1_eq_Suc) simp
+
+lemma image_Suc_atLeastLessThan [simp]:
+ "Suc ` {i..<j} = {Suc i..<Suc j}"
+ using image_add_atLeastLessThan [of 1 i j]
+ by (simp only: plus_1_eq_Suc) simp
+
+corollary image_Suc_atMost:
+ "Suc ` {..n} = {1..Suc n}"
+ by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+corollary image_Suc_lessThan:
+ "Suc ` {..<n} = {1..n}"
+ by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+lemma image_diff_atLeastAtMost [simp]:
+ fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
+ apply auto
+ apply (rule_tac x="d-x" in rev_image_eqI, auto)
+ done
+
+lemma image_diff_atLeastLessThan [simp]:
+ fixes a b c::"'a::linordered_idom"
+ shows "(-) c ` {a..<b} = {c - b<..c - a}"
+proof -
+ have "(-) c ` {a..<b} = (+) c ` uminus ` {a ..<b}"
+ unfolding image_image by simp
+ also have "\<dots> = {c - b<..c - a}" by simp
+ finally show ?thesis by simp
+qed
+
+lemma image_minus_const_greaterThanAtMost_real[simp]:
+ fixes a b c::"'a::linordered_idom"
+ shows "(-) c ` {a<..b} = {c - b..<c - a}"
+proof -
+ have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}"
+ unfolding image_image by simp
+ also have "\<dots> = {c - b..<c - a}" by simp
+ finally show ?thesis by simp
+qed
+
+lemma image_minus_const_atLeast_real[simp]:
+ fixes a c::"'a::linordered_idom"
+ shows "(-) c ` {a..} = {..c - a}"
+proof -
+ have "(-) c ` {a..} = (+) c ` uminus ` {a ..}"
+ unfolding image_image by simp
+ also have "\<dots> = {..c - a}" by simp
+ finally show ?thesis by simp
+qed
+
+lemma image_minus_const_AtMost_real[simp]:
+ fixes b c::"'a::linordered_idom"
+ shows "(-) c ` {..b} = {c - b..}"
+proof -
+ have "(-) c ` {..b} = (+) c ` uminus ` {..b}"
+ unfolding image_image by simp
+ also have "\<dots> = {c - b..}" by simp
+ finally show ?thesis by simp
+qed
+
+context linordered_field begin
+
+lemma image_mult_atLeastAtMost [simp]:
+ "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
+ using that
+ by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
+
+lemma image_mult_atLeastAtMost_if:
+ "( * ) c ` {x .. y} =
+ (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
+proof -
+ consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
+ using local.antisym_conv3 local.leI by blast
+ then show ?thesis
+ proof cases
+ case 1
+ have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
+ by (simp add: image_image)
+ also have "\<dots> = {c * y .. c * x}"
+ using \<open>c < 0\<close>
+ by simp
+ finally show ?thesis
+ using \<open>c < 0\<close> by auto
+ qed (auto simp: not_le local.mult_less_cancel_left_pos)
+qed
+
+lemma image_mult_atLeastAtMost_if':
+ "(\<lambda>x. x * c) ` {x..y} =
+ (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
+ by (subst mult.commute)
+ (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
+
+lemma image_affinity_atLeastAtMost:
+ "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {m*a + c .. m *b + c}
+ else {m*b + c .. m*a + c})"
+proof -
+ have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
+ unfolding image_comp[symmetric]
+ by (simp add: o_def)
+ then show ?thesis
+ by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
+qed
+
+lemma image_affinity_atLeastAtMost_diff:
+ "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {m*a - c .. m*b - c}
+ else {m*b - c .. m*a - c})"
+ using image_affinity_atLeastAtMost [of m "-c" a b]
+ by simp
+
+lemma image_affinity_atLeastAtMost_div:
+ "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {a/m + c .. b/m + c}
+ else {b/m + c .. a/m + c})"
+ using image_affinity_atLeastAtMost [of "inverse m" c a b]
+ by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+lemma image_affinity_atLeastAtMost_div_diff:
+ "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {a/m - c .. b/m - c}
+ else {b/m - c .. a/m - c})"
+ using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
+ by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+end
+
+lemma atLeast1_lessThan_eq_remove0:
+ "{Suc 0..<n} = {..<n} - {0}"
+ by auto
+
+lemma atLeast1_atMost_eq_remove0:
+ "{Suc 0..n} = {..n} - {0}"
+ by auto
+
+lemma image_add_int_atLeastLessThan:
+ "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
+ apply (auto simp add: image_def)
+ apply (rule_tac x = "x - l" in bexI)
+ apply auto
+ done
+
+lemma image_minus_const_atLeastLessThan_nat:
+ fixes c :: nat
+ shows "(\<lambda>i. i - c) ` {x ..< y} =
+ (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
+ (is "_ = ?right")
+proof safe
+ fix a assume a: "a \<in> ?right"
+ show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
+ proof cases
+ assume "c < y" with a show ?thesis
+ by (auto intro!: image_eqI[of _ _ "a + c"])
+ next
+ assume "\<not> c < y" with a show ?thesis
+ by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
+ qed
+qed auto
+
+lemma image_int_atLeastLessThan:
+ "int ` {a..<b} = {int a..<int b}"
+ by (auto intro!: image_eqI [where x = "nat x" for x])
+
+lemma image_int_atLeastAtMost:
+ "int ` {a..b} = {int a..int b}"
+ by (auto intro!: image_eqI [where x = "nat x" for x])
+
+
subsubsection \<open>Finiteness\<close>
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
--- a/src/HOL/Topological_Spaces.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Feb 23 15:17:51 2018 +0100
@@ -609,7 +609,6 @@
and "filterlim g G (at x within {x. \<not>P x})"
shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
using assms by (intro filterlim_at_within_If) simp_all
-
lemma (in linorder_topology) at_within_order:
assumes "UNIV \<noteq> {x}"
shows "at x within s =
@@ -692,7 +691,18 @@
(\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal
eventually_filtercomap_nhds eventually_principal by blast
-
+
+lemma eventually_at_right_field:
+ "eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
+ for x :: "'a::{linordered_field, linorder_topology}"
+ using linordered_field_no_ub[rule_format, of x]
+ by (auto simp: eventually_at_right)
+
+lemma eventually_at_left_field:
+ "eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
+ for x :: "'a::{linordered_field, linorder_topology}"
+ using linordered_field_no_lb[rule_format, of x]
+ by (auto simp: eventually_at_left)
subsubsection \<open>Tendsto\<close>
@@ -762,9 +772,11 @@
end
-lemma tendsto_within_subset:
- "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
- by (blast intro: tendsto_mono at_le)
+lemma (in topological_space) filterlim_within_subset:
+ "filterlim f l (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> filterlim f l (at x within T)"
+ by (blast intro: filterlim_mono at_le)
+
+lemmas tendsto_within_subset = filterlim_within_subset
lemma (in order_topology) order_tendsto_iff:
"(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
@@ -963,6 +975,11 @@
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+lemma eventually_Lim_ident_at:
+ "(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
+ (\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
+ by (cases "at x within X = bot") (auto simp: Lim_ident_at)
+
lemma filterlim_at_bot_at_right:
fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
@@ -2612,6 +2629,37 @@
by (metis less_le)
qed
+lemma (in linorder_topology) not_in_connected_cases:
+ assumes conn: "connected S"
+ assumes nbdd: "x \<notin> S"
+ assumes ne: "S \<noteq> {}"
+ obtains "bdd_above S" "\<And>y. y \<in> S \<Longrightarrow> x \<ge> y" | "bdd_below S" "\<And>y. y \<in> S \<Longrightarrow> x \<le> y"
+proof -
+ obtain s where "s \<in> S" using ne by blast
+ {
+ assume "s \<le> x"
+ have "False" if "x \<le> y" "y \<in> S" for y
+ using connectedD_interval[OF conn \<open>s \<in> S\<close> \<open>y \<in> S\<close> \<open>s \<le> x\<close> \<open>x \<le> y\<close>] \<open>x \<notin> S\<close>
+ by simp
+ then have wit: "y \<in> S \<Longrightarrow> x \<ge> y" for y
+ using le_cases by blast
+ then have "bdd_above S"
+ by (rule local.bdd_aboveI)
+ note this wit
+ } moreover {
+ assume "x \<le> s"
+ have "False" if "x \<ge> y" "y \<in> S" for y
+ using connectedD_interval[OF conn \<open>y \<in> S\<close> \<open>s \<in> S\<close> \<open>x \<ge> y\<close> \<open>s \<ge> x\<close> ] \<open>x \<notin> S\<close>
+ by simp
+ then have wit: "y \<in> S \<Longrightarrow> x \<le> y" for y
+ using le_cases by blast
+ then have "bdd_below S"
+ by (rule bdd_belowI)
+ note this wit
+ } ultimately show ?thesis
+ by (meson le_cases that)
+qed
+
lemma connected_continuous_image:
assumes *: "continuous_on s f"
and "connected s"
@@ -3454,6 +3502,15 @@
lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
by (fact continuous_Pair)
+lemma continuous_on_compose_Pair:
+ assumes f: "continuous_on (Sigma A B) (\<lambda>(a, b). f a b)"
+ assumes g: "continuous_on C g"
+ assumes h: "continuous_on C h"
+ assumes subset: "\<And>c. c \<in> C \<Longrightarrow> g c \<in> A" "\<And>c. c \<in> C \<Longrightarrow> h c \<in> B (g c)"
+ shows "continuous_on C (\<lambda>c. f (g c) (h c))"
+ using continuous_on_compose2[OF f continuous_on_Pair[OF g h]] subset
+ by auto
+
subsubsection \<open>Connectedness of products\<close>
--- a/src/HOL/Transcendental.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/Transcendental.thy Fri Feb 23 15:17:51 2018 +0100
@@ -1389,6 +1389,8 @@
declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
and DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]
+
lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
proof -
from summable_norm[OF summable_norm_exp, of x]
@@ -1883,6 +1885,8 @@
declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
and DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_ln[derivative_intros] = DERIV_ln[THEN DERIV_compose_FDERIV]
+
lemma ln_series:
assumes "0 < x" and "x < 2"
shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
@@ -3094,24 +3098,33 @@
shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
using tendsto_powr'[of f a F g b] assms by auto
+lemma has_derivative_powr[derivative_intros]:
+ assumes g[derivative_intros]: "(g has_derivative g') (at x within X)"
+ and f[derivative_intros]:"(f has_derivative f') (at x within X)"
+ assumes pos: "0 < g x" and "x \<in> X"
+ shows "((\<lambda>x. g x powr f x::real) has_derivative (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+proof -
+ have "\<forall>\<^sub>F x in at x within X. g x > 0"
+ by (rule order_tendstoD[OF _ pos])
+ (rule has_derivative_continuous[OF g, unfolded continuous_within])
+ then obtain d where "d > 0" and pos': "\<And>x'. x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> 0 < g x'"
+ using pos unfolding eventually_at by force
+ have "((\<lambda>x. exp (f x * ln (g x))) has_derivative
+ (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+ using pos
+ by (auto intro!: derivative_eq_intros simp: divide_simps powr_def)
+ then show ?thesis
+ by (rule has_derivative_transform_within[OF _ \<open>d > 0\<close> \<open>x \<in> X\<close>]) (auto simp: powr_def dest: pos')
+qed
+
lemma DERIV_powr:
fixes r :: real
assumes g: "DERIV g x :> m"
and pos: "g x > 0"
and f: "DERIV f x :> r"
shows "DERIV (\<lambda>x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
-proof -
- have "DERIV (\<lambda>x. exp (f x * ln (g x))) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
- using pos
- by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff)
- then show ?thesis
- proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
- from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
- unfolding isCont_def by (rule order_tendstoD(1))
- with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
- by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
- qed
-qed
+ using assms
+ by (auto intro!: derivative_eq_intros ext simp: has_field_derivative_def algebra_simps)
lemma DERIV_fun_powr:
fixes r :: real
@@ -3344,6 +3357,8 @@
declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
and DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV]
+
lemma DERIV_cos [simp]: "DERIV cos x :> - sin x"
for x :: "'a::{real_normed_field,banach}"
unfolding sin_def cos_def scaleR_conv_of_real
@@ -3359,6 +3374,8 @@
declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
and DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV]
+
lemma isCont_sin: "isCont sin x"
for x :: "'a::{real_normed_field,banach}"
by (rule DERIV_sin [THEN DERIV_isCont])
@@ -4598,6 +4615,8 @@
unfolding tan_def
by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
+lemmas has_derivative_tan[derivative_intros] = DERIV_tan[THEN DERIV_compose_FDERIV]
+
lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
for x :: "'a::{real_normed_field,banach}"
by (rule DERIV_tan [THEN DERIV_isCont])
@@ -5265,6 +5284,10 @@
DERIV_arctan[THEN DERIV_chain2, derivative_intros]
DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_arctan[derivative_intros] = DERIV_arctan[THEN DERIV_compose_FDERIV]
+ and has_derivative_arccos[derivative_intros] = DERIV_arccos[THEN DERIV_compose_FDERIV]
+ and has_derivative_arcsin[derivative_intros] = DERIV_arcsin[THEN DERIV_compose_FDERIV]
+
lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- (pi/2)))"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
(auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
--- a/src/HOL/ex/Radix_Sort.thy Fri Feb 23 15:07:30 2018 +0100
+++ b/src/HOL/ex/Radix_Sort.thy Fri Feb 23 15:17:51 2018 +0100
@@ -2,27 +2,42 @@
theory Radix_Sort
imports
- "HOL-Library.Multiset"
"HOL-Library.List_lexord"
"HOL-Library.Sublist"
+ "HOL-Library.Multiset"
+begin
+
+locale Radix_Sort =
+fixes sort1 :: "('a list \<Rightarrow> 'a::linorder) \<Rightarrow> 'a list list \<Rightarrow> 'a list list"
+assumes sorted: "sorted (map f (sort1 f xs))"
+assumes mset: "mset (sort1 f xs) = mset xs"
+assumes stable: "stable_sort_key sort1"
begin
-fun radix_sort :: "nat \<Rightarrow> 'a::linorder list list \<Rightarrow> 'a list list" where
+lemma set_sort1[simp]: "set(sort1 f xs) = set xs"
+by (metis mset set_mset_mset)
+
+abbreviation "sort_col i xss \<equiv> sort1 (\<lambda>xs. xs ! i) xss"
+abbreviation "sorted_col i xss \<equiv> sorted (map (\<lambda>xs. xs ! i) xss)"
+
+fun radix_sort :: "nat \<Rightarrow> 'a list list \<Rightarrow> 'a list list" where
"radix_sort 0 xss = xss" |
-"radix_sort (Suc n) xss = radix_sort n (sort_key (\<lambda>xs. xs ! n) xss)"
+"radix_sort (Suc i) xss = radix_sort i (sort_col i xss)"
+
+lemma mset_radix_sort: "mset (radix_sort i xss) = mset xss"
+by(induction i arbitrary: xss) (auto simp: mset)
abbreviation "sorted_from i xss \<equiv> sorted (map (drop i) xss)"
-definition "cols xss k = (\<forall>xs \<in> set xss. length xs = k)"
+definition "cols xss n = (\<forall>xs \<in> set xss. length xs = n)"
-lemma mset_radix_sort: "mset (radix_sort k xss) = mset xss"
-by(induction k arbitrary: xss) (auto)
-
-lemma cols_sort_key: "cols xss n \<Longrightarrow> cols (sort_key f xss) n"
+lemma cols_sort1: "cols xss n \<Longrightarrow> cols (sort1 f xss) n"
by(simp add: cols_def)
-lemma sorted_from_Suc2: "\<lbrakk> cols xss n; i < n;
- sorted (map (\<lambda>xs. xs!i) xss); \<forall>xs \<in> set xss. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = xs!i] \<rbrakk>
+lemma sorted_from_Suc2:
+ "\<lbrakk> cols xss n; i < n;
+ sorted_col i xss;
+ \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
\<Longrightarrow> sorted_from i xss"
proof(induction xss rule: induct_list012)
case 1 show ?case by simp
@@ -36,7 +51,8 @@
proof -
have "drop i xs1 = xs1!i # drop (i+1) xs1"
using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs1)
- also have "\<dots> \<le> xs2!i # drop (i+1) xs2" using "3.prems"(3,4) by(auto)
+ also have "\<dots> \<le> xs2!i # drop (i+1) xs2"
+ using "3.prems"(3) "3.prems"(4)[of "xs2!i"] by(auto)
also have "\<dots> = drop i xs2"
using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs2)
finally show ?thesis .
@@ -44,8 +60,8 @@
have "sorted_from i (xs2 # xss)"
proof(rule "3.IH"[OF _ "3.prems"(2)])
show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
- show "sorted (map (\<lambda>xs. xs ! i) (xs2 # xss))" using "3.prems"(3) by simp
- show "\<forall>xs\<in>set (xs2 # xss). sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = xs ! i]"
+ show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
+ show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
using "3.prems"(4)
sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
by fastforce
@@ -54,21 +70,34 @@
qed
lemma sorted_from_radix_sort_step:
- "\<lbrakk> cols xss n; i < n; sorted_from (Suc i) xss \<rbrakk> \<Longrightarrow> sorted_from i (sort_key (\<lambda>xs. xs ! i) xss)"
-apply (rule sorted_from_Suc2)
-apply (auto simp add: sort_key_stable[of _ xss "%xs. xs!i"] sorted_filter cols_def)
-done
+assumes "cols xss n" and "i < n" and "sorted_from (i+1) xss"
+shows "sorted_from i (sort_col i xss)"
+proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
+ show "sorted_col i (sort_col i xss)" by(simp add: sorted)
+ fix x show "sorted_from (i+1) [ys \<leftarrow> sort_col i xss . ys ! i = x]"
+ proof -
+ from assms(3)
+ have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"
+ by(rule sorted_filter)
+ thus "sorted (map (drop (i+1)) (filter (\<lambda>ys. ys!i = x) (sort_col i xss)))"
+ by (metis stable stable_sort_key_def)
+ qed
+qed
lemma sorted_from_radix_sort:
- "cols xss n \<Longrightarrow> i \<le> n \<Longrightarrow> sorted_from i xss \<Longrightarrow> sorted_from 0 (radix_sort i xss)"
-apply(induction i arbitrary: xss)
- apply(simp add: sort_key_const)
-apply(simp add: sorted_from_radix_sort_step cols_sort_key)
-done
+ "\<lbrakk> cols xss n; i \<le> n; sorted_from i xss \<rbrakk> \<Longrightarrow> sorted_from 0 (radix_sort i xss)"
+proof(induction i arbitrary: xss)
+ case 0 thus ?case by simp
+next
+ case (Suc i)
+ thus ?case by(simp add: sorted_from_radix_sort_step cols_sort1)
+qed
-lemma sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
+corollary sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
apply(frule sorted_from_radix_sort[OF _ le_refl])
apply(auto simp add: cols_def sorted_equals_nth_mono)
done
end
+
+end