--- a/src/HOL/Library/Formal_Power_Series.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Aug 02 21:30:30 2016 +0200
@@ -4457,7 +4457,7 @@
text \<open>Connection to E c over the complex numbers --- Euler and de Moivre.\<close>
-lemma Eii_sin_cos: "E (ii * c) = fps_cos c + fps_const ii * fps_sin c"
+lemma Eii_sin_cos: "E (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c"
(is "?l = ?r")
proof -
have "?l $ n = ?r $ n" for n
@@ -4477,7 +4477,7 @@
by (simp add: fps_eq_iff)
qed
-lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c"
+lemma E_minus_ii_sin_cos: "E (- (\<i> * c)) = fps_cos c - fps_const \<i> * fps_sin c"
unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd)
lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
@@ -4490,7 +4490,7 @@
lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
by (fact numeral_fps_const) (* FIXME: duplicate *)
-lemma fps_cos_Eii: "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
+lemma fps_cos_Eii: "fps_cos c = (E (\<i> * c) + E (- \<i> * c)) / fps_const 2"
proof -
have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2"
by (simp add: numeral_fps_const)
@@ -4499,9 +4499,9 @@
by (simp add: fps_sin_even fps_cos_odd numeral_fps_const fps_divide_unit fps_const_inverse th)
qed
-lemma fps_sin_Eii: "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)"
+lemma fps_sin_Eii: "fps_sin c = (E (\<i> * c) - E (- \<i> * c)) / fps_const (2*\<i>)"
proof -
- have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * ii)"
+ have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * \<i>)"
by (simp add: fps_eq_iff numeral_fps_const)
show ?thesis
unfolding Eii_sin_cos minus_mult_commute
@@ -4509,15 +4509,15 @@
qed
lemma fps_tan_Eii:
- "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))"
+ "fps_tan c = (E (\<i> * c) - E (- \<i> * c)) / (fps_const \<i> * (E (\<i> * c) + E (- \<i> * c)))"
unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg
apply (simp add: fps_divide_unit fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
apply simp
done
lemma fps_demoivre:
- "(fps_cos a + fps_const ii * fps_sin a)^n =
- fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)"
+ "(fps_cos a + fps_const \<i> * fps_sin a)^n =
+ fps_cos (of_nat n * a) + fps_const \<i> * fps_sin (of_nat n * a)"
unfolding Eii_sin_cos[symmetric] E_power_mult
by (simp add: ac_simps)
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Aug 02 21:30:30 2016 +0200
@@ -126,13 +126,13 @@
lemma unimodular_reduce_norm:
assumes md: "cmod z = 1"
- shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
+ shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + \<i>) < 1 \<or> cmod (z - \<i>) < 1"
proof -
obtain x y where z: "z = Complex x y "
by (cases z) auto
from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1"
by (simp add: cmod_def)
- have False if "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
+ have False if "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + \<i>) \<ge> 1" "cmod (z - \<i>) \<ge> 1"
proof -
from that z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
by (simp_all add: cmod_def power2_eq_square algebra_simps)
@@ -190,17 +190,17 @@
apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1")
apply (rule_tac x="-1" in exI)
apply simp
- apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
+ apply (cases "cmod (complex_of_real (cmod b) / b + \<i>) < 1")
apply (cases "even m")
- apply (rule_tac x="ii" in exI)
+ apply (rule_tac x="\<i>" in exI)
apply (simp add: m power_mult)
- apply (rule_tac x="- ii" in exI)
+ apply (rule_tac x="- \<i>" in exI)
apply (simp add: m power_mult)
apply (cases "even m")
- apply (rule_tac x="- ii" in exI)
+ apply (rule_tac x="- \<i>" in exI)
apply (simp add: m power_mult)
apply (auto simp add: m power_mult)
- apply (rule_tac x="ii" in exI)
+ apply (rule_tac x="\<i>" in exI)
apply (auto simp add: m power_mult)
done
then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1"
--- a/src/HOL/Library/Inner_Product.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Library/Inner_Product.thy Tue Aug 02 21:30:30 2016 +0200
@@ -293,10 +293,10 @@
lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
unfolding inner_complex_def by simp
-lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
+lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
unfolding inner_complex_def by simp
-lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
+lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
unfolding inner_complex_def by simp
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Aug 02 21:30:30 2016 +0200
@@ -3453,7 +3453,7 @@
pathstart p = pathstart \<gamma> \<and>
pathfinish p = pathfinish \<gamma> \<and>
(\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
- contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
lemma winding_number:
assumes "path \<gamma>" "z \<notin> path_image \<gamma>" "0 < e"
@@ -3461,7 +3461,7 @@
pathstart p = pathstart \<gamma> \<and>
pathfinish p = pathfinish \<gamma> \<and>
(\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
- contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * winding_number \<gamma> z"
+ contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * winding_number \<gamma> z"
proof -
have "path_image \<gamma> \<subseteq> UNIV - {z}"
using assms by blast
@@ -3476,11 +3476,11 @@
then obtain h where h: "polynomial_function h \<and> pathstart h = pathstart \<gamma> \<and> pathfinish h = pathfinish \<gamma> \<and>
(\<forall>t \<in> {0..1}. norm(h t - \<gamma> t) < d/2)"
using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "d/2"] d by auto
- define nn where "nn = 1/(2* pi*ii) * contour_integral h (\<lambda>w. 1/(w - z))"
+ define nn where "nn = 1/(2* pi*\<i>) * contour_integral h (\<lambda>w. 1/(w - z))"
have "\<exists>n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
(\<forall>t \<in> {0..1}. norm(\<gamma> t - p t) < e) \<and>
- contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
(is "\<exists>n. \<forall>e > 0. ?PP e n")
proof (rule_tac x=nn in exI, clarify)
fix e::real
@@ -3509,7 +3509,7 @@
"\<And>e. e>0 \<Longrightarrow> \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
(\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
- contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
shows "winding_number \<gamma> z = n"
proof -
have "path_image \<gamma> \<subseteq> UNIV - {z}"
@@ -3525,7 +3525,7 @@
"valid_path p \<and> z \<notin> path_image p \<and>
pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and>
(\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
- contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
using pi [OF e] by blast
obtain q where q:
"valid_path q \<and> z \<notin> path_image q \<and>
@@ -3552,7 +3552,7 @@
"\<And>e. e>0 \<Longrightarrow> \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
pathfinish p = pathstart p \<and>
(\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
- contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
shows "winding_number \<gamma> z = n"
proof -
have "path_image \<gamma> \<subseteq> UNIV - {z}"
@@ -3568,7 +3568,7 @@
"valid_path p \<and> z \<notin> path_image p \<and>
pathfinish p = pathstart p \<and>
(\<forall>t \<in> {0..1}. norm (\<gamma> t - p t) < e) \<and>
- contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * ii * n"
+ contour_integral p (\<lambda>w. 1/(w - z)) = 2 * pi * \<i> * n"
using pi [OF e] by blast
obtain q where q:
"valid_path q \<and> z \<notin> path_image q \<and>
@@ -3590,12 +3590,12 @@
lemma winding_number_valid_path:
assumes "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
- shows "winding_number \<gamma> z = 1/(2*pi*ii) * contour_integral \<gamma> (\<lambda>w. 1/(w - z))"
+ shows "winding_number \<gamma> z = 1/(2*pi*\<i>) * contour_integral \<gamma> (\<lambda>w. 1/(w - z))"
using assms by (auto simp: valid_path_imp_path intro!: winding_number_unique)
lemma has_contour_integral_winding_number:
assumes \<gamma>: "valid_path \<gamma>" "z \<notin> path_image \<gamma>"
- shows "((\<lambda>w. 1/(w - z)) has_contour_integral (2*pi*ii*winding_number \<gamma> z)) \<gamma>"
+ shows "((\<lambda>w. 1/(w - z)) has_contour_integral (2*pi*\<i>*winding_number \<gamma> z)) \<gamma>"
by (simp add: winding_number_valid_path has_contour_integral_integral contour_integrable_inversediff assms)
lemma winding_number_trivial [simp]: "z \<noteq> a \<Longrightarrow> winding_number(linepath a a) z = 0"
@@ -3697,7 +3697,7 @@
show ?thesis
apply (simp add: Re_winding_number [OF \<gamma>] field_simps)
apply (rule has_integral_component_nonneg
- [of ii "\<lambda>x. if x \<in> {0<..<1}
+ [of \<i> "\<lambda>x. if x \<in> {0<..<1}
then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else 0", simplified])
prefer 3 apply (force simp: *)
apply (simp add: Basis_complex_def)
@@ -3718,8 +3718,8 @@
proof -
have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
apply (rule has_integral_component_le
- [of ii "\<lambda>x. ii*e" "ii*e" "{0..1}"
- "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else ii*e"
+ [of \<i> "\<lambda>x. \<i>*e" "\<i>*e" "{0..1}"
+ "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else \<i>*e"
"contour_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
using e
apply (simp_all add: Basis_complex_def)
@@ -3874,7 +3874,7 @@
corollary winding_number_exp_2pi:
"\<lbrakk>path p; z \<notin> path_image p\<rbrakk>
- \<Longrightarrow> pathfinish p - z = exp (2 * pi * ii * winding_number p z) * (pathstart p - z)"
+ \<Longrightarrow> pathfinish p - z = exp (2 * pi * \<i> * winding_number p z) * (pathstart p - z)"
using winding_number [of p z 1] unfolding valid_path_def path_image_def pathstart_def pathfinish_def
by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps contour_integral_integral exp_minus)
@@ -4330,7 +4330,7 @@
if x: "0 \<le> x" "x \<le> 1" for x
proof -
have "integral {0..x} (\<lambda>t. vector_derivative \<gamma> (at t) / (\<gamma> t - z)) / (2 * of_real pi * \<i>) =
- 1 / (2*pi*ii) * contour_integral (subpath 0 x \<gamma>) (\<lambda>w. 1/(w - z))"
+ 1 / (2*pi*\<i>) * contour_integral (subpath 0 x \<gamma>) (\<lambda>w. 1/(w - z))"
using assms x
apply (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff])
done
@@ -4343,7 +4343,7 @@
qed
show ?thesis
apply (rule continuous_on_eq
- [where f = "\<lambda>x. 1 / (2*pi*ii) *
+ [where f = "\<lambda>x. 1 / (2*pi*\<i>) *
integral {0..x} (\<lambda>t. 1/(\<gamma> t - z) * vector_derivative \<gamma> (at t))"])
apply (rule continuous_intros)+
apply (rule indefinite_integral_continuous)
@@ -4491,7 +4491,7 @@
and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
and z: "z \<in> interior s - k" and vpg: "valid_path \<gamma>"
and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
- shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+ shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
proof -
obtain f' where f': "(f has_field_derivative f') (at z)"
using fcd [OF z] by (auto simp: field_differentiable_def)
@@ -4536,7 +4536,7 @@
theorem Cauchy_integral_formula_convex_simple:
"\<lbrakk>convex s; f holomorphic_on s; z \<in> interior s; valid_path \<gamma>; path_image \<gamma> \<subseteq> s - {z};
pathfinish \<gamma> = pathstart \<gamma>\<rbrakk>
- \<Longrightarrow> ((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+ \<Longrightarrow> ((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
apply (rule Cauchy_integral_formula_weak [where k = "{}"])
using holomorphic_on_imp_continuous_on
by auto (metis at_within_interior holomorphic_on_def interiorE subsetCE)
@@ -4856,19 +4856,19 @@
subsection\<open>Partial circle path\<close>
definition part_circlepath :: "[complex, real, real, real, real] \<Rightarrow> complex"
- where "part_circlepath z r s t \<equiv> \<lambda>x. z + of_real r * exp (ii * of_real (linepath s t x))"
+ where "part_circlepath z r s t \<equiv> \<lambda>x. z + of_real r * exp (\<i> * of_real (linepath s t x))"
lemma pathstart_part_circlepath [simp]:
- "pathstart(part_circlepath z r s t) = z + r*exp(ii * s)"
+ "pathstart(part_circlepath z r s t) = z + r*exp(\<i> * s)"
by (metis part_circlepath_def pathstart_def pathstart_linepath)
lemma pathfinish_part_circlepath [simp]:
- "pathfinish(part_circlepath z r s t) = z + r*exp(ii*t)"
+ "pathfinish(part_circlepath z r s t) = z + r*exp(\<i>*t)"
by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
proposition has_vector_derivative_part_circlepath [derivative_intros]:
"((part_circlepath z r s t) has_vector_derivative
- (ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)))
+ (\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
(at x within X)"
apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real)
apply (rule has_vector_derivative_real_complex)
@@ -4877,13 +4877,13 @@
corollary vector_derivative_part_circlepath:
"vector_derivative (part_circlepath z r s t) (at x) =
- ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+ \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
using has_vector_derivative_part_circlepath vector_derivative_at by blast
corollary vector_derivative_part_circlepath01:
"\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
\<Longrightarrow> vector_derivative (part_circlepath z r s t) (at x within {0..1}) =
- ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)"
+ \<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
using has_vector_derivative_part_circlepath
by (auto simp: vector_derivative_at_within_ivl)
@@ -4899,7 +4899,7 @@
proposition path_image_part_circlepath:
assumes "s \<le> t"
- shows "path_image (part_circlepath z r s t) = {z + r * exp(ii * of_real x) | x. s \<le> x \<and> x \<le> t}"
+ shows "path_image (part_circlepath z r s t) = {z + r * exp(\<i> * of_real x) | x. s \<le> x \<and> x \<le> t}"
proof -
{ fix z::real
assume "0 \<le> z" "z \<le> 1"
@@ -4986,7 +4986,7 @@
by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
have "finite (part_circlepath z r s t -` {y} \<inter> {0..1})" if "y \<in> k" for y
proof -
- define w where "w = (y - z)/of_real r / exp(ii * of_real s)"
+ define w where "w = (y - z)/of_real r / exp(\<i> * of_real s)"
have fin: "finite (of_real -` {z. cmod z \<le> 1 \<and> exp (\<i> * complex_of_real (t - s) * z) = w})"
apply (rule finite_vimageI [OF finite_bounded_log2])
using \<open>s < t\<close> apply (auto simp: inj_of_real)
@@ -5063,7 +5063,7 @@
done
next
case False then have "r \<noteq> 0" "s \<noteq> t" by auto
- have *: "\<And>x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z \<longleftrightarrow> ii*(x - y) * (t - s) = z"
+ have *: "\<And>x y z s t. \<i>*((1 - x) * s + x * t) = \<i>*(((1 - y) * s + y * t)) + z \<longleftrightarrow> \<i>*(x - y) * (t - s) = z"
by (simp add: algebra_simps)
have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
\<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> \<bar>x - y\<bar> \<in> {0,1})"
@@ -5134,7 +5134,7 @@
definition circlepath :: "[complex, real, real] \<Rightarrow> complex"
where "circlepath z r \<equiv> part_circlepath z r 0 (2*pi)"
-lemma circlepath: "circlepath z r = (\<lambda>x. z + r * exp(2 * of_real pi * ii * of_real x))"
+lemma circlepath: "circlepath z r = (\<lambda>x. z + r * exp(2 * of_real pi * \<i> * of_real x))"
by (simp add: circlepath_def part_circlepath_def linepath_def algebra_simps)
lemma pathstart_circlepath [simp]: "pathstart (circlepath z r) = z + r"
@@ -5173,7 +5173,7 @@
using path_image_circlepath_minus_subset by fastforce
proposition has_vector_derivative_circlepath [derivative_intros]:
- "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x)))
+ "((circlepath z r) has_vector_derivative (2 * pi * \<i> * r * exp (2 * of_real pi * \<i> * of_real x)))
(at x within X)"
apply (simp add: circlepath_def scaleR_conv_of_real)
apply (rule derivative_eq_intros)
@@ -5182,13 +5182,13 @@
corollary vector_derivative_circlepath:
"vector_derivative (circlepath z r) (at x) =
- 2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+ 2 * pi * \<i> * r * exp(2 * of_real pi * \<i> * x)"
using has_vector_derivative_circlepath vector_derivative_at by blast
corollary vector_derivative_circlepath01:
"\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
\<Longrightarrow> vector_derivative (circlepath z r) (at x within {0..1}) =
- 2 * pi * ii * r * exp(2 * of_real pi * ii * x)"
+ 2 * pi * \<i> * r * exp(2 * of_real pi * \<i> * x)"
using has_vector_derivative_circlepath
by (auto simp: vector_derivative_at_within_ivl)
@@ -5300,7 +5300,7 @@
theorem Cauchy_integral_circlepath:
assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r"
- shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+ shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * \<i> * f w))
(circlepath z r)"
proof -
have "r > 0"
@@ -5320,7 +5320,7 @@
corollary Cauchy_integral_circlepath_simple:
assumes "f holomorphic_on cball z r" "norm(w - z) < r"
- shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w))
+ shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * \<i> * f w))
(circlepath z r)"
using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath)
@@ -5634,7 +5634,7 @@
and w: "w \<in> ball z r"
shows "(\<lambda>u. f u/(u - w)^2) contour_integrable_on (circlepath z r)"
(is "?thes1")
- and "(f has_field_derivative (1 / (2 * of_real pi * ii) * contour_integral(circlepath z r) (\<lambda>u. f u / (u - w)^2))) (at w)"
+ and "(f has_field_derivative (1 / (2 * of_real pi * \<i>) * contour_integral(circlepath z r) (\<lambda>u. f u / (u - w)^2))) (at w)"
(is "?thes2")
proof -
have [simp]: "r \<ge> 0" using w
@@ -5642,7 +5642,7 @@
have f: "continuous_on (path_image (circlepath z r)) f"
by (rule continuous_on_subset [OF contf]) (force simp add: cball_def sphere_def)
have int: "\<And>w. dist z w < r \<Longrightarrow>
- ((\<lambda>u. f u / (u - w)) has_contour_integral (\<lambda>x. 2 * of_real pi * ii * f x) w) (circlepath z r)"
+ ((\<lambda>u. f u / (u - w)) has_contour_integral (\<lambda>x. 2 * of_real pi * \<i> * f x) w) (circlepath z r)"
by (rule Cauchy_integral_circlepath [OF contf holf]) (simp add: dist_norm norm_minus_commute)
show ?thes1
apply (simp add: power2_eq_square)
@@ -5651,7 +5651,7 @@
done
have "((\<lambda>x. 2 * of_real pi * \<i> * f x) has_field_derivative contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)^2)) (at w)"
apply (simp add: power2_eq_square)
- apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\<lambda>x. 2 * of_real pi * ii * f x", simplified])
+ apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\<lambda>x. 2 * of_real pi * \<i> * f x", simplified])
apply (blast intro: int)
done
then have fder: "(f has_field_derivative contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)^2) / (2 * of_real pi * \<i>)) (at w)"
@@ -5676,7 +5676,7 @@
using field_differentiable_at_within field_differentiable_def fder by blast
then have "continuous_on (path_image (circlepath z r)) f"
using \<open>r > 0\<close> by (force elim: holomorphic_on_subset [THEN holomorphic_on_imp_continuous_on])
- then have contfpi: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1/(2 * of_real pi*ii) * f x)"
+ then have contfpi: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1/(2 * of_real pi*\<i>) * f x)"
by (auto intro: continuous_intros)+
have contf_cball: "continuous_on (cball z r) f" using holf_cball
by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset)
@@ -6079,7 +6079,7 @@
and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
and z: "z \<in> interior s" and vpg: "valid_path \<gamma>"
and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
- shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+ shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def)
using no_isolated_singularity [where s = "interior s"]
@@ -6096,7 +6096,7 @@
assumes contf: "continuous_on (cball z r) f"
and holf: "f holomorphic_on ball z r"
and w: "w \<in> ball z r"
- shows "((\<lambda>u. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * ii) / (fact k) * (deriv ^^ k) f w))
+ shows "((\<lambda>u. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * \<i>) / (fact k) * (deriv ^^ k) f w))
(circlepath z r)"
using w
proof (induction k arbitrary: w)
@@ -6137,7 +6137,7 @@
and w: "w \<in> ball z r"
shows "(\<lambda>u. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)"
(is "?thes1")
- and "(deriv ^^ k) f w = (fact k) / (2 * pi * ii) * contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k))"
+ and "(deriv ^^ k) f w = (fact k) / (2 * pi * \<i>) * contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k))"
(is "?thes2")
proof -
have *: "((\<lambda>u. f u / (u - w) ^ Suc k) has_contour_integral (2 * pi) * \<i> / (fact k) * (deriv ^^ k) f w)
@@ -6152,12 +6152,12 @@
corollary Cauchy_contour_integral_circlepath:
assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \<in> ball z r"
- shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)) = (2 * pi * ii) * (deriv ^^ k) f w / (fact k)"
+ shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)) = (2 * pi * \<i>) * (deriv ^^ k) f w / (fact k)"
by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms])
corollary Cauchy_contour_integral_circlepath_2:
assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \<in> ball z r"
- shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^2) = (2 * pi * ii) * deriv f w"
+ shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^2) = (2 * pi * \<i>) * deriv f w"
using Cauchy_contour_integral_circlepath [OF assms, of 1]
by (simp add: power2_eq_square)
@@ -6263,10 +6263,10 @@
apply auto
done
then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
- sums (2 * of_real pi * ii * f w)"
+ sums (2 * of_real pi * \<i> * f w)"
using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]])
then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2)))
- sums ((2 * of_real pi * ii * f w) / (\<i> * (complex_of_real pi * 2)))"
+ sums ((2 * of_real pi * \<i> * f w) / (\<i> * (complex_of_real pi * 2)))"
by (rule sums_divide)
then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2)))
sums f w"
@@ -6407,7 +6407,7 @@
by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) \<longlongrightarrow> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
- have f_tends_cig: "((\<lambda>n. 2 * of_real pi * ii * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
+ have f_tends_cig: "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. f n u/(u - w))"])
apply (rule eventually_mono [OF cont])
apply (rule contour_integral_unique [OF Cauchy_integral_circlepath])
@@ -7077,7 +7077,7 @@
and z: "z \<in> u" and \<gamma>: "polynomial_function \<gamma>"
and pasz: "path_image \<gamma> \<subseteq> u - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
and zero: "\<And>w. w \<notin> u \<Longrightarrow> winding_number \<gamma> w = 0"
- shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+ shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
proof -
obtain \<gamma>' where pf\<gamma>': "polynomial_function \<gamma>'" and \<gamma>': "\<And>x. (\<gamma> has_vector_derivative (\<gamma>' x)) (at x)"
using has_vector_derivative_polynomial_function [OF \<gamma>] by blast
@@ -7468,7 +7468,7 @@
and z: "z \<in> s" and vpg: "valid_path \<gamma>"
and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
and zero: "\<And>w. w \<notin> s \<Longrightarrow> winding_number \<gamma> w = 0"
- shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+ shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
proof -
have "path \<gamma>" using vpg by (blast intro: valid_path_imp_path)
have hols: "(\<lambda>w. f w / (w - z)) holomorphic_on s - {z}" "(\<lambda>w. 1 / (w - z)) holomorphic_on s - {z}"
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Aug 02 21:30:30 2016 +0200
@@ -75,44 +75,44 @@
subsection\<open>Euler and de Moivre formulas.\<close>
text\<open>The sine series times @{term i}\<close>
-lemma sin_ii_eq: "(\<lambda>n. (ii * sin_coeff n) * z^n) sums (ii * sin z)"
+lemma sin_ii_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
proof -
- have "(\<lambda>n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)"
+ have "(\<lambda>n. \<i> * sin_coeff n *\<^sub>R z^n) sums (\<i> * sin z)"
using sin_converges sums_mult by blast
then show ?thesis
by (simp add: scaleR_conv_of_real field_simps)
qed
-theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)"
+theorem exp_Euler: "exp(\<i> * z) = cos(z) + \<i> * sin(z)"
proof -
- have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n)
- = (\<lambda>n. (ii * z) ^ n /\<^sub>R (fact n))"
+ have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n)
+ = (\<lambda>n. (\<i> * z) ^ n /\<^sub>R (fact n))"
proof
fix n
- show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)"
+ show "(cos_coeff n + \<i> * sin_coeff n) * z^n = (\<i> * z) ^ n /\<^sub>R (fact n)"
by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
qed
- also have "... sums (exp (ii * z))"
+ also have "... sums (exp (\<i> * z))"
by (rule exp_converges)
- finally have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" .
- moreover have "(\<lambda>n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)"
+ finally have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (exp (\<i> * z))" .
+ moreover have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (cos z + \<i> * sin z)"
using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
by (simp add: field_simps scaleR_conv_of_real)
ultimately show ?thesis
using sums_unique2 by blast
qed
-corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)"
+corollary exp_minus_Euler: "exp(-(\<i> * z)) = cos(z) - \<i> * sin(z)"
using exp_Euler [of "-z"]
by simp
-lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)"
+lemma sin_exp_eq: "sin z = (exp(\<i> * z) - exp(-(\<i> * z))) / (2*\<i>)"
by (simp add: exp_Euler exp_minus_Euler)
-lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2"
+lemma sin_exp_eq': "sin z = \<i> * (exp(-(\<i> * z)) - exp(\<i> * z)) / 2"
by (simp add: exp_Euler exp_minus_Euler)
-lemma cos_exp_eq: "cos z = (exp(ii * z) + exp(-(ii * z))) / 2"
+lemma cos_exp_eq: "cos z = (exp(\<i> * z) + exp(-(\<i> * z))) / 2"
by (simp add: exp_Euler exp_minus_Euler)
subsection\<open>Relationships between real and complex trig functions\<close>
@@ -127,7 +127,7 @@
shows "Re(cos(of_real x)) = cos x"
by (simp add: cos_of_real)
-lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)"
+lemma DeMoivre: "(cos z + \<i> * sin z) ^ n = cos(n * z) + \<i> * sin(n * z)"
apply (simp add: exp_Euler [symmetric])
by (metis exp_of_nat_mult mult.left_commute)
@@ -174,7 +174,7 @@
subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
lemma Euler: "exp(z) = of_real(exp(Re z)) *
- (of_real(cos(Im z)) + ii * of_real(sin(Im z)))"
+ (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
@@ -209,7 +209,7 @@
apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1))
by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 sin_zero_iff_int2)
-lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * ii)"
+lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * \<i>)"
(is "?lhs = ?rhs")
proof -
have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
@@ -226,9 +226,9 @@
lemma exp_integer_2pi:
assumes "n \<in> \<int>"
- shows "exp((2 * n * pi) * ii) = 1"
+ shows "exp((2 * n * pi) * \<i>) = 1"
proof -
- have "exp((2 * n * pi) * ii) = exp 0"
+ have "exp((2 * n * pi) * \<i>) = exp 0"
using assms
by (simp only: Ints_def exp_eq) auto
also have "... = 1"
@@ -377,7 +377,7 @@
finally show ?thesis .
qed
-lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
+lemma dist_exp_ii_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
using cos_double_sin [of "t/2"]
apply (simp add: real_sqrt_mult)
@@ -385,27 +385,27 @@
lemma sinh_complex:
fixes z :: complex
- shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)"
+ shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
lemma sin_ii_times:
fixes z :: complex
- shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)"
+ shows "sin(\<i> * z) = \<i> * ((exp z - inverse (exp z)) / 2)"
using sinh_complex by auto
lemma sinh_real:
fixes x :: real
- shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)"
+ shows "of_real((exp x - inverse (exp x)) / 2) = -\<i> * sin(\<i> * of_real x)"
by (simp add: exp_of_real sin_ii_times of_real_numeral)
lemma cosh_complex:
fixes z :: complex
- shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)"
+ shows "(exp z + inverse (exp z)) / 2 = cos(\<i> * z)"
by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
lemma cosh_real:
fixes x :: real
- shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)"
+ shows "of_real((exp x + inverse (exp x)) / 2) = cos(\<i> * of_real x)"
by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
lemmas cos_ii_times = cosh_complex [symmetric]
@@ -614,14 +614,14 @@
definition Arg :: "complex \<Rightarrow> real" where
"Arg z \<equiv> if z = 0 then 0
else THE t. 0 \<le> t \<and> t < 2*pi \<and>
- z = of_real(norm z) * exp(ii * of_real t)"
+ z = of_real(norm z) * exp(\<i> * of_real t)"
lemma Arg_0 [simp]: "Arg(0) = 0"
by (simp add: Arg_def)
lemma Arg_unique_lemma:
- assumes z: "z = of_real(norm z) * exp(ii * of_real t)"
- and z': "z = of_real(norm z) * exp(ii * of_real t')"
+ assumes z: "z = of_real(norm z) * exp(\<i> * of_real t)"
+ and z': "z = of_real(norm z) * exp(\<i> * of_real t')"
and t: "0 \<le> t" "t < 2*pi"
and t': "0 \<le> t'" "t' < 2*pi"
and nz: "z \<noteq> 0"
@@ -647,7 +647,7 @@
by (simp add: n)
qed
-lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))"
+lemma Arg: "0 \<le> Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
proof (cases "z=0")
case True then show ?thesis
by (simp add: Arg_def)
@@ -657,7 +657,7 @@
and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t"
using sincos_total_2pi [OF complex_unit_circle [OF False]]
by blast
- have z: "z = of_real(norm z) * exp(ii * of_real t)"
+ have z: "z = of_real(norm z) * exp(\<i> * of_real t)"
apply (rule complex_eqI)
using t False ReIm
apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps)
@@ -673,13 +673,13 @@
corollary
shows Arg_ge_0: "0 \<le> Arg z"
and Arg_lt_2pi: "Arg z < 2*pi"
- and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))"
+ and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
using Arg by auto
-lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(ii * of_real t))"
+lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(\<i> * of_real t))"
using Arg [of z] by auto
-lemma Arg_unique: "\<lbrakk>of_real r * exp(ii * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
+lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
apply (rule Arg_unique_lemma [OF _ Arg_eq])
using Arg [of z]
apply (auto simp: norm_mult)
@@ -1012,13 +1012,13 @@
text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
definition unwinding :: "complex \<Rightarrow> complex" where
- "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)"
-
-lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)"
+ "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
+
+lemma unwinding_2pi: "(2*pi) * \<i> * unwinding(z) = z - Ln(exp z)"
by (simp add: unwinding_def)
lemma Ln_times_unwinding:
- "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)"
+ "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \<i> * unwinding(Ln w + Ln z)"
using unwinding_2pi by (simp add: exp_add)
@@ -1192,22 +1192,22 @@
apply (metis Im_Ln_less_pi Im_Ln_le_pi add.commute add_mono_thms_linordered_field(3) inverse_nonzero_iff_nonzero mult_2)
done
-lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
+lemma Ln_minus1 [simp]: "Ln(-1) = \<i> * pi"
apply (rule exp_complex_eqI)
using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
apply (auto simp: abs_if)
done
-lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2"
- using Ln_exp [of "ii * (of_real pi/2)"]
+lemma Ln_ii [simp]: "Ln \<i> = \<i> * of_real pi/2"
+ using Ln_exp [of "\<i> * (of_real pi/2)"]
unfolding exp_Euler
by simp
-lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
+lemma Ln_minus_ii [simp]: "Ln(-\<i>) = - (\<i> * pi/2)"
proof -
- have "Ln(-ii) = Ln(inverse ii)" by simp
- also have "... = - (Ln ii)" using Ln_inverse by blast
- also have "... = - (ii * pi/2)" by simp
+ have "Ln(-\<i>) = Ln(inverse \<i>)" by simp
+ also have "... = - (Ln \<i>)" using Ln_inverse by blast
+ also have "... = - (\<i> * pi/2)" by simp
finally show ?thesis .
qed
@@ -1215,9 +1215,9 @@
assumes "w \<noteq> 0" "z \<noteq> 0"
shows "Ln(w * z) =
(if Im(Ln w + Ln z) \<le> -pi then
- (Ln(w) + Ln(z)) + ii * of_real(2*pi)
+ (Ln(w) + Ln(z)) + \<i> * of_real(2*pi)
else if Im(Ln w + Ln z) > pi then
- (Ln(w) + Ln(z)) - ii * of_real(2*pi)
+ (Ln(w) + Ln(z)) - \<i> * of_real(2*pi)
else Ln(w) + Ln(z))"
using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
@@ -1242,8 +1242,8 @@
lemma Ln_minus:
assumes "z \<noteq> 0"
shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
- then Ln(z) + ii * pi
- else Ln(z) - ii * pi)" (is "_ = ?rhs")
+ then Ln(z) + \<i> * pi
+ else Ln(z) - \<i> * pi)" (is "_ = ?rhs")
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
by (fastforce simp: exp_add exp_diff exp_Euler intro!: Ln_unique)
@@ -1280,9 +1280,9 @@
lemma Ln_times_ii:
assumes "z \<noteq> 0"
- shows "Ln(ii * z) = (if 0 \<le> Re(z) | Im(z) < 0
- then Ln(z) + ii * of_real pi/2
- else Ln(z) - ii * of_real(3 * pi/2))"
+ shows "Ln(\<i> * z) = (if 0 \<le> Re(z) | Im(z) < 0
+ then Ln(z) + \<i> * of_real pi/2
+ else Ln(z) - \<i> * of_real(3 * pi/2))"
using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
by (auto simp: Ln_times)
@@ -1313,7 +1313,7 @@
by simp
next
case False
- then have "z / of_real(norm z) = exp(ii * of_real(Arg z))"
+ then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
using Arg [of z]
by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Tue Aug 02 21:30:30 2016 +0200
@@ -42,7 +42,7 @@
have der_dif: "(deriv ^^ n) (\<lambda>w. f w - y) z = (deriv ^^ n) f z"
using \<open>0 < r\<close> \<open>0 < n\<close>
by (auto simp: higher_deriv_diff [OF holf holomorphic_on_const])
- have "norm ((2 * of_real pi * ii)/(fact n) * (deriv ^^ n) (\<lambda>w. f w - y) z)
+ have "norm ((2 * of_real pi * \<i>)/(fact n) * (deriv ^^ n) (\<lambda>w. f w - y) z)
\<le> (B0/r^(Suc n)) * (2 * pi * r)"
apply (rule has_contour_integral_bound_circlepath [of "(\<lambda>u. (f u - y)/(u - z)^(Suc n))" _ z])
using Cauchy_has_contour_integral_higher_derivative_circlepath [OF contf' holf']
@@ -70,7 +70,7 @@
(circlepath \<xi> r)"
apply (rule Cauchy_has_contour_integral_higher_derivative_circlepath [OF contf holf])
using \<open>0 < r\<close> by simp
- then have "norm ((2 * pi * ii)/(fact n) * (deriv ^^ n) f \<xi>) \<le> (B / r^(Suc n)) * (2 * pi * r)"
+ then have "norm ((2 * pi * \<i>)/(fact n) * (deriv ^^ n) f \<xi>) \<le> (B / r^(Suc n)) * (2 * pi * r)"
apply (rule has_contour_integral_bound_circlepath)
using \<open>0 \<le> B\<close> \<open>0 < r\<close>
apply (simp_all add: norm_divide norm_power nof frac_le norm_minus_commute del: power_Suc)
@@ -1229,13 +1229,13 @@
done
then obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<subseteq> U"
using \<open>open U\<close> open_contains_cball by blast
- then have "\<epsilon> * exp(2 * of_real pi * ii * (0/n)) \<in> cball 0 \<epsilon>"
- "\<epsilon> * exp(2 * of_real pi * ii * (1/n)) \<in> cball 0 \<epsilon>"
+ then have "\<epsilon> * exp(2 * of_real pi * \<i> * (0/n)) \<in> cball 0 \<epsilon>"
+ "\<epsilon> * exp(2 * of_real pi * \<i> * (1/n)) \<in> cball 0 \<epsilon>"
by (auto simp: norm_mult)
- with \<epsilon> have "\<epsilon> * exp(2 * of_real pi * ii * (0/n)) \<in> U"
- "\<epsilon> * exp(2 * of_real pi * ii * (1/n)) \<in> U" by blast+
- then obtain y0 y1 where "y0 \<in> T" and y0: "(y0 - \<xi>) * g y0 = \<epsilon> * exp(2 * of_real pi * ii * (0/n))"
- and "y1 \<in> T" and y1: "(y1 - \<xi>) * g y1 = \<epsilon> * exp(2 * of_real pi * ii * (1/n))"
+ with \<epsilon> have "\<epsilon> * exp(2 * of_real pi * \<i> * (0/n)) \<in> U"
+ "\<epsilon> * exp(2 * of_real pi * \<i> * (1/n)) \<in> U" by blast+
+ then obtain y0 y1 where "y0 \<in> T" and y0: "(y0 - \<xi>) * g y0 = \<epsilon> * exp(2 * of_real pi * \<i> * (0/n))"
+ and "y1 \<in> T" and y1: "(y1 - \<xi>) * g y1 = \<epsilon> * exp(2 * of_real pi * \<i> * (1/n))"
by (auto simp: U_def)
then have "y0 \<in> ball \<xi> \<delta>" "y1 \<in> ball \<xi> \<delta>" using Tsb by auto
moreover have "y0 \<noteq> y1"
@@ -1720,7 +1720,7 @@
then have 3: "continuous_on S (\<lambda>z. if 0 \<le> Im z then f z else cnj (f (cnj z)))"
by force
show ?thesis
- apply (rule holomorphic_on_paste_across_line [OF \<open>open S\<close>, of "-ii" _ 0])
+ apply (rule holomorphic_on_paste_across_line [OF \<open>open S\<close>, of "- \<i>" _ 0])
using 1 2 3
apply auto
done
@@ -2141,7 +2141,7 @@
definition residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
"residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
- \<longrightarrow> (f has_contour_integral 2*pi* ii *int) (circlepath z \<epsilon>))"
+ \<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"
lemma contour_integral_circlepath_eq:
assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2"
@@ -2253,11 +2253,11 @@
lemma base_residue:
assumes "open s" "z\<in>s" "r>0" and f_holo:"f holomorphic_on (s - {z})"
and r_cball:"cball z r \<subseteq> s"
- shows "(f has_contour_integral 2*pi*ii* (residue f z)) (circlepath z r)"
+ shows "(f has_contour_integral 2 * pi * \<i> * (residue f z)) (circlepath z r)"
proof -
obtain e where "e>0" and e_cball:"cball z e \<subseteq> s"
using open_contains_cball[of s] \<open>open s\<close> \<open>z\<in>s\<close> by auto
- define c where "c \<equiv> 2*pi*ii"
+ define c where "c \<equiv> 2 * pi * \<i>"
define i where "i \<equiv> contour_integral (circlepath z e) f / c"
have "(f has_contour_integral c*i) (circlepath z \<epsilon>)" when "\<epsilon>>0" "\<epsilon><e" for \<epsilon>
proof -
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 02 21:30:30 2016 +0200
@@ -167,8 +167,7 @@
instantiation complex :: euclidean_space
begin
-definition Basis_complex_def:
- "Basis = {1, ii}"
+definition Basis_complex_def: "Basis = {1, \<i>}"
instance
by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)
--- a/src/HOL/Nonstandard_Analysis/NSComplex.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy Tue Aug 02 21:30:30 2016 +0200
@@ -35,7 +35,7 @@
definition
iii :: hcomplex where
- "iii = star_of ii"
+ "iii = star_of \<i>"
(*------- complex conjugate ------*)
@@ -602,7 +602,7 @@
subsection\<open>@{term hcomplex_of_complex}: the Injection from
type @{typ complex} to to @{typ hcomplex}\<close>
-lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
+lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex \<i>"
by (rule iii_def)
lemma hRe_hcomplex_of_complex:
--- a/src/HOL/Probability/Characteristic_Functions.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy Tue Aug 02 21:30:30 2016 +0200
@@ -48,8 +48,8 @@
lemma interval_integral_iexp:
fixes a b :: real
- shows "(CLBINT x=a..b. iexp x) = ii * iexp a - ii * iexp b"
- by (subst interval_integral_FTC_finite [where F = "\<lambda>x. -ii * iexp x"])
+ shows "(CLBINT x=a..b. iexp x) = \<i> * iexp a - \<i> * iexp b"
+ by (subst interval_integral_FTC_finite [where F = "\<lambda>x. -\<i> * iexp x"])
(auto intro!: derivative_eq_intros continuous_intros)
subsection \<open>The Characteristic Function of a Real Measure.\<close>
@@ -64,7 +64,7 @@
lemma (in prob_space) integrable_iexp:
assumes f: "f \<in> borel_measurable M" "\<And>x. Im (f x) = 0"
- shows "integrable M (\<lambda>x. exp (ii * (f x)))"
+ shows "integrable M (\<lambda>x. exp (\<i> * (f x)))"
proof (intro integrable_const_bound [of _ 1])
from f have "\<And>x. of_real (Re (f x)) = f x"
by (simp add: complex_eq_iff)
@@ -133,18 +133,18 @@
fixes x :: real and n :: nat
defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
shows "(CLBINT s=0..x. f s n * iexp s) =
- x^Suc n / Suc n + (ii / Suc n) * (CLBINT s=0..x. f s (Suc n) * iexp s)"
+ x^Suc n / Suc n + (\<i> / Suc n) * (CLBINT s=0..x. f s (Suc n) * iexp s)"
proof -
have 1:
"((\<lambda>s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s)
- has_vector_derivative complex_of_real((x - s)^n) * iexp s + (ii * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n))))
+ has_vector_derivative complex_of_real((x - s)^n) * iexp s + (\<i> * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n))))
(at s within A)" for s A
by (intro derivative_eq_intros) auto
let ?F = "\<lambda>s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s"
- have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS")
+ have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (\<i> * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS")
proof -
- have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) *
+ have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (\<i> * iexp s) *
complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))))"
by (cases "0 \<le> x") (auto intro!: simp: f_def[abs_def])
also have "... = ?F x - ?F 0"
@@ -165,7 +165,7 @@
fixes x :: real
defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
shows "iexp x =
- (\<Sum>k \<le> n. (ii * x)^k / (fact k)) + ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (f s n) * (iexp s))" (is "?P n")
+ (\<Sum>k \<le> n. (\<i> * x)^k / (fact k)) + ((\<i> ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (f s n) * (iexp s))" (is "?P n")
proof (induction n)
show "?P 0"
by (auto simp add: field_simps interval_integral_iexp f_def zero_ereal_def)
@@ -184,7 +184,7 @@
lemma iexp_eq2:
fixes x :: real
defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
- shows "iexp x = (\<Sum>k\<le>Suc n. (ii*x)^k/fact k) + ii^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))"
+ shows "iexp x = (\<Sum>k\<le>Suc n. (\<i>*x)^k/fact k) + \<i>^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))"
proof -
have isCont_f: "isCont (\<lambda>s. f s n) x" for n x
by (auto simp: f_def)
@@ -204,7 +204,7 @@
(auto intro!: derivative_eq_intros simp del: power_Suc simp add: add_nonneg_eq_0_iff)
qed (auto intro: continuous_at_imp_continuous_on isCont_f)
- have calc3: "ii ^ (Suc (Suc n)) / (fact (Suc n)) = (ii ^ (Suc n) / (fact n)) * (ii / (Suc n))"
+ have calc3: "\<i> ^ (Suc (Suc n)) / (fact (Suc n)) = (\<i> ^ (Suc n) / (fact n)) * (\<i> / (Suc n))"
by (simp add: field_simps)
show ?thesis
@@ -246,10 +246,10 @@
finally show ?thesis .
qed
-lemma iexp_approx1: "cmod (iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k)) \<le> \<bar>x\<bar>^(Suc n) / fact (Suc n)"
+lemma iexp_approx1: "cmod (iexp x - (\<Sum>k \<le> n. (\<i> * x)^k / fact k)) \<le> \<bar>x\<bar>^(Suc n) / fact (Suc n)"
proof -
- have "iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k) =
- ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s))" (is "?t1 = ?t2")
+ have "iexp x - (\<Sum>k \<le> n. (\<i> * x)^k / fact k) =
+ ((\<i> ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s))" (is "?t1 = ?t2")
by (subst iexp_eq1 [of _ n], simp add: field_simps)
then have "cmod (?t1) = cmod (?t2)"
by simp
@@ -268,7 +268,7 @@
finally show ?thesis .
qed
-lemma iexp_approx2: "cmod (iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k)) \<le> 2 * \<bar>x\<bar>^n / fact n"
+lemma iexp_approx2: "cmod (iexp x - (\<Sum>k \<le> n. (\<i> * x)^k / fact k)) \<le> 2 * \<bar>x\<bar>^n / fact n"
proof (induction n) \<comment> \<open>really cases\<close>
case (Suc n)
have *: "\<And>a b. interval_lebesgue_integrable lborel a b f \<Longrightarrow> interval_lebesgue_integrable lborel a b g \<Longrightarrow>
@@ -277,8 +277,8 @@
using order_trans[OF f g] f g unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def
by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono)
- have "iexp x - (\<Sum>k \<le> Suc n. (ii * x)^k / fact k) =
- ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" (is "?t1 = ?t2")
+ have "iexp x - (\<Sum>k \<le> Suc n. (\<i> * x)^k / fact k) =
+ ((\<i> ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" (is "?t1 = ?t2")
unfolding iexp_eq2 [of x n] by (simp add: field_simps)
then have "cmod (?t1) = cmod (?t2)"
by simp
@@ -301,13 +301,13 @@
lemma (in real_distribution) char_approx1:
assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x^k)"
- shows "cmod (char M t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
+ shows "cmod (char M t - (\<Sum>k \<le> n. ((\<i> * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
(2*\<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>x\<bar>^n)" (is "cmod (char M t - ?t1) \<le> _")
proof -
have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
by (intro integrable_const_bound) auto
- define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
+ define c where [abs_def]: "c k x = (\<i> * t)^k / fact k * complex_of_real (x^k)" for k x
have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
@@ -335,14 +335,14 @@
lemma (in real_distribution) char_approx2:
assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x ^ k)"
- shows "cmod (char M t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
+ shows "cmod (char M t - (\<Sum>k \<le> n. ((\<i> * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
(\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
(is "cmod (char M t - ?t1) \<le> _")
proof -
have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
by (intro integrable_const_bound) auto
- define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
+ define c where [abs_def]: "c k x = (\<i> * t)^k / fact k * complex_of_real (x^k)" for k x
have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
@@ -445,7 +445,7 @@
assumes integrable_moments : "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. X x ^ k)"
and rv_X[measurable]: "random_variable borel X"
and \<mu>_distr : "distr M borel X = \<mu>"
- shows "cmod (char \<mu> t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. (X x)^k))) \<le>
+ shows "cmod (char \<mu> t - (\<Sum>k \<le> n. ((\<i> * t)^k / fact k) * expectation (\<lambda>x. (X x)^k))) \<le>
(2 * \<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>X x\<bar>^n)"
unfolding \<mu>_distr[symmetric]
apply (subst (1 2) integral_distr [symmetric, OF rv_X], simp, simp)
@@ -495,7 +495,7 @@
"char std_normal_distribution = (\<lambda>t. complex_of_real (exp (- (t^2) / 2)))"
proof (intro ext LIMSEQ_unique)
fix t :: real
- let ?f' = "\<lambda>k. (ii * t)^k / fact k * (LINT x | std_normal_distribution. x^k)"
+ let ?f' = "\<lambda>k. (\<i> * t)^k / fact k * (LINT x | std_normal_distribution. x^k)"
let ?f = "\<lambda>n. (\<Sum>k \<le> n. ?f' k)"
show "?f \<longlonglongrightarrow> exp (-(t^2) / 2)"
proof (rule limseq_even_odd)
--- a/src/HOL/Probability/Levy.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/Probability/Levy.thy Tue Aug 02 21:30:30 2016 +0200
@@ -19,21 +19,21 @@
lemma Levy_Inversion_aux1:
fixes a b :: real
assumes "a \<le> b"
- shows "((\<lambda>t. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t)) \<longlongrightarrow> b - a) (at 0)"
+ shows "((\<lambda>t. (iexp (-(t * a)) - iexp (-(t * b))) / (\<i> * t)) \<longlongrightarrow> b - a) (at 0)"
(is "(?F \<longlongrightarrow> _) (at _)")
proof -
have 1: "cmod (?F t - (b - a)) \<le> a^2 / 2 * abs t + b^2 / 2 * abs t" if "t \<noteq> 0" for t
proof -
have "cmod (?F t - (b - a)) = cmod (
- (iexp (-(t * a)) - (1 + ii * -(t * a))) / (ii * t) -
- (iexp (-(t * b)) - (1 + ii * -(t * b))) / (ii * t))"
- (is "_ = cmod (?one / (ii * t) - ?two / (ii * t))")
+ (iexp (-(t * a)) - (1 + \<i> * -(t * a))) / (\<i> * t) -
+ (iexp (-(t * b)) - (1 + \<i> * -(t * b))) / (\<i> * t))"
+ (is "_ = cmod (?one / (\<i> * t) - ?two / (\<i> * t))")
using \<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps)
- also have "\<dots> \<le> cmod (?one / (ii * t)) + cmod (?two / (ii * t))"
+ also have "\<dots> \<le> cmod (?one / (\<i> * t)) + cmod (?two / (\<i> * t))"
by (rule norm_triangle_ineq4)
- also have "cmod (?one / (ii * t)) = cmod ?one / abs t"
+ also have "cmod (?one / (\<i> * t)) = cmod ?one / abs t"
by (simp add: norm_divide norm_mult)
- also have "cmod (?two / (ii * t)) = cmod ?two / abs t"
+ also have "cmod (?two / (\<i> * t)) = cmod ?two / abs t"
by (simp add: norm_divide norm_mult)
also have "cmod ?one / abs t + cmod ?two / abs t \<le>
((- (a * t))^2 / 2) / abs t + ((- (b * t))^2 / 2) / abs t"
@@ -60,9 +60,9 @@
lemma Levy_Inversion_aux2:
fixes a b t :: real
assumes "a \<le> b" and "t \<noteq> 0"
- shows "cmod ((iexp (t * b) - iexp (t * a)) / (ii * t)) \<le> b - a" (is "?F \<le> _")
+ shows "cmod ((iexp (t * b) - iexp (t * a)) / (\<i> * t)) \<le> b - a" (is "?F \<le> _")
proof -
- have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (ii * t))"
+ have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (\<i> * t))"
using \<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus)
also have "\<dots> = cmod (iexp (t * (b - a)) - 1) / abs t"
unfolding norm_divide norm_mult norm_exp_ii_times using \<open>t \<noteq> 0\<close>
@@ -81,14 +81,14 @@
assumes "a \<le> b"
defines "\<mu> \<equiv> measure M" and "\<phi> \<equiv> char M"
assumes "\<mu> {a} = 0" and "\<mu> {b} = 0"
- shows "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t) * \<phi> t))
+ shows "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (\<i> * t) * \<phi> t))
\<longlonglongrightarrow> \<mu> {a<..b}"
(is "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. ?F t * \<phi> t)) \<longlonglongrightarrow> of_real (\<mu> {a<..b})")
proof -
interpret P: pair_sigma_finite lborel M ..
from bounded_Si obtain B where Bprop: "\<And>T. abs (Si T) \<le> B" by auto
from Bprop [of 0] have [simp]: "B \<ge> 0" by auto
- let ?f = "\<lambda>t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (ii * t)"
+ let ?f = "\<lambda>t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (\<i> * t)"
{ fix T :: real
assume "T \<ge> 0"
let ?f' = "\<lambda>(t, x). indicator {-T<..<T} t *\<^sub>R ?f t x"
@@ -110,7 +110,7 @@
using 1
by (intro interval_lebesgue_integral_add(2) [symmetric] interval_integrable_mirror[THEN iffD2]) simp_all
also have "\<dots> = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) -
- (iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (ii * t))"
+ (iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (\<i> * t))"
using \<open>T \<ge> 0\<close> by (intro interval_integral_cong) (auto simp add: divide_simps)
also have "\<dots> = (CLBINT t=(0::real)..T. complex_of_real(
2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))"
--- a/src/HOL/ex/BinEx.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/ex/BinEx.thy Tue Aug 02 21:30:30 2016 +0200
@@ -750,22 +750,22 @@
subsection\<open>Complex Arithmetic\<close>
-lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
+lemma "(1359 + 93746*\<i>) - (2468 + 46375*\<i>) = -1109 + 47371*\<i>"
by simp
-lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
+lemma "- (65745 + -47371*\<i>) = -65745 + 47371*\<i>"
by simp
text\<open>Multiplication requires distributive laws. Perhaps versions instantiated
to literal constants should be added to the simpset.\<close>
-lemma "(1 + ii) * (1 - ii) = 2"
+lemma "(1 + \<i>) * (1 - \<i>) = 2"
by (simp add: ring_distribs)
-lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
+lemma "(1 + 2*\<i>) * (1 + 3*\<i>) = -5 + 5*\<i>"
by (simp add: ring_distribs)
-lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
+lemma "(-84 + 255*\<i>) + (51 * 255*\<i>) = -84 + 13260 * \<i>"
by (simp add: ring_distribs)
text\<open>No inequalities or linear arithmetic: the complex numbers are unordered!\<close>
--- a/src/HOL/ex/Cubic_Quartic.thy Tue Aug 02 21:05:34 2016 +0200
+++ b/src/HOL/ex/Cubic_Quartic.thy Tue Aug 02 21:30:30 2016 +0200
@@ -93,8 +93,8 @@
q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3);
s = csqrt(q^2 + p^3);
s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s));
- s2 = -s1 * (1 + ii * csqrt 3) / 2;
- s3 = -s1 * (1 - ii * csqrt 3) / 2
+ s2 = -s1 * (1 + \<i> * csqrt 3) / 2;
+ s3 = -s1 * (1 - \<i> * csqrt 3) / 2
in
if p = 0 then
a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow>
@@ -112,8 +112,8 @@
let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
let ?s = "csqrt (?q^2 + ?p^3)"
let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)"
- let ?s2 = "- ?s1 * (1 + ii * csqrt 3) / 2"
- let ?s3 = "- ?s1 * (1 - ii * csqrt 3) / 2"
+ let ?s2 = "- ?s1 * (1 + \<i> * csqrt 3) / 2"
+ let ?s3 = "- ?s1 * (1 - \<i> * csqrt 3) / 2"
let ?y = "x + b / (3 * a)"
from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a * 3) \<noteq> 0"
by auto
@@ -122,9 +122,9 @@
have "csqrt 3^2 = 3" by (rule power2_csqrt)
then have th0:
"?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and>
- ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \<and>
- ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and>
- ii^2 + 1 = 0 \<and> csqrt 3^2 = 3"
+ ?s2 = - ?s1 * (1 + \<i> * csqrt 3) / 2 \<and>
+ ?s3 = - ?s1 * (1 - \<i> * csqrt 3) / 2 \<and>
+ \<i>^2 + 1 = 0 \<and> csqrt 3^2 = 3"
using zero by (simp add: field_simps ccbrt)
from cubic_basic[OF th0, of ?y]
show ?thesis