# HG changeset patch # User paulson # Date 1568892975 -3600 # Node ID 65371451fde8afb008925d55f5f3c5260c40c14e # Parent 4e39d87c9737f0dc9e094f7f4d52a5abc7f80a68 A few more simple results diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Change_Of_Vars.thy --- a/src/HOL/Analysis/Change_Of_Vars.thy Wed Sep 18 14:41:37 2019 +0100 +++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Sep 19 12:36:15 2019 +0100 @@ -9,41 +9,6 @@ begin -subsection \Orthogonal Transformation of Balls\ - -lemma image_orthogonal_transformation_ball: - fixes f :: "'a::euclidean_space \ 'a" - assumes "orthogonal_transformation f" - shows "f ` ball x r = ball (f x) r" -proof (intro equalityI subsetI) - fix y assume "y \ f ` ball x r" - with assms show "y \ ball (f x) r" - by (auto simp: orthogonal_transformation_isometry) -next - fix y assume y: "y \ ball (f x) r" - then obtain z where z: "y = f z" - using assms orthogonal_transformation_surj by blast - with y assms show "y \ f ` ball x r" - by (auto simp: orthogonal_transformation_isometry) -qed - -lemma image_orthogonal_transformation_cball: - fixes f :: "'a::euclidean_space \ 'a" - assumes "orthogonal_transformation f" - shows "f ` cball x r = cball (f x) r" -proof (intro equalityI subsetI) - fix y assume "y \ f ` cball x r" - with assms show "y \ cball (f x) r" - by (auto simp: orthogonal_transformation_isometry) -next - fix y assume y: "y \ cball (f x) r" - then obtain z where z: "y = f z" - using assms orthogonal_transformation_surj by blast - with y assms show "y \ f ` cball x r" - by (auto simp: orthogonal_transformation_isometry) -qed - - subsection \Measurable Shear and Stretch\ proposition diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Sep 18 14:41:37 2019 +0100 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Sep 19 12:36:15 2019 +0100 @@ -2568,12 +2568,23 @@ apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) done -lemma lim_ln_over_n: "((\n. ln(real_of_nat n) / of_nat n) \ 0) sequentially" +lemma lim_ln_over_n [tendsto_intros]: "((\n. ln(real_of_nat n) / of_nat n) \ 0) sequentially" using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]] apply (subst filterlim_sequentially_Suc [symmetric]) apply (simp add: lim_sequentially dist_norm) done +lemma lim_log_over_n [tendsto_intros]: + "(\n. log k n/n) \ 0" +proof - + have *: "log k n/n = (1/ln k) * (ln n / n)" for n + unfolding log_def by auto + have "(\n. (1/ln k) * (ln n / n)) \ (1/ln k) * 0" + by (intro tendsto_intros) + then show ?thesis + unfolding * by auto +qed + lemma lim_1_over_complex_power: assumes "0 < Re s" shows "(\n. 1 / of_nat n powr s) \ 0" diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Wed Sep 18 14:41:37 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Sep 19 12:36:15 2019 +0100 @@ -2000,6 +2000,11 @@ lemma infdist_zero[simp]: "a \ A \ infdist a A = 0" by (auto intro!: antisym infdist_nonneg infdist_le2) +lemma infdist_Un_min: + assumes "A \ {}" "B \ {}" + shows "infdist x (A \ B) = min (infdist x A) (infdist x B)" +using assms by (simp add: infdist_def cINF_union inf_real_def) + lemma infdist_triangle: "infdist x A \ infdist y A + dist x y" proof (cases "A = {}") case True @@ -2041,6 +2046,9 @@ finally show ?thesis by simp qed +lemma infdist_triangle_abs: "\infdist x A - infdist y A\ \ dist x y" + by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle) + lemma in_closure_iff_infdist_zero: assumes "A \ {}" shows "x \ closure A \ infdist x A = 0" @@ -3236,6 +3244,15 @@ by (auto simp: setdist_def infdist_def) qed +lemma infdist_mono: + assumes "A \ B" "A \ {}" + shows "infdist x B \ infdist x A" + by (simp add: assms infdist_eq_setdist setdist_subset_right) + +lemma infdist_singleton [simp]: + "infdist x {y} = dist x y" + by (simp add: infdist_eq_setdist) + proposition setdist_attains_inf: assumes "compact B" "B \ {}" obtains y where "y \ B" "setdist A B = infdist y A" diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Elementary_Normed_Spaces.thy --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Wed Sep 18 14:41:37 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Sep 19 12:36:15 2019 +0100 @@ -9,17 +9,13 @@ theory Elementary_Normed_Spaces imports "HOL-Library.FuncSet" - Elementary_Metric_Spaces Linear_Algebra + Elementary_Metric_Spaces Cartesian_Space Connected begin +subsection \Orthogonal Transformation of Balls\ subsection\<^marker>\tag unimportant\ \Various Lemmas Combining Imports\ -lemma countable_PiE: - "finite I \ (\i. i \ I \ countable (F i)) \ countable (Pi\<^sub>E I F)" - by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) - - lemma open_sums: fixes T :: "('b::real_normed_vector) set" assumes "open S \ open T" @@ -53,6 +49,38 @@ qed qed +lemma image_orthogonal_transformation_ball: + fixes f :: "'a::euclidean_space \ 'a" + assumes "orthogonal_transformation f" + shows "f ` ball x r = ball (f x) r" +proof (intro equalityI subsetI) + fix y assume "y \ f ` ball x r" + with assms show "y \ ball (f x) r" + by (auto simp: orthogonal_transformation_isometry) +next + fix y assume y: "y \ ball (f x) r" + then obtain z where z: "y = f z" + using assms orthogonal_transformation_surj by blast + with y assms show "y \ f ` ball x r" + by (auto simp: orthogonal_transformation_isometry) +qed + +lemma image_orthogonal_transformation_cball: + fixes f :: "'a::euclidean_space \ 'a" + assumes "orthogonal_transformation f" + shows "f ` cball x r = cball (f x) r" +proof (intro equalityI subsetI) + fix y assume "y \ f ` cball x r" + with assms show "y \ cball (f x) r" + by (auto simp: orthogonal_transformation_isometry) +next + fix y assume y: "y \ cball (f x) r" + then obtain z where z: "y = f z" + using assms orthogonal_transformation_surj by blast + with y assms show "y \ f ` cball x r" + by (auto simp: orthogonal_transformation_isometry) +qed + subsection \Support\ diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Analysis/Elementary_Topology.thy --- a/src/HOL/Analysis/Elementary_Topology.thy Wed Sep 18 14:41:37 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Topology.thy Thu Sep 19 12:36:15 2019 +0100 @@ -2479,6 +2479,14 @@ unfolding homeomorphism_def by (intro conjI ballI continuous_on_compose) (auto simp: image_iff) +lemma homeomorphism_cong: + "homeomorphism X' Y' f' g'" + if "homeomorphism X Y f g" "X' = X" "Y' = Y" "\x. x \ X \ f' x = f x" "\y. y \ Y \ g' y = g y" + using that by (auto simp add: homeomorphism_def) + +lemma homeomorphism_empty [simp]: + "homeomorphism {} {} f g" + unfolding homeomorphism_def by auto lemma homeomorphism_symD: "homeomorphism S t f g \ homeomorphism t S g f" by (simp add: homeomorphism_def) diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Wed Sep 18 14:41:37 2019 +0100 +++ b/src/HOL/Library/Extended_Real.thy Thu Sep 19 12:36:15 2019 +0100 @@ -1725,13 +1725,44 @@ by (cases a b c rule: ereal3_cases) (auto simp: field_simps zero_less_mult_iff) -lemma ereal_inverse_real: "\z\ \ \ \ z \ 0 \ ereal (inverse (real_of_ereal z)) = inverse z" - by (cases z) simp_all +lemma ereal_inverse_real [simp]: "\z\ \ \ \ z \ 0 \ ereal (inverse (real_of_ereal z)) = inverse z" + by auto lemma ereal_inverse_mult: "a \ 0 \ b \ 0 \ inverse (a * (b::ereal)) = inverse a * inverse b" by (cases a; cases b) auto +lemma inverse_eq_infinity_iff_eq_zero [simp]: + "1/(x::ereal) = \ \ x = 0" +by (simp add: divide_ereal_def) + +lemma ereal_distrib_left: + fixes a b c :: ereal + assumes "a \ \ \ b \ -\" + and "a \ -\ \ b \ \" + and "\c\ \ \" + shows "c * (a + b) = c * a + c * b" +using assms +by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps) + +lemma ereal_distrib_minus_left: + fixes a b c :: ereal + assumes "a \ \ \ b \ \" + and "a \ -\ \ b \ -\" + and "\c\ \ \" + shows "c * (a - b) = c * a - c * b" +using assms +by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps) + +lemma ereal_distrib_minus_right: + fixes a b c :: ereal + assumes "a \ \ \ b \ \" + and "a \ -\ \ b \ -\" + and "\c\ \ \" + shows "(a - b) * c = a * c - b * c" +using assms +by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps) + subsection "Complete lattice" @@ -4116,6 +4147,11 @@ by (force simp: continuous_on_def mult_ac) qed (insert assms, auto simp: mono_def ereal_mult_right_mono) +lemma Liminf_ereal_mult_left: + assumes "F \ bot" "(c::real) \ 0" + shows "Liminf F (\n. ereal c * f n) = ereal c * Liminf F f" +using Liminf_ereal_mult_right[OF assms] by (subst (1 2) mult.commute) + lemma Limsup_ereal_mult_left: assumes "F \ bot" "(c::real) \ 0" shows "Limsup F (\n. ereal c * f n) = ereal c * Limsup F f" diff -r 4e39d87c9737 -r 65371451fde8 src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Sep 18 14:41:37 2019 +0100 +++ b/src/HOL/Power.thy Thu Sep 19 12:36:15 2019 +0100 @@ -54,12 +54,6 @@ lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n" by (induct n) (simp_all add: power_add) -lemma power2_eq_square: "a\<^sup>2 = a * a" - by (simp add: numeral_2_eq_2) - -lemma power3_eq_cube: "a ^ 3 = a * a * a" - by (simp add: numeral_3_eq_3 mult.assoc) - lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2" by (subst mult.commute) (simp add: power_mult) @@ -73,6 +67,15 @@ by (simp only: numeral_Bit1 One_nat_def add_Suc_right add_0_right power_Suc power_add Let_def mult.assoc) +lemma power2_eq_square: "a\<^sup>2 = a * a" + by (simp add: numeral_2_eq_2) + +lemma power3_eq_cube: "a ^ 3 = a * a * a" + by (simp add: numeral_3_eq_3 mult.assoc) + +lemma power4_eq_xxxx: "x^4 = x * x * x * x" + by (simp add: mult.assoc power_numeral_even) + lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)" proof (induct "f x" arbitrary: f) case 0