Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
--- a/src/HOL/Complex.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Complex.thy Sat Apr 11 11:56:40 2015 +0100
@@ -167,6 +167,10 @@
lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
by (simp add: Im_divide sqr_conv_mult)
+lemma of_real_Re [simp]:
+ "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
+ by (auto simp: Reals_def)
+
subsection {* The Complex Number $i$ *}
primcorec "ii" :: complex ("\<i>") where
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sat Apr 11 11:56:40 2015 +0100
@@ -241,7 +241,9 @@
show ?case
proof (cases x)
case (Float m e)
- hence "0 < m" using assms powr_gt_zero[of 2 e] by (auto simp: sign_simps)
+ hence "0 < m" using assms
+ apply (auto simp: sign_simps)
+ by (meson not_less powr_ge_pzero)
hence "0 < sqrt m" by auto
have int_nat_bl: "(nat (bitlen m)) = bitlen m" using bitlen_nonneg by auto
@@ -1858,7 +1860,8 @@
finally show "?ln \<le> ?ub" .
qed
-lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
+lemma ln_add:
+ fixes x::real assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
proof -
have "x \<noteq> 0" using assms by auto
have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
@@ -1885,7 +1888,7 @@
let ?uthird = "rapprox_rat (max prec 1) 1 3"
let ?lthird = "lapprox_rat prec 1 3"
- have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1)"
+ have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1::real)"
using ln_add[of "3 / 2" "1 / 2"] by auto
have lb3: "?lthird \<le> 1 / 3" using lapprox_rat[of prec 1 3] by auto
hence lb3_ub: "real ?lthird < 1" by auto
@@ -1955,10 +1958,8 @@
lemma float_pos_eq_mantissa_pos: "x > 0 \<longleftrightarrow> mantissa x > 0"
apply (subst Float_mantissa_exponent[of x, symmetric])
- apply (auto simp add: zero_less_mult_iff zero_float_def powr_gt_zero[of 2 "exponent x"] dest: less_zeroE)
- using powr_gt_zero[of 2 "exponent x"]
- apply simp
- done
+ apply (auto simp add: zero_less_mult_iff zero_float_def dest: less_zeroE)
+ by (metis not_le powr_ge_pzero)
lemma Float_pos_eq_mantissa_pos: "Float m e > 0 \<longleftrightarrow> m > 0"
using powr_gt_zero[of 2 "e"]
@@ -2140,8 +2141,9 @@
let ?s = "Float (e + (bitlen m - 1)) 0"
let ?x = "Float m (- (bitlen m - 1))"
- have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e]
- by (auto simp: zero_less_mult_iff)
+ have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e]
+ apply (auto simp add: zero_less_mult_iff)
+ using not_le powr_ge_pzero by blast
def bl \<equiv> "bitlen m - 1" hence "bl \<ge> 0" using `m > 0` by (simp add: bitlen_def)
have "1 \<le> Float m e" using `1 \<le> x` Float unfolding less_eq_float_def by auto
from bitlen_div[OF `0 < m`] float_gt1_scale[OF `1 \<le> Float m e`] `bl \<ge> 0`
@@ -2180,7 +2182,7 @@
from float_gt1_scale[OF `1 \<le> Float m e`]
show "0 \<le> real (e + (bitlen m - 1))" by auto
next
- have "0 \<le> ln 2" by simp
+ have "0 \<le> ln (2 :: real)" by simp
thus "0 \<le> real (ub_ln2 prec)" using ub_ln2[of prec] by arith
qed auto
ultimately have "ln x \<le> float_plus_up prec ?ub2 ?ub_horner"
@@ -2333,10 +2335,9 @@
unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
by auto
-lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
- unfolding powr_def interpret_floatarith.simps ..
-
-lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
+lemma interpret_floatarith_log:
+ "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs =
+ log (interpret_floatarith b vs) (interpret_floatarith x vs)"
unfolding log_def interpret_floatarith.simps divide_inverse ..
lemma interpret_floatarith_num:
@@ -3481,7 +3482,7 @@
subsection {* Implement proof method \texttt{approximation} *}
lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
- interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
+ interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
interpret_floatarith_sin
oracle approximation_oracle = {* fn (thy, t) =>
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Sat Apr 11 11:56:40 2015 +0100
@@ -35,7 +35,7 @@
section "Compute some transcendental values"
-lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < inverse (2^51) "
+lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < (inverse (2^51) :: real)"
by (approximation 60)
lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"
--- a/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy Sat Apr 11 11:56:40 2015 +0100
@@ -28,7 +28,7 @@
lemma
fixes x::real
- shows "x > 1 \<Longrightarrow> x \<le> 2 powr 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
+ shows "x > 1 \<Longrightarrow> x \<le> 2 ^ 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
using [[quickcheck_approximation_custom_seed = 1]]
using [[quickcheck_approximation_epsilon = 0.00000001]]
--\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sat Apr 11 11:56:40 2015 +0100
@@ -103,7 +103,7 @@
constant ln \<rightharpoonup>
(SML) "Math.ln"
and (OCaml) "Pervasives.ln"
-declare ln_def[code del]
+declare ln_real_def[code del]
code_printing
constant cos \<rightharpoonup>
--- a/src/HOL/Library/Float.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Library/Float.thy Sat Apr 11 11:56:40 2015 +0100
@@ -82,16 +82,18 @@
lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
apply (auto simp: float_def)
apply hypsubst_thin
- apply (rule_tac x="-x" in exI)
- apply (rule_tac x="xa" in exI)
+ apply (rename_tac m e)
+ apply (rule_tac x="-m" in exI)
+ apply (rule_tac x="e" in exI)
apply (simp add: field_simps)
done
lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
apply (auto simp: float_def)
apply hypsubst_thin
- apply (rule_tac x="x * xa" in exI)
- apply (rule_tac x="xb + xc" in exI)
+ apply (rename_tac mx my ex ey)
+ apply (rule_tac x="mx * my" in exI)
+ apply (rule_tac x="ex + ey" in exI)
apply (simp add: powr_add)
done
@@ -107,16 +109,18 @@
lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
apply (auto simp add: float_def)
apply hypsubst_thin
- apply (rule_tac x="x" in exI)
- apply (rule_tac x="xa - d" in exI)
+ apply (rename_tac m e)
+ apply (rule_tac x="m" in exI)
+ apply (rule_tac x="e - d" in exI)
apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
done
lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
apply (auto simp add: float_def)
apply hypsubst_thin
- apply (rule_tac x="x" in exI)
- apply (rule_tac x="xa - d" in exI)
+ apply (rename_tac m e)
+ apply (rule_tac x="m" in exI)
+ apply (rule_tac x="e - d" in exI)
apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
done
@@ -687,8 +691,9 @@
from neg have "2 powr real p \<le> 2 powr 0"
by (intro powr_mono) auto
- also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
- also have "\<dots> \<le> \<lfloor>x * 2 powr real p\<rfloor>" unfolding real_of_int_le_iff
+ also have "\<dots> \<le> \<lfloor>2 powr 0::real\<rfloor>" by simp
+ also have "... \<le> \<lfloor>x * 2 powr (real p)\<rfloor>"
+ unfolding real_of_int_le_iff
using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
finally show ?thesis
using prec x
@@ -723,7 +728,7 @@
proof
have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
- finally show "round_up e f - f \<le> 2 powr real (- e)"
+ finally show "round_up e f - f \<le> 2 powr - (real e)"
by simp
qed (simp add: algebra_simps round_up)
@@ -740,7 +745,7 @@
proof
have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
- finally show "f - round_down e f \<le> 2 powr real (- e)"
+ finally show "f - round_down e f \<le> 2 powr - (real e)"
by simp
qed (simp add: algebra_simps round_down)
@@ -923,8 +928,9 @@
shows "0 \<le> e + (bitlen m - 1)"
proof -
have "0 < Float m e" using assms by auto
- hence "0 < m" using powr_gt_zero[of 2 e]
- by (auto simp: zero_less_mult_iff)
+ hence "0 < m" using powr_gt_zero[of 2 e]
+ apply (auto simp: zero_less_mult_iff)
+ using not_le powr_ge_pzero by blast
hence "m \<noteq> 0" by auto
show ?thesis
proof (cases "0 \<le> e")
@@ -2017,8 +2023,7 @@
by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
- apply (auto simp: zero_float_def mult_le_0_iff)
- using powr_gt_zero[of 2 b] by simp
+ by (auto simp: zero_float_def mult_le_0_iff) (simp add: not_less [symmetric])
lemma real_of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
unfolding pprt_def sup_float_def max_def sup_real_def by auto
--- a/src/HOL/Library/Formal_Power_Series.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Sat Apr 11 11:56:40 2015 +0100
@@ -624,7 +624,7 @@
by blast
}
then show ?thesis
- unfolding LIMSEQ_def by blast
+ unfolding lim_sequentially by blast
qed
--- a/src/HOL/Limits.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Limits.thy Sat Apr 11 11:56:40 2015 +0100
@@ -1287,7 +1287,7 @@
lemma LIMSEQ_iff:
fixes L :: "'a::real_normed_vector"
shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
-unfolding LIMSEQ_def dist_norm ..
+unfolding lim_sequentially dist_norm ..
lemma LIMSEQ_I:
fixes L :: "'a::real_normed_vector"
--- a/src/HOL/MacLaurin.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/MacLaurin.thy Sat Apr 11 11:56:40 2015 +0100
@@ -389,6 +389,12 @@
(exp t / (fact n)) * x ^ n"
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
+lemma exp_lower_taylor_quadratic:
+ fixes x::real
+ shows "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
+ using Maclaurin_exp_le [of x 3]
+ by (auto simp: numeral_3_eq_3 power2_eq_square power_Suc)
+
subsection{*Version for Sine Function*}
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Sat Apr 11 11:56:40 2015 +0100
@@ -189,18 +189,15 @@
lemma zero_le_float:
"(0 <= float (a,b)) = (0 <= a)"
- using powr_gt_zero[of 2 "real b", arith]
- by (simp add: float_def zero_le_mult_iff)
+ by (simp add: float_def zero_le_mult_iff) (simp add: not_less [symmetric])
lemma float_le_zero:
"(float (a,b) <= 0) = (a <= 0)"
- using powr_gt_zero[of 2 "real b", arith]
- by (simp add: float_def mult_le_0_iff)
+ by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric])
lemma float_abs:
"abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
- using powr_gt_zero[of 2 "real b", arith]
- by (simp add: float_def abs_if mult_less_0_iff)
+ by (simp add: float_def abs_if mult_less_0_iff not_less)
lemma float_zero:
"float (0, b) = 0"
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Sat Apr 11 11:56:40 2015 +0100
@@ -188,7 +188,7 @@
by simp
qed
show "convergent f"
- proof (rule convergentI, subst LIMSEQ_def, safe)
+ proof (rule convergentI, subst lim_sequentially, safe)
--{* The limit function converges according to its norm *}
fix e::real
assume "e > 0" hence "e/2 > 0" by simp
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Sat Apr 11 11:56:40 2015 +0100
@@ -250,6 +250,21 @@
by (metis closed_halfspace_Im_eq)
qed
+lemma closed_Real_halfspace_Re_le: "closed (\<real> \<inter> {w. Re w \<le> x})"
+ by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le)
+
+lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
+ using closed_halfspace_Re_ge
+ by (simp add: closed_Int closed_complex_Reals)
+
+lemma closed_real_abs_le: "closed {w \<in> \<real>. \<bar>Re w\<bar> \<le> r}"
+proof -
+ have "{w \<in> \<real>. \<bar>Re w\<bar> \<le> r} = (\<real> \<inter> {w. Re w \<le> r}) \<inter> (\<real> \<inter> {w. Re w \<ge> -r})"
+ by auto
+ then show "closed {w \<in> \<real>. \<bar>Re w\<bar> \<le> r}"
+ by (simp add: closed_Int closed_Real_halfspace_Re_ge closed_Real_halfspace_Re_le)
+qed
+
lemma real_lim:
fixes l::complex
assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
@@ -1151,4 +1166,93 @@
done
qed
+
+subsection {* Polynomal function extremal theorem, from HOL Light*}
+
+lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes "0 < e"
+ shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
+proof (induct n)
+ case 0 with assms
+ show ?case
+ apply (rule_tac x="norm (c 0) / e" in exI)
+ apply (auto simp: field_simps)
+ done
+next
+ case (Suc n)
+ obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
+ using Suc assms by blast
+ show ?case
+ proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
+ fix z::'a
+ assume z1: "M \<le> norm z" and "1 + norm (c (Suc n)) / e \<le> norm z"
+ then have z2: "e + norm (c (Suc n)) \<le> e * norm z"
+ using assms by (simp add: field_simps)
+ have "norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
+ using M [OF z1] by simp
+ then have "norm (\<Sum>i\<le>n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
+ by simp
+ then have "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
+ by (blast intro: norm_triangle_le elim: )
+ also have "... \<le> (e + norm (c (Suc n))) * norm z ^ Suc n"
+ by (simp add: norm_power norm_mult algebra_simps)
+ also have "... \<le> (e * norm z) * norm z ^ Suc n"
+ by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
+ finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
+ by (simp add: power_Suc)
+ qed
+qed
+
+lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+ assumes k: "c k \<noteq> 0" "1\<le>k" and kn: "k\<le>n"
+ shows "eventually (\<lambda>z. norm (\<Sum>i\<le>n. c(i) * z^i) \<ge> B) at_infinity"
+using kn
+proof (induction n)
+ case 0
+ then show ?case
+ using k by simp
+next
+ case (Suc m)
+ let ?even = ?case
+ show ?even
+ proof (cases "c (Suc m) = 0")
+ case True
+ then show ?even using Suc k
+ by auto (metis antisym_conv less_eq_Suc_le not_le)
+ next
+ case False
+ then obtain M where M:
+ "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>m. c i * z^i) \<le> norm (c (Suc m)) / 2 * norm z ^ Suc m"
+ using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
+ by auto
+ have "\<exists>b. \<forall>z. b \<le> norm z \<longrightarrow> B \<le> norm (\<Sum>i\<le>Suc m. c i * z^i)"
+ proof (rule exI [where x="max M (max 1 (\<bar>B\<bar> / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
+ fix z::'a
+ assume z1: "M \<le> norm z" "1 \<le> norm z"
+ and "\<bar>B\<bar> * 2 / norm (c (Suc m)) \<le> norm z"
+ then have z2: "\<bar>B\<bar> \<le> norm (c (Suc m)) * norm z / 2"
+ using False by (simp add: field_simps)
+ have nz: "norm z \<le> norm z ^ Suc m"
+ by (metis `1 \<le> norm z` One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
+ have *: "\<And>y x. norm (c (Suc m)) * norm z / 2 \<le> norm y - norm x \<Longrightarrow> B \<le> norm (x + y)"
+ by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
+ have "norm z * norm (c (Suc m)) + 2 * norm (\<Sum>i\<le>m. c i * z^i)
+ \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
+ using M [of z] Suc z1 by auto
+ also have "... \<le> 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
+ using nz by (simp add: mult_mono del: power_Suc)
+ finally show "B \<le> norm ((\<Sum>i\<le>m. c i * z^i) + c (Suc m) * z ^ Suc m)"
+ using Suc.IH
+ apply (auto simp: eventually_at_infinity)
+ apply (rule *)
+ apply (simp add: field_simps norm_mult norm_power)
+ done
+ qed
+ then show ?even
+ by (simp add: eventually_at_infinity)
+ qed
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Sat Apr 11 11:56:40 2015 +0100
@@ -8,7 +8,6 @@
imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
begin
-
lemma cmod_add_real_less:
assumes "Im z \<noteq> 0" "r\<noteq>0"
shows "cmod (z + r) < cmod z + abs r"
@@ -613,6 +612,14 @@
apply (simp only: pos_le_divide_eq [symmetric], linarith)
done
+lemma e_less_3: "exp 1 < (3::real)"
+ using e_approx_32
+ by (simp add: abs_if split: split_if_asm)
+
+lemma ln3_gt_1: "ln 3 > (1::real)"
+ by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
+
+
subsection{*The argument of a complex number*}
definition Arg :: "complex \<Rightarrow> real" where
@@ -892,8 +899,9 @@
subsection{*Complex logarithms (the conventional principal value)*}
-definition Ln where
- "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+definition Ln :: "complex \<Rightarrow> complex"
+ where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+
lemma
assumes "z \<noteq> 0"
@@ -941,6 +949,7 @@
apply (auto simp: exp_of_nat_mult [symmetric])
done
+
subsection{*The Unwinding Number and the Ln-product Formula*}
text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
@@ -1128,8 +1137,8 @@
apply (cases "z=0", auto)
apply (rule exp_complex_eqI)
apply (auto simp: abs_if split: split_if_asm)
- apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal)
- apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less)
+ apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps mult_2 neg_equal_0_iff_equal)
+ apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff mpi_less_Im_Ln mult.commute mult_2_right)
by (metis exp_Ln exp_cnj)
lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
@@ -1141,7 +1150,7 @@
inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
done
-lemma Ln_1 [simp]: "Ln(1) = 0"
+lemma Ln_1 [simp]: "Ln 1 = 0"
proof -
have "Ln (exp 0) = 0"
by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
@@ -1149,6 +1158,18 @@
by simp
qed
+instantiation complex :: ln
+begin
+
+definition ln_complex :: "complex \<Rightarrow> complex"
+ where "ln_complex \<equiv> Ln"
+
+instance
+ by intro_classes (simp add: ln_complex_def)
+
+end
+
+
lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
apply (rule exp_complex_eqI)
using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
@@ -1242,6 +1263,93 @@
by (auto simp: of_real_numeral Ln_times)
+
+subsection{*Complex Powers*}
+
+lemma powr_0 [simp]: "0 powr z = 0"
+ by (simp add: powr_def)
+
+lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
+ by (simp add: powr_def ln_complex_def)
+
+lemma powr_nat:
+ fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
+ by (simp add: exp_of_nat_mult powr_def ln_complex_def)
+
+lemma powr_add:
+ fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
+ by (simp add: powr_def algebra_simps exp_add)
+
+lemma powr_minus:
+ fixes w::complex shows "w powr (-z) = inverse(w powr z)"
+ by (simp add: powr_def exp_minus)
+
+lemma powr_diff:
+ fixes w::complex shows "w powr (z1 - z2) = w powr z1 / w powr z2"
+ by (simp add: powr_def algebra_simps exp_diff)
+
+lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
+ apply (simp add: powr_def ln_complex_def)
+ using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
+ by auto
+
+lemma powr_real_real:
+ "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
+ apply (simp add: powr_def ln_complex_def)
+ by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
+ exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
+
+lemma powr_of_real:
+ fixes x::real
+ shows "0 < x \<Longrightarrow> x powr y = x powr y"
+ by (simp add: powr_def powr_real_real)
+
+lemma norm_powr_real_mono:
+ "w \<in> \<real> \<Longrightarrow> 1 < Re w
+ \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
+ by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
+
+lemma powr_times_real:
+ "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
+ \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
+ by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
+
+lemma has_field_derivative_powr:
+ "(Im z = 0 \<Longrightarrow> 0 < Re z)
+ \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
+ apply (cases "z=0", auto)
+ apply (simp add: powr_def ln_complex_def)
+ apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
+ apply (auto simp: dist_complex_def ln_complex_def)
+ apply (intro derivative_eq_intros | simp add: assms)+
+ apply (simp add: field_simps exp_diff)
+ done
+
+lemma has_field_derivative_powr_right:
+ "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
+ apply (simp add: powr_def ln_complex_def)
+ apply (intro derivative_eq_intros | simp add: assms)+
+ done
+
+lemma complex_differentiable_powr_right:
+ "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
+using complex_differentiable_def has_field_derivative_powr_right by blast
+
+
+lemma holomorphic_on_powr_right:
+ "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
+ unfolding holomorphic_on_def
+ using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
+
+
+lemma norm_powr_real_powr:
+ "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
+ by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
+
+lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
+ using Ln_of_real by force
+
+
subsection{*Relation between Square Root and exp/ln, hence its derivative*}
lemma csqrt_exp_Ln:
@@ -1336,10 +1444,6 @@
using open_Compl
by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
-lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
- using closed_halfspace_Re_ge
- by (simp add: closed_Int closed_complex_Reals)
-
lemma continuous_within_csqrt_posreal:
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
proof (cases "Im z = 0 --> 0 < Re(z)")
@@ -1867,15 +1971,15 @@
Re z = pi & Im z \<le> 0"
shows "Arccos(cos z) = z"
proof -
- have *: "((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z))) = sin z"
+ have *: "((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z))) = sin z"
by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
- have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2"
+ have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2"
by (simp add: field_simps power2_eq_square)
then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
- \<i> * csqrt (((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2)))"
+ \<i> * csqrt (((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2)))"
by (simp add: cos_exp_eq Arccos_def exp_minus)
also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
- \<i> * ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))))"
+ \<i> * ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))))"
apply (subst csqrt_square)
using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
apply (auto simp: * Re_sin Im_sin)
@@ -2177,4 +2281,129 @@
lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
+subsection{*Some interrelationships among the real inverse trig functions.*}
+
+lemma arccos_arctan:
+ assumes "-1 < x" "x < 1"
+ shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
+proof -
+ have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
+ proof (rule sin_eq_0_pi)
+ show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
+ using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
+ by (simp add: algebra_simps)
+ next
+ show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
+ using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms
+ by (simp add: algebra_simps)
+ next
+ show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
+ using assms
+ by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
+ power2_eq_square square_eq_1_iff)
+ qed
+ then show ?thesis
+ by simp
+qed
+
+lemma arcsin_plus_arccos:
+ assumes "-1 \<le> x" "x \<le> 1"
+ shows "arcsin x + arccos x = pi/2"
+proof -
+ have "arcsin x = pi/2 - arccos x"
+ apply (rule sin_inj_pi)
+ using assms arcsin [OF assms] arccos [OF assms]
+ apply (auto simp: algebra_simps sin_diff)
+ done
+ then show ?thesis
+ by (simp add: algebra_simps)
+qed
+
+lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
+ using arcsin_plus_arccos by force
+
+lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
+ using arcsin_plus_arccos by force
+
+lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
+ by (simp add: arccos_arctan arcsin_arccos_eq)
+
+lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
+ by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
+
+lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
+ apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
+ apply (subst Arcsin_Arccos_csqrt_pos)
+ apply (auto simp: power_le_one zz)
+ done
+
+lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
+ using arcsin_arccos_sqrt_pos [of "-x"]
+ by (simp add: arcsin_minus)
+
+lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
+ apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
+ apply (subst Arccos_Arcsin_csqrt_pos)
+ apply (auto simp: power_le_one zz)
+ done
+
+lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
+ using arccos_arcsin_sqrt_pos [of "-x"]
+ by (simp add: arccos_minus)
+
+subsection{*continuity results for arcsin and arccos.*}
+
+lemma continuous_on_Arcsin_real [continuous_intros]:
+ "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
+proof -
+ have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arcsin (Re x))) =
+ continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arcsin (of_real (Re x)))))"
+ by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin)
+ also have "... = ?thesis"
+ by (rule continuous_on_cong [OF refl]) simp
+ finally show ?thesis
+ using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
+ continuous_on_of_real
+ by fastforce
+qed
+
+lemma continuous_within_Arcsin_real:
+ "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arcsin"
+proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
+ case True then show ?thesis
+ using continuous_on_Arcsin_real continuous_on_eq_continuous_within
+ by blast
+next
+ case False
+ with closed_real_abs_le [of 1] show ?thesis
+ by (rule continuous_within_closed_nontrivial)
+qed
+
+lemma continuous_on_Arccos_real:
+ "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arccos"
+proof -
+ have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arccos (Re x))) =
+ continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arccos (of_real (Re x)))))"
+ by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos)
+ also have "... = ?thesis"
+ by (rule continuous_on_cong [OF refl]) simp
+ finally show ?thesis
+ using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
+ continuous_on_of_real
+ by fastforce
+qed
+
+lemma continuous_within_Arccos_real:
+ "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arccos"
+proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
+ case True then show ?thesis
+ using continuous_on_Arccos_real continuous_on_eq_continuous_within
+ by blast
+next
+ case False
+ with closed_real_abs_le [of 1] show ?thesis
+ by (rule continuous_within_closed_nontrivial)
+qed
+
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Apr 11 11:56:40 2015 +0100
@@ -4077,7 +4077,7 @@
apply (erule_tac x="e/2" in allE)
apply auto
done
- from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]]
+ from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]]
obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"
using `e > 0` by auto
{
@@ -4096,7 +4096,7 @@
then have "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
}
then have "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s`
- unfolding LIMSEQ_def by auto
+ unfolding lim_sequentially by auto
}
then show ?thesis unfolding complete_def by auto
qed
@@ -4442,7 +4442,7 @@
fix e :: real
assume "e > 0"
then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
- using l[unfolded LIMSEQ_def] by auto
+ using l[unfolded lim_sequentially] by auto
have "t (max n N) \<in> s n"
using assms(3)
unfolding subset_eq
@@ -4542,7 +4542,7 @@
fix x
assume "P x"
then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2"
- using l[THEN spec[where x=x], unfolded LIMSEQ_def] and `e > 0`
+ using l[THEN spec[where x=x], unfolded lim_sequentially] and `e > 0`
by (auto elim!: allE[where x="e/2"])
fix n :: nat
assume "n \<ge> N"
@@ -4571,7 +4571,7 @@
assume "P x"
then have "l x = l' x"
using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
- using l and assms(2) unfolding LIMSEQ_def by blast
+ using l and assms(2) unfolding lim_sequentially by blast
}
ultimately show ?thesis by auto
qed
@@ -4809,7 +4809,7 @@
then obtain d where "d > 0" and d: "\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
obtain N where N: "\<forall>n\<ge>N. dist (x n) (y n) < d"
- using xy[unfolded LIMSEQ_def dist_norm] and `d>0` by auto
+ using xy[unfolded lim_sequentially dist_norm] and `d>0` by auto
{
fix n
assume "n\<ge>N"
@@ -4824,7 +4824,7 @@
by auto
}
then have "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially"
- unfolding LIMSEQ_def and dist_real_def by auto
+ unfolding lim_sequentially and dist_real_def by auto
}
then show ?rhs by auto
next
@@ -4864,7 +4864,7 @@
}
then have "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"
using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn
- unfolding LIMSEQ_def dist_real_def by auto
+ unfolding lim_sequentially dist_real_def by auto
then have False using fxy and `e>0` by auto
}
then show ?lhs
@@ -6615,7 +6615,7 @@
then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
}
then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
- unfolding LIMSEQ_def by(auto simp add: dist_norm)
+ unfolding lim_sequentially by(auto simp add: dist_norm)
then have "(f ---> x) sequentially"
unfolding f_def
using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
@@ -7446,7 +7446,7 @@
unfolding e_def using zero_le_dist[of "f x" x]
by (metis dist_eq_0_iff dist_nz e_def)
then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"
- using x[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
+ using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto
then have N':"dist (z N) x < e / 2" by auto
have *: "c * dist (z N) x \<le> dist (z N) x"
--- a/src/HOL/NSA/HLog.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/NSA/HLog.thy Sat Apr 11 11:56:40 2015 +0100
@@ -34,13 +34,13 @@
lemma powhr_mult:
"!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-by (transfer, rule powr_mult)
+by (transfer, simp add: powr_mult)
-lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a"
+lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
by (transfer, simp)
-lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
-by (metis less_numeral_extra(3) powhr_gt_zero)
+lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
+by transfer simp
lemma powhr_divide:
"!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
@@ -105,8 +105,8 @@
==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
by (transfer, rule log_eq_div_ln_mult_log)
-lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)"
-by (transfer, simp add: powr_def)
+lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
+ by (transfer, simp add: powr_def)
lemma HInfinite_powhr:
"[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;
--- a/src/HOL/NSA/HTranscendental.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/NSA/HTranscendental.thy Sat Apr 11 11:56:40 2015 +0100
@@ -306,34 +306,37 @@
lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
by transfer (rule exp_gt_one)
-lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x"
+abbreviation real_ln :: "real \<Rightarrow> real" where
+ "real_ln \<equiv> ln"
+
+lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x"
by transfer (rule ln_exp)
-lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)"
+lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
by transfer (rule exp_ln_iff)
-lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u"
+lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u"
by transfer (rule ln_unique)
-lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
+lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x"
by transfer (rule ln_less_self)
-lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x"
+lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* real_ln) x"
by transfer (rule ln_ge_zero)
-lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x"
+lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
by transfer (rule ln_gt_zero)
-lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
+lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* real_ln) x \<noteq> 0"
by transfer simp
-lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
+lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* real_ln) x \<in> HFinite"
apply (rule HFinite_bounded)
apply assumption
apply (simp_all add: starfun_ln_less_self order_less_imp_le)
done
-lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
+lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x"
by transfer (rule ln_inverse)
lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
@@ -360,7 +363,7 @@
(* using previous result to get to result *)
lemma starfun_ln_HInfinite:
- "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
+ "[| x \<in> HInfinite; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
apply (drule starfun_exp_HFinite)
apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
@@ -374,7 +377,7 @@
(* check out this proof!!! *)
lemma starfun_ln_HFinite_not_Infinitesimal:
- "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
+ "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HFinite"
apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
@@ -383,22 +386,22 @@
(* we do proof by considering ln of 1/x *)
lemma starfun_ln_Infinitesimal_HInfinite:
- "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
+ "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
apply (drule Infinitesimal_inverse_HInfinite)
apply (frule positive_imp_inverse_positive)
apply (drule_tac [2] starfun_ln_HInfinite)
apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
done
-lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
+lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0"
by transfer (rule ln_less_zero)
lemma starfun_ln_Infinitesimal_less_zero:
- "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
+ "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0"
by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
lemma starfun_ln_HInfinite_gt_zero:
- "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
+ "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x"
by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
--- a/src/HOL/NSA/NSComplex.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/NSA/NSComplex.thy Sat Apr 11 11:56:40 2015 +0100
@@ -72,7 +72,7 @@
(*------------ e ^ (x + iy) ------------*)
definition
hExp :: "hcomplex => hcomplex" where
- "hExp = *f* Exp"
+ "hExp = *f* exp"
definition
HComplex :: "[hypreal,hypreal] => hcomplex" where
@@ -485,7 +485,7 @@
by transfer (rule rcis_Ex)
lemma hRe_hcomplex_polar [simp]:
- "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
+ "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
r * ( *f* cos) a"
by transfer simp
@@ -493,7 +493,7 @@
by transfer (rule Re_rcis)
lemma hIm_hcomplex_polar [simp]:
- "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
+ "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
r * ( *f* sin) a"
by transfer simp
@@ -621,8 +621,8 @@
subsection{*Numerals and Arithmetic*}
-lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
- "hcomplex_of_hypreal (hypreal_of_real x) =
+lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
+ "hcomplex_of_hypreal (hypreal_of_real x) =
hcomplex_of_complex (complex_of_real x)"
by transfer (rule refl)
@@ -642,15 +642,15 @@
"hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)"
by transfer (rule norm_numeral)
-lemma hcomplex_neg_numeral_hcmod [simp]:
+lemma hcomplex_neg_numeral_hcmod [simp]:
"hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)"
by transfer (rule norm_neg_numeral)
-lemma hcomplex_numeral_hRe [simp]:
+lemma hcomplex_numeral_hRe [simp]:
"hRe(numeral v :: hcomplex) = numeral v"
by transfer (rule complex_Re_numeral)
-lemma hcomplex_numeral_hIm [simp]:
+lemma hcomplex_numeral_hIm [simp]:
"hIm(numeral v :: hcomplex) = 0"
by transfer (rule complex_Im_numeral)
--- a/src/HOL/Probability/Borel_Space.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Sat Apr 11 11:56:40 2015 +0100
@@ -1038,7 +1038,7 @@
lemma borel_measurable_ln[measurable (raw)]:
assumes f: "f \<in> borel_measurable M"
- shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
+ shows "(\<lambda>x. ln (f x :: real)) \<in> borel_measurable M"
apply (rule measurable_compose[OF f])
apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
apply (auto intro!: continuous_on_ln continuous_on_id)
--- a/src/HOL/Probability/Information.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Probability/Information.thy Sat Apr 11 11:56:40 2015 +0100
@@ -46,7 +46,7 @@
finally have "exp u \<noteq> x"
by auto }
then show "log b x = log b 0"
- by (simp add: log_def ln_def)
+ by (simp add: log_def ln_real_def)
qed
lemma log_mult_eq:
--- a/src/HOL/Probability/Regularity.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Probability/Regularity.thy Sat Apr 11 11:56:40 2015 +0100
@@ -363,7 +363,7 @@
fix e::real assume "e > 0"
with measure_LIMSEQ
have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
- by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
+ by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1)
hence "\<exists>n0. \<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
unfolding choice_iff by blast
--- a/src/HOL/Real_Vector_Spaces.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Apr 11 11:56:40 2015 +0100
@@ -1544,19 +1544,19 @@
subsubsection {* Limits of Sequences *}
-lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
+lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
unfolding tendsto_iff eventually_sequentially ..
lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
- unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
+ unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)
lemma metric_LIMSEQ_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)"
-by (simp add: LIMSEQ_def)
+by (simp add: lim_sequentially)
lemma metric_LIMSEQ_D:
"\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
-by (simp add: LIMSEQ_def)
+by (simp add: lim_sequentially)
subsubsection {* Limits of Functions *}
@@ -1823,7 +1823,7 @@
proof (rule tendstoI)
fix e :: real assume "0 < e"
with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
- by (auto simp: LIMSEQ_def dist_real_def)
+ by (auto simp: lim_sequentially dist_real_def)
{ fix x :: real
obtain n where "x \<le> real_of_nat n"
using ex_le_of_nat[of x] ..
--- a/src/HOL/Set_Interval.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Set_Interval.thy Sat Apr 11 11:56:40 2015 +0100
@@ -1562,12 +1562,6 @@
"(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
by (induction n) (auto simp: setsum.distrib)
-lemma setsum_zero_power [simp]:
- fixes c :: "nat \<Rightarrow> 'a::division_ring"
- shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
-apply (cases "finite A")
- by (induction A rule: finite_induct) auto
-
lemma setsum_zero_power' [simp]:
fixes c :: "nat \<Rightarrow> 'a::field"
shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
--- a/src/HOL/Transcendental.thy Thu Apr 09 20:42:38 2015 +0200
+++ b/src/HOL/Transcendental.thy Sat Apr 11 11:56:40 2015 +0100
@@ -1285,88 +1285,130 @@
subsection {* Natural Logarithm *}
-definition ln :: "real \<Rightarrow> real"
- where "ln x = (THE u. exp u = x)"
-
-lemma ln_exp [simp]: "ln (exp x) = x"
- by (simp add: ln_def)
-
-lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
+class ln = real_normed_algebra_1 + banach +
+ fixes ln :: "'a \<Rightarrow> 'a"
+ assumes ln_one [simp]: "ln 1 = 0"
+
+definition powr :: "['a,'a] => 'a::ln" (infixr "powr" 80)
+ -- {*exponentation via ln and exp*}
+ where "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
+
+
+instantiation real :: ln
+begin
+
+definition ln_real :: "real \<Rightarrow> real"
+ where "ln_real x = (THE u. exp u = x)"
+
+instance
+by intro_classes (simp add: ln_real_def)
+
+end
+
+lemma powr_eq_0_iff [simp]: "w powr z = 0 \<longleftrightarrow> w = 0"
+ by (simp add: powr_def)
+
+lemma ln_exp [simp]:
+ fixes x::real shows "ln (exp x) = x"
+ by (simp add: ln_real_def)
+
+lemma exp_ln [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> exp (ln x) = x"
by (auto dest: exp_total)
-lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
+lemma exp_ln_iff [simp]:
+ fixes x::real shows "exp (ln x) = x \<longleftrightarrow> 0 < x"
by (metis exp_gt_zero exp_ln)
-lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
+lemma ln_unique:
+ fixes x::real shows "exp y = x \<Longrightarrow> ln x = y"
by (erule subst, rule ln_exp)
-lemma ln_one [simp]: "ln 1 = 0"
- by (rule ln_unique) simp
-
-lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
+lemma ln_mult:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
by (rule ln_unique) (simp add: exp_add)
-lemma ln_setprod:
+lemma ln_setprod:
+ fixes f:: "'a => real"
+ shows
"\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i > 0\<rbrakk> \<Longrightarrow> ln(setprod f I) = setsum (\<lambda>x. ln(f x)) I"
by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos)
-lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
+lemma ln_inverse:
+ fixes x::real shows "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
by (rule ln_unique) (simp add: exp_minus)
-lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
+lemma ln_div:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
by (rule ln_unique) (simp add: exp_diff)
lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
by (rule ln_unique) (simp add: exp_real_of_nat_mult)
-lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
+lemma ln_less_cancel_iff [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
by (subst exp_less_cancel_iff [symmetric]) simp
-lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
+lemma ln_le_cancel_iff [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
by (simp add: linorder_not_less [symmetric])
-lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
+lemma ln_inj_iff [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
by (simp add: order_eq_iff)
-lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
+lemma ln_add_one_self_le_self [simp]:
+ fixes x::real shows "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
apply (rule exp_le_cancel_iff [THEN iffD1])
apply (simp add: exp_ge_add_one_self_aux)
done
-lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
+lemma ln_less_self [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> ln x < x"
by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
-lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
+lemma ln_ge_zero [simp]:
+ fixes x::real shows "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
using ln_le_cancel_iff [of 1 x] by simp
-lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
+lemma ln_ge_zero_imp_ge_one:
+ fixes x::real shows "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
using ln_le_cancel_iff [of 1 x] by simp
-lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
+lemma ln_ge_zero_iff [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
using ln_le_cancel_iff [of 1 x] by simp
-lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
+lemma ln_less_zero_iff [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
using ln_less_cancel_iff [of x 1] by simp
-lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
+lemma ln_gt_zero:
+ fixes x::real shows "1 < x \<Longrightarrow> 0 < ln x"
using ln_less_cancel_iff [of 1 x] by simp
-lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
+lemma ln_gt_zero_imp_gt_one:
+ fixes x::real shows "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
using ln_less_cancel_iff [of 1 x] by simp
-lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
+lemma ln_gt_zero_iff [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
using ln_less_cancel_iff [of 1 x] by simp
-lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
+lemma ln_eq_zero_iff [simp]:
+ fixes x::real shows "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
using ln_inj_iff [of x 1] by simp
-lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
+lemma ln_less_zero:
+ fixes x::real shows "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
by simp
-lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
- by (auto simp add: ln_def intro!: arg_cong[where f=The])
-
-lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
+lemma ln_neg_is_const:
+ fixes x::real shows "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
+ by (auto simp add: ln_real_def intro!: arg_cong[where f=The])
+
+lemma isCont_ln:
+ fixes x::real assumes "x \<noteq> 0" shows "isCont ln x"
proof cases
assume "0 < x"
moreover then have "isCont ln (exp (ln x))"
@@ -1381,32 +1423,35 @@
intro!: exI[of _ "\<bar>x\<bar>"])
qed
-lemma tendsto_ln [tendsto_intros]:
+lemma tendsto_ln [tendsto_intros]:
+ fixes a::real shows
"(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
by (rule isCont_tendsto_compose [OF isCont_ln])
lemma continuous_ln:
- "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
+ "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x :: real))"
unfolding continuous_def by (rule tendsto_ln)
lemma isCont_ln' [continuous_intros]:
- "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
+ "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x :: real))"
unfolding continuous_at by (rule tendsto_ln)
lemma continuous_within_ln [continuous_intros]:
- "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
+ "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x :: real))"
unfolding continuous_within by (rule tendsto_ln)
lemma continuous_on_ln [continuous_intros]:
- "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
+ "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x :: real))"
unfolding continuous_on_def by (auto intro: tendsto_ln)
-lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
+lemma DERIV_ln:
+ fixes x::real shows "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
done
-lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
+lemma DERIV_ln_divide:
+ fixes x::real shows "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
@@ -1533,13 +1578,13 @@
unfolding power2_eq_square
apply (rule mult_left_mono)
using assms
- apply (auto simp: )
+ apply auto
done
show ?thesis
apply (rule order_trans [OF norm_exp])
apply (rule order_trans [OF exp_bound])
using assms n
- apply (auto simp: )
+ apply auto
done
qed
@@ -1549,7 +1594,8 @@
using exp_bound_lemma [of x]
by simp
-lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
+lemma ln_one_minus_pos_upper_bound:
+ fixes x::real shows "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
proof -
assume a: "0 <= (x::real)" and b: "x < 1"
have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
@@ -1590,7 +1636,8 @@
apply auto
done
-lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
+lemma ln_one_plus_pos_lower_bound:
+ fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
proof -
assume a: "0 <= x" and b: "x <= 1"
have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
@@ -1614,7 +1661,8 @@
qed
lemma ln_one_minus_pos_lower_bound:
- "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
+ fixes x::real
+ shows "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
proof -
assume a: "0 <= x" and b: "x <= (1 / 2)"
from b have c: "x < 1" by auto
@@ -1642,14 +1690,15 @@
by (rule order_trans)
qed
-lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
+lemma ln_add_one_self_le_self2:
+ fixes x::real shows "-1 < x \<Longrightarrow> ln(1 + x) <= x"
apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
apply (subst ln_le_cancel_iff)
apply auto
done
lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
- "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
+ fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
proof -
assume x: "0 <= x"
assume x1: "x <= 1"
@@ -1672,7 +1721,7 @@
qed
lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
- "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
+ fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
proof -
assume a: "-(1 / 2) <= x"
assume b: "x <= 0"
@@ -1692,7 +1741,7 @@
qed
lemma abs_ln_one_plus_x_minus_x_bound:
- "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
+ fixes x::real shows "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
apply (case_tac "0 <= x")
apply (rule order_trans)
apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
@@ -1701,7 +1750,8 @@
apply auto
done
-lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
+lemma ln_x_over_x_mono:
+ fixes x::real shows "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
proof -
assume x: "exp 1 <= x" "x <= y"
moreover have "0 < exp (1::real)" by simp
@@ -1737,15 +1787,17 @@
finally show ?thesis using b by (simp add: field_simps)
qed
-lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
+lemma ln_le_minus_one:
+ fixes x::real shows "0 < x \<Longrightarrow> ln x \<le> x - 1"
using exp_ge_add_one_self[of "ln x"] by simp
lemma ln_eq_minus_one:
+ fixes x::real
assumes "0 < x" "ln x = x - 1"
shows "x = 1"
proof -
let ?l = "\<lambda>y. ln y - y + 1"
- have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
+ have D: "\<And>x::real. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
by (auto intro!: derivative_eq_intros)
show ?thesis
@@ -1814,11 +1866,11 @@
by (simp add: Deriv.DERIV_iff2)
qed
-lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
+lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
(auto simp: eventually_at_filter)
-lemma ln_at_top: "LIM x at_top. ln x :> at_top"
+lemma ln_at_top: "LIM x at_top. ln (x::real) :> at_top"
by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
(auto intro: eventually_gt_at_top)
@@ -1846,10 +1898,6 @@
qed
-definition powr :: "[real,real] => real" (infixr "powr" 80)
- -- {*exponentation with real exponent*}
- where "x powr a = exp(a * ln x)"
-
definition log :: "[real,real] => real"
-- {*logarithm of @{term x} to base @{term a}*}
where "log a x = ln x / ln a"
@@ -1891,67 +1939,77 @@
lemma powr_one_eq_one [simp]: "1 powr a = 1"
by (simp add: powr_def)
-lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
+lemma powr_zero_eq_one [simp]: "x powr 0 = (if x=0 then 0 else 1)"
by (simp add: powr_def)
-lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
- by (simp add: powr_def)
+lemma powr_one_gt_zero_iff [simp]:
+ fixes x::real shows "(x powr 1 = x) = (0 \<le> x)"
+ by (auto simp: powr_def)
declare powr_one_gt_zero_iff [THEN iffD2, simp]
-lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
+lemma powr_mult:
+ fixes x::real shows "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
-lemma powr_gt_zero [simp]: "0 < x powr a"
+lemma powr_ge_pzero [simp]:
+ fixes x::real shows "0 <= x powr y"
by (simp add: powr_def)
-lemma powr_ge_pzero [simp]: "0 <= x powr y"
- by (rule order_less_imp_le, rule powr_gt_zero)
-
-lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
- by (simp add: powr_def)
-
-lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
+lemma powr_divide:
+ fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
done
-lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
+lemma powr_divide2:
+ fixes x::real shows "x powr a / x powr b = x powr (a - b)"
apply (simp add: powr_def)
apply (subst exp_diff [THEN sym])
apply (simp add: left_diff_distrib)
done
-lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
+lemma powr_add:
+ fixes x::real shows "x powr (a + b) = (x powr a) * (x powr b)"
by (simp add: powr_def exp_add [symmetric] distrib_right)
-lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
+lemma powr_mult_base:
+ fixes x::real shows "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
using assms by (auto simp: powr_add)
-lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
+lemma powr_powr:
+ fixes x::real shows "(x powr a) powr b = x powr (a * b)"
by (simp add: powr_def)
-lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
+lemma powr_powr_swap:
+ fixes x::real shows "(x powr a) powr b = (x powr b) powr a"
by (simp add: powr_powr mult.commute)
-lemma powr_minus: "x powr (-a) = inverse (x powr a)"
+lemma powr_minus:
+ fixes x::real shows "x powr (-a) = inverse (x powr a)"
by (simp add: powr_def exp_minus [symmetric])
-lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
+lemma powr_minus_divide:
+ fixes x::real shows "x powr (-a) = 1/(x powr a)"
by (simp add: divide_inverse powr_minus)
-lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
+lemma divide_powr_uminus:
+ fixes a::real shows "a / b powr c = a * b powr (- c)"
by (simp add: powr_minus_divide)
-lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
+lemma powr_less_mono:
+ fixes x::real shows "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
by (simp add: powr_def)
-lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
+lemma powr_less_cancel:
+ fixes x::real shows "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
by (simp add: powr_def)
-lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
+lemma powr_less_cancel_iff [simp]:
+ fixes x::real shows "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
by (blast intro: powr_less_cancel powr_less_mono)
-lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
+lemma powr_le_cancel_iff [simp]:
+ fixes x::real shows "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
by (simp add: linorder_not_less [symmetric])
lemma log_ln: "ln x = log (exp(1)) x"
@@ -2007,6 +2065,9 @@
lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
by (simp add: log_mult divide_inverse log_inverse)
+lemma powr_gt_zero [simp]: "0 < x powr a \<longleftrightarrow> (x::real) \<noteq> 0"
+ by (simp add: powr_def)
+
lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"
@@ -2071,14 +2132,18 @@
lemma le_log_iff:
assumes "1 < b" "x > 0"
- shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> x"
- by (metis assms(1) assms(2) dual_order.strict_trans powr_le_cancel_iff powr_log_cancel
- powr_one_eq_one powr_one_gt_zero_iff)
+ shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> (x::real)"
+ using assms
+ apply auto
+ apply (metis (no_types, hide_lams) less_irrefl less_le_trans linear powr_le_cancel_iff
+ powr_log_cancel zero_less_one)
+ apply (metis not_less order.trans order_refl powr_le_cancel_iff powr_log_cancel zero_le_one)
+ done
lemma less_log_iff:
assumes "1 < b" "x > 0"
shows "y < log b x \<longleftrightarrow> b powr y < x"
- by (metis assms(1) assms(2) dual_order.strict_trans less_irrefl powr_less_cancel_iff
+ by (metis assms dual_order.strict_trans less_irrefl powr_less_cancel_iff
powr_log_cancel zero_less_one)
lemma
@@ -2136,22 +2201,28 @@
else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
by (auto simp: powr_int)
-lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
- using powr_realpow [of x 1] by simp
-
-lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
+lemma powr_one:
+ fixes x::real shows "0 \<le> x \<Longrightarrow> x powr 1 = x"
+ using powr_realpow [of x 1]
+ by simp
+
+lemma powr_numeral:
+ fixes x::real shows "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
by (fact powr_realpow_numeral)
-lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
+lemma powr_neg_one:
+ fixes x::real shows "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
using powr_int [of x "- 1"] by simp
-lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
+lemma powr_neg_numeral:
+ fixes x::real shows "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
using powr_int [of x "- numeral n"] by simp
lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
-lemma ln_powr: "ln (x powr y) = y * ln x"
+lemma ln_powr:
+ fixes x::real shows "x \<noteq> 0 \<Longrightarrow> ln (x powr y) = y * ln x"
by (simp add: powr_def)
lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) = ln b / n"
@@ -2163,7 +2234,7 @@
lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) = log b a / n"
by(simp add: log_def ln_root)
-lemma log_powr: "log b (x powr y) = y * log b x"
+lemma log_powr: "x \<noteq> 0 \<Longrightarrow> log b (x powr y) = y * log b x"
by (simp add: log_def ln_powr)
lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
@@ -2175,65 +2246,58 @@
lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
by (simp add: log_def ln_realpow)
-lemma log_base_powr: "log (a powr b) x = log a x / b"
+lemma log_base_powr: "a \<noteq> 0 \<Longrightarrow> log (a powr b) x = log a x / b"
by (simp add: log_def ln_powr)
lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
by(simp add: log_def ln_root)
-lemma ln_bound: "1 <= x ==> ln x <= x"
+lemma ln_bound:
+ fixes x::real shows "1 <= x ==> ln x <= x"
apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
apply simp
apply (rule ln_add_one_self_le_self, simp)
done
-lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
+lemma powr_mono:
+ fixes x::real shows "a <= b ==> 1 <= x ==> x powr a <= x powr b"
apply (cases "x = 1", simp)
apply (cases "a = b", simp)
apply (rule order_less_imp_le)
apply (rule powr_less_mono, auto)
done
-lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
- apply (subst powr_zero_eq_one [THEN sym])
- apply (rule powr_mono, assumption+)
- done
-
-lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
- apply (unfold powr_def)
- apply (rule exp_less_mono)
- apply (rule mult_strict_left_mono)
- apply (subst ln_less_cancel_iff, assumption)
- apply (rule order_less_trans)
- prefer 2
- apply assumption+
- done
-
-lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
- apply (unfold powr_def)
- apply (rule exp_less_mono)
- apply (rule mult_strict_left_mono_neg)
- apply (subst ln_less_cancel_iff)
- apply assumption
- apply (rule order_less_trans)
- prefer 2
- apply assumption+
- done
-
-lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
+lemma ge_one_powr_ge_zero:
+ fixes x::real shows "1 <= x ==> 0 <= a ==> 1 <= x powr a"
+using powr_mono by fastforce
+
+lemma powr_less_mono2:
+ fixes x::real shows "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
+ by (simp add: powr_def)
+
+
+lemma powr_less_mono2_neg:
+ fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
+ by (simp add: powr_def)
+
+lemma powr_mono2:
+ fixes x::real shows "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
apply (case_tac "a = 0", simp)
apply (case_tac "x = y", simp)
apply (metis less_eq_real_def powr_less_mono2)
done
-lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
+lemma powr_inj:
+ fixes x::real shows "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
unfolding powr_def exp_inj_iff by simp
-lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
- by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
- powr_gt_zero)
+lemma ln_powr_bound:
+ fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
+by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute mult_imp_le_div_pos not_less powr_gt_zero)
+
lemma ln_powr_bound2:
+ fixes x::real
assumes "1 < x" and "0 < a"
shows "(ln x) powr a <= (a powr a) * x"
proof -
@@ -2244,7 +2308,7 @@
finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
by (metis assms less_imp_le ln_gt_zero powr_mono2)
also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
- by (metis assms(2) powr_mult powr_gt_zero)
+ using assms powr_mult by auto
also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
by (rule powr_powr)
also have "... = x" using assms
@@ -2252,37 +2316,56 @@
finally show ?thesis .
qed
-lemma tendsto_powr [tendsto_intros]:
- "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
- unfolding powr_def by (intro tendsto_intros)
+lemma tendsto_powr [tendsto_intros]: (*FIXME a mess, suggests a general rule about exceptions*)
+ fixes a::real
+ shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
+ apply (simp add: powr_def)
+ apply (simp add: tendsto_def)
+ apply (simp add: Topological_Spaces.eventually_conj_iff )
+ apply safe
+ apply (case_tac "0 \<in> S")
+ apply (auto simp: )
+ apply (subgoal_tac "\<exists>T. open T & a : T & 0 \<notin> T")
+ apply clarify
+ apply (drule_tac x="T" in spec)
+ apply (simp add: )
+ apply (metis (mono_tags, lifting) eventually_mono)
+ apply (simp add: separation_t1)
+ apply (subgoal_tac "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F")
+ apply (simp add: tendsto_def)
+ apply (metis (mono_tags, lifting) eventually_mono)
+ apply (simp add: tendsto_def [symmetric])
+ apply (intro tendsto_intros)
+ apply (auto simp: )
+ done
lemma continuous_powr:
assumes "continuous F f"
and "continuous F g"
and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
- shows "continuous F (\<lambda>x. (f x) powr (g x))"
+ shows "continuous F (\<lambda>x. (f x) powr (g x :: real))"
using assms unfolding continuous_def by (rule tendsto_powr)
lemma continuous_at_within_powr[continuous_intros]:
assumes "continuous (at a within s) f"
and "continuous (at a within s) g"
and "f a \<noteq> 0"
- shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
+ shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x :: real))"
using assms unfolding continuous_within by (rule tendsto_powr)
lemma isCont_powr[continuous_intros, simp]:
- assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
+ assumes "isCont f a" "isCont g a" "f a \<noteq> (0::real)"
shows "isCont (\<lambda>x. (f x) powr g x) a"
using assms unfolding continuous_at by (rule tendsto_powr)
lemma continuous_on_powr[continuous_intros]:
- assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
+ assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> (0::real)"
shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
(* FIXME: generalize by replacing d by with g x and g ---> d? *)
lemma tendsto_zero_powrI:
- assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
+ assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> (0::real)) F"
and "0 < d"
shows "((\<lambda>x. f x powr d) ---> 0) F"
proof (rule tendstoI)
@@ -2303,14 +2386,17 @@
lemma tendsto_neg_powr:
assumes "s < 0"
and "LIM x F. f x :> at_top"
- shows "((\<lambda>x. f x powr s) ---> 0) F"
+ shows "((\<lambda>x. f x powr s) ---> (0::real)) F"
proof (rule tendstoI)
fix e :: real assume "0 < e"
def Z \<equiv> "e powr (1 / s)"
+ have "Z > 0"
+ using Z_def `0 < e` by auto
from assms have "eventually (\<lambda>x. Z < f x) F"
by (simp add: filterlim_at_top_dense)
moreover
- from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
+ from assms have "\<And>x::real. Z < x \<Longrightarrow> x powr s < Z powr s"
+ using `Z > 0`
by (auto simp: Z_def intro!: powr_less_mono2_neg)
with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
by (simp add: powr_powr Z_def dist_real_def)
@@ -2318,13 +2404,11 @@
show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
qed
-(* it is funny that this isn't in the library! It could go in Transcendental *)
lemma tendsto_exp_limit_at_right:
fixes x :: real
shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
proof cases
assume "x \<noteq> 0"
-
have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
by (auto intro!: derivative_eq_intros)
then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
@@ -2335,7 +2419,10 @@
proof (rule filterlim_mono_eventually)
show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
unfolding eventually_at_right[OF zero_less_one]
- using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
+ using `x \<noteq> 0`
+ apply (intro exI[of _ "1 / \<bar>x\<bar>"])
+ apply (auto simp: field_simps powr_def abs_if)
+ by (metis add_less_same_cancel1 mult_less_0_iff not_less_iff_gr_or_eq zero_less_one)
qed (simp_all add: at_eq_sup_left_right)
qed simp
@@ -4445,7 +4532,7 @@
lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
apply (rule trans [OF sin_mono_less_eq [symmetric]])
using arcsin_ubound arcsin_lbound
- apply (auto simp: )
+ apply auto
done
lemma arcsin_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
@@ -4460,7 +4547,7 @@
lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
apply (rule trans [OF cos_mono_less_eq [symmetric]])
using arccos_ubound arccos_lbound
- apply (auto simp: )
+ apply auto
done
lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
@@ -5009,4 +5096,253 @@
qed
qed
+
+subsection{*Basics about polynomial functions: extremal behaviour and root counts*}
+(*ALL COULD GO TO COMPLEX_MAIN OR EARLIER*)
+
+lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*)
+ fixes x :: "'a::idom"
+ assumes "1 \<le> n"
+ shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
+ (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
+proof -
+ have h: "bij_betw (\<lambda>(i,j). (j,i)) ((SIGMA i : atMost n. lessThan i)) (SIGMA j : lessThan n. {Suc j..n})"
+ by (auto simp: bij_betw_def inj_on_def)
+ have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
+ (\<Sum>i\<le>n. a i * (x^i - y^i))"
+ by (simp add: right_diff_distrib setsum_subtractf)
+ also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
+ by (simp add: power_diff_sumr2 mult.assoc)
+ also have "... = (\<Sum>i\<le>n. \<Sum>j<i. a i * (x - y) * (y^(i - Suc j) * x^j))"
+ by (simp add: setsum_right_distrib)
+ also have "... = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
+ by (simp add: setsum.Sigma)
+ also have "... = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
+ by (auto simp add: setsum.reindex_bij_betw [OF h, symmetric] intro: setsum.strong_cong)
+ also have "... = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
+ by (simp add: setsum.Sigma)
+ also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
+ by (simp add: setsum_right_distrib mult_ac)
+ finally show ?thesis .
+qed
+
+lemma polyfun_diff_alt: (*COMPLEX_SUB_POLYFUN_ALT in HOL Light*)
+ fixes x :: "'a::idom"
+ assumes "1 \<le> n"
+ shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
+ (x - y) * ((\<Sum>j<n. \<Sum>k<n-j. a(j+k+1) * y^k * x^j))"
+proof -
+ { fix j::nat
+ assume "j<n"
+ have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
+ apply (auto simp: bij_betw_def inj_on_def)
+ apply (rule_tac x="x + Suc j" in image_eqI)
+ apply (auto simp: )
+ done
+ have "(\<Sum>i=Suc j..n. a i * y^(i - j - 1)) = (\<Sum>k<n-j. a(j+k+1) * y^k)"
+ by (auto simp add: setsum.reindex_bij_betw [OF h, symmetric] intro: setsum.strong_cong)
+ }
+ then show ?thesis
+ by (simp add: polyfun_diff [OF assms] setsum_left_distrib)
+qed
+
+lemma polyfun_linear_factor: (*COMPLEX_POLYFUN_LINEAR_FACTOR in HOL Light*)
+ fixes a :: "'a::idom"
+ shows "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c(i) * z^i) = (z - a) * (\<Sum>i<n. b(i) * z^i) + (\<Sum>i\<le>n. c(i) * a^i)"
+proof (cases "n=0")
+ case True then show ?thesis
+ by simp
+next
+ case False
+ have "(\<exists>b. \<forall>z. (\<Sum>i\<le>n. c(i) * z^i) = (z - a) * (\<Sum>i<n. b(i) * z^i) + (\<Sum>i\<le>n. c(i) * a^i)) =
+ (\<exists>b. \<forall>z. (\<Sum>i\<le>n. c(i) * z^i) - (\<Sum>i\<le>n. c(i) * a^i) = (z - a) * (\<Sum>i<n. b(i) * z^i))"
+ by (simp add: algebra_simps)
+ also have "... = (\<exists>b. \<forall>z. (z - a) * (\<Sum>j<n. (\<Sum>i = Suc j..n. c i * a^(i - Suc j)) * z^j) = (z - a) * (\<Sum>i<n. b(i) * z^i))"
+ using False by (simp add: polyfun_diff)
+ also have "... = True"
+ by auto
+ finally show ?thesis
+ by simp
+qed
+
+lemma polyfun_linear_factor_root: (*COMPLEX_POLYFUN_LINEAR_FACTOR_ROOT in HOL Light*)
+ fixes a :: "'a::idom"
+ assumes "(\<Sum>i\<le>n. c(i) * a^i) = 0"
+ obtains b where "\<And>z. (\<Sum>i\<le>n. c(i) * z^i) = (z - a) * (\<Sum>i<n. b(i) * z^i)"
+ using polyfun_linear_factor [of c n a] assms
+ by auto
+
+lemma isCont_polynom:
+ fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+ shows "isCont (\<lambda>w. \<Sum>i\<le>n. c i * w^i) a"
+ by simp
+
+lemma zero_polynom_imp_zero_coeffs:
+ fixes c :: "nat \<Rightarrow> 'a::{ab_semigroup_mult,real_normed_div_algebra}"
+ assumes "\<And>w. (\<Sum>i\<le>n. c i * w^i) = 0" "k \<le> n"
+ shows "c k = 0"
+using assms
+proof (induction n arbitrary: c k)
+ case 0
+ then show ?case
+ by simp
+next
+ case (Suc n c k)
+ have [simp]: "c 0 = 0" using Suc.prems(1) [of 0]
+ by simp
+ { fix w
+ have "(\<Sum>i\<le>Suc n. c i * w^i) = (\<Sum>i\<le>n. c (Suc i) * w ^ Suc i)"
+ unfolding Set_Interval.setsum_atMost_Suc_shift
+ by simp
+ also have "... = w * (\<Sum>i\<le>n. c (Suc i) * w^i)"
+ by (simp add: power_Suc mult_ac setsum_right_distrib del: setsum_atMost_Suc)
+ finally have "(\<Sum>i\<le>Suc n. c i * w^i) = w * (\<Sum>i\<le>n. c (Suc i) * w^i)" .
+ }
+ then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
+ using Suc by auto
+ then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
+ by (simp cong: LIM_cong) --{*the case @{term"w=0"} by continuity}*}
+ then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
+ using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
+ by (force simp add: Limits.isCont_iff)
+ then have "\<And>w. (\<Sum>i\<le>n. c (Suc i) * w^i) = 0" using wnz
+ by metis
+ then have "\<And>i. i\<le>n \<Longrightarrow> c (Suc i) = 0"
+ using Suc.IH [of "\<lambda>i. c (Suc i)"]
+ by blast
+ then show ?case using `k \<le> Suc n`
+ by (cases k) auto
+qed
+
+lemma polyfun_rootbound: (*COMPLEX_POLYFUN_ROOTBOUND in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
+ assumes "c k \<noteq> 0" "k\<le>n"
+ shows "finite {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<and>
+ card {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<le> n"
+using assms
+proof (induction n arbitrary: c k)
+ case 0
+ then show ?case
+ by simp
+next
+ case (Suc m c k)
+ let ?succase = ?case
+ show ?case
+ proof (cases "{z. (\<Sum>i\<le>Suc m. c(i) * z^i) = 0} = {}")
+ case True
+ then show ?succase
+ by simp
+ next
+ case False
+ then obtain z0 where z0: "(\<Sum>i\<le>Suc m. c(i) * z0^i) = 0"
+ by blast
+ then obtain b where b: "\<And>w. (\<Sum>i\<le>Suc m. c i * w^i) = (w - z0) * (\<Sum>i\<le>m. b i * w^i)"
+ using polyfun_linear_factor_root [OF z0, unfolded lessThan_Suc_atMost]
+ by blast
+ then have eq: "{z. (\<Sum>i\<le>Suc m. c(i) * z^i) = 0} = insert z0 {z. (\<Sum>i\<le>m. b(i) * z^i) = 0}"
+ by auto
+ have "~(\<forall>k\<le>m. b k = 0)"
+ proof
+ assume [simp]: "\<forall>k\<le>m. b k = 0"
+ then have "\<And>w. (\<Sum>i\<le>m. b i * w^i) = 0"
+ by simp
+ then have "\<And>w. (\<Sum>i\<le>Suc m. c i * w^i) = 0"
+ using b by simp
+ then have "\<And>k. k \<le> Suc m \<Longrightarrow> c k = 0"
+ using zero_polynom_imp_zero_coeffs
+ by blast
+ then show False using Suc.prems
+ by blast
+ qed
+ then obtain k' where bk': "b k' \<noteq> 0" "k' \<le> m"
+ by blast
+ show ?succase
+ using Suc.IH [of b k'] bk'
+ by (simp add: eq card_insert_if del: setsum_atMost_Suc)
+ qed
+qed
+
+lemma
+ fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
+ assumes "c k \<noteq> 0" "k\<le>n"
+ shows polyfun_roots_finite: "finite {z. (\<Sum>i\<le>n. c(i) * z^i) = 0}"
+ and polyfun_roots_card: "card {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<le> n"
+using polyfun_rootbound assms
+ by auto
+
+lemma polyfun_finite_roots: (*COMPLEX_POLYFUN_FINITE_ROOTS in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
+ shows "finite {x. (\<Sum>i\<le>n. c i * x^i) = 0} \<longleftrightarrow> (\<exists>i\<le>n. c i \<noteq> 0)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ moreover
+ { assume "\<forall>i\<le>n. c i = 0"
+ then have "\<And>x. (\<Sum>i\<le>n. c i * x^i) = 0"
+ by simp
+ then have "\<not> finite {x. (\<Sum>i\<le>n. c i * x^i) = 0}"
+ using ex_new_if_finite [OF infinite_UNIV_char_0 [where 'a='a]]
+ by auto
+ }
+ ultimately show ?rhs
+ by metis
+next
+ assume ?rhs
+ then show ?lhs
+ using polyfun_rootbound
+ by blast
+qed
+
+lemma polyfun_eq_0: (*COMPLEX_POLYFUN_EQ_0 in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
+ shows "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = 0) \<longleftrightarrow> (\<forall>i\<le>n. c i = 0)"
+ using zero_polynom_imp_zero_coeffs by auto
+
+lemma polyfun_eq_coeffs:
+ fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
+ shows "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = (\<Sum>i\<le>n. d i * x^i)) \<longleftrightarrow> (\<forall>i\<le>n. c i = d i)"
+proof -
+ have "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = (\<Sum>i\<le>n. d i * x^i)) \<longleftrightarrow> (\<forall>x. (\<Sum>i\<le>n. (c i - d i) * x^i) = 0)"
+ by (simp add: left_diff_distrib Groups_Big.setsum_subtractf)
+ also have "... \<longleftrightarrow> (\<forall>i\<le>n. c i - d i = 0)"
+ by (rule polyfun_eq_0)
+ finally show ?thesis
+ by simp
+qed
+
+lemma polyfun_eq_const: (*COMPLEX_POLYFUN_EQ_CONST in HOL Light*)
+ fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
+ shows "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = k) \<longleftrightarrow> c 0 = k \<and> (\<forall>i \<in> {1..n}. c i = 0)"
+ (is "?lhs = ?rhs")
+proof -
+ have *: "\<forall>x. (\<Sum>i\<le>n. (if i=0 then k else 0) * x^i) = k"
+ by (induct n) auto
+ show ?thesis
+ proof
+ assume ?lhs
+ with * have "(\<forall>i\<le>n. c i = (if i=0 then k else 0))"
+ by (simp add: polyfun_eq_coeffs [symmetric])
+ then show ?rhs
+ by simp
+ next
+ assume ?rhs then show ?lhs
+ by (induct n) auto
+ qed
+qed
+
+lemma root_polyfun:
+ fixes z:: "'a::idom"
+ assumes "1 \<le> n"
+ shows "z^n = a \<longleftrightarrow> (\<Sum>i\<le>n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0"
+ using assms
+ by (cases n; simp add: setsum_head_Suc atLeast0AtMost [symmetric])
+
+lemma
+ fixes zz :: "'a::{idom,real_normed_div_algebra}"
+ assumes "1 \<le> n"
+ shows finite_roots_unity: "finite {z::'a. z^n = 1}"
+ and card_roots_unity: "card {z::'a. z^n = 1} \<le> n"
+ using polyfun_rootbound [of "\<lambda>i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms
+ by (auto simp add: root_polyfun [OF assms])
+
end