Commit 2023-03-15 16:55 48b89dbf

View on Github →

feat: port Data.Complex.Exponential (#2785)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Complex/Basic.lean

added theorem Complex.im_ofNat

added theorem Complex.re_ofNat

Created Mathlib/Data/Complex/Exponential.lean

added theorem Complex.abs_cos_add_sin_mul_I

added theorem Complex.abs_exp

added theorem Complex.abs_exp_eq_iff_re_eq

added theorem Complex.abs_exp_ofReal

added theorem Complex.abs_exp_ofReal_mul_I

added theorem Complex.abs_exp_sub_one_le

added theorem Complex.abs_exp_sub_one_sub_id_le

added def Complex.cos

added theorem Complex.cos_add

added theorem Complex.cos_add_cos

added theorem Complex.cos_add_mul_I

added theorem Complex.cos_add_sin_I

added theorem Complex.cos_add_sin_mul_I_pow

added theorem Complex.cos_conj

added theorem Complex.cos_eq

added theorem Complex.cos_mul_I

added theorem Complex.cos_neg

added theorem Complex.cos_ofReal_im

added theorem Complex.cos_ofReal_re

added theorem Complex.cos_sq'

added theorem Complex.cos_sq

added theorem Complex.cos_sq_add_sin_sq

added theorem Complex.cos_sub

added theorem Complex.cos_sub_cos

added theorem Complex.cos_sub_sin_I

added theorem Complex.cos_three_mul

added theorem Complex.cos_two_mul'

added theorem Complex.cos_two_mul

added theorem Complex.cos_zero

added def Complex.cosh

added theorem Complex.cosh_add

added theorem Complex.cosh_add_sinh

added theorem Complex.cosh_conj

added theorem Complex.cosh_mul_I

added theorem Complex.cosh_neg

added theorem Complex.cosh_ofReal_im

added theorem Complex.cosh_ofReal_re

added theorem Complex.cosh_sq

added theorem Complex.cosh_sq_sub_sinh_sq

added theorem Complex.cosh_sub

added theorem Complex.cosh_sub_sinh

added theorem Complex.cosh_three_mul

added theorem Complex.cosh_two_mul

added theorem Complex.cosh_zero

added def Complex.exp'

added def Complex.exp

added theorem Complex.exp_add

added theorem Complex.exp_add_mul_I

added theorem Complex.exp_bound'

added theorem Complex.exp_bound

added theorem Complex.exp_conj

added theorem Complex.exp_eq_exp_re_mul_sin_add_cos

added theorem Complex.exp_im

added theorem Complex.exp_int_mul

added theorem Complex.exp_list_sum

added theorem Complex.exp_mul_I

added theorem Complex.exp_multiset_sum

added theorem Complex.exp_nat_mul

added theorem Complex.exp_ne_zero

added theorem Complex.exp_neg

added theorem Complex.exp_ofReal_im

added theorem Complex.exp_ofReal_mul_I_im

added theorem Complex.exp_ofReal_mul_I_re

added theorem Complex.exp_ofReal_re

added theorem Complex.exp_re

added theorem Complex.exp_sub

added theorem Complex.exp_sub_cosh

added theorem Complex.exp_sub_sinh

added theorem Complex.exp_sum

added theorem Complex.exp_zero

added theorem Complex.inv_one_add_tan_sq

added theorem Complex.isCauSeq_abs_exp

added theorem Complex.isCauSeq_exp

added theorem Complex.ofReal_cos

added theorem Complex.ofReal_cos_ofReal_re

added theorem Complex.ofReal_cosh

added theorem Complex.ofReal_cosh_ofReal_re

added theorem Complex.ofReal_exp

added theorem Complex.ofReal_exp_ofReal_re

added theorem Complex.ofReal_sin

added theorem Complex.ofReal_sin_ofReal_re

added theorem Complex.ofReal_sinh

added theorem Complex.ofReal_sinh_ofReal_re

added theorem Complex.ofReal_tan

added theorem Complex.ofReal_tan_ofReal_re

added theorem Complex.ofReal_tanh

added theorem Complex.ofReal_tanh_ofReal_re

added def Complex.sin

added theorem Complex.sin_add

added theorem Complex.sin_add_mul_I

added theorem Complex.sin_conj

added theorem Complex.sin_eq

added theorem Complex.sin_mul_I

added theorem Complex.sin_neg

added theorem Complex.sin_ofReal_im

added theorem Complex.sin_ofReal_re

added theorem Complex.sin_sq

added theorem Complex.sin_sq_add_cos_sq

added theorem Complex.sin_sub

added theorem Complex.sin_sub_sin

added theorem Complex.sin_three_mul

added theorem Complex.sin_two_mul

added theorem Complex.sin_zero

added def Complex.sinh

added theorem Complex.sinh_add

added theorem Complex.sinh_add_cosh

added theorem Complex.sinh_conj

added theorem Complex.sinh_mul_I

added theorem Complex.sinh_neg

added theorem Complex.sinh_of_real_im

added theorem Complex.sinh_of_real_re

added theorem Complex.sinh_sq

added theorem Complex.sinh_sub

added theorem Complex.sinh_sub_cosh

added theorem Complex.sinh_three_mul

added theorem Complex.sinh_two_mul

added theorem Complex.sinh_zero

added theorem Complex.sum_div_factorial_le

added def Complex.tan

added theorem Complex.tan_conj

added theorem Complex.tan_eq_sin_div_cos

added theorem Complex.tan_mul_I

added theorem Complex.tan_mul_cos

added theorem Complex.tan_neg

added theorem Complex.tan_of_real_im

added theorem Complex.tan_of_real_re

added theorem Complex.tan_sq_div_one_add_tan_sq

added theorem Complex.tan_zero

added def Complex.tanh

added theorem Complex.tanh_conj

added theorem Complex.tanh_eq_sinh_div_cosh

added theorem Complex.tanh_mul_I

added theorem Complex.tanh_neg

added theorem Complex.tanh_ofReal_im

added theorem Complex.tanh_ofReal_re

added theorem Complex.tanh_zero

added theorem Complex.two_cos

added theorem Complex.two_cosh

added theorem Complex.two_sin

added theorem Complex.two_sinh

added theorem Real.abs_cos_eq_sqrt_one_sub_sin_sq

added theorem Real.abs_cos_le_one

added theorem Real.abs_exp

added theorem Real.abs_exp_sub_one_le

added theorem Real.abs_exp_sub_one_sub_id_le

added theorem Real.abs_sin_eq_sqrt_one_sub_cos_sq

added theorem Real.abs_sin_le_one

added theorem Real.add_one_le_exp

added theorem Real.add_one_le_exp_of_nonneg

added theorem Real.add_one_le_exp_of_nonpos

added theorem Real.cos_abs

added theorem Real.cos_bound

added theorem Real.cos_le_one

added theorem Real.cos_neg

added theorem Real.cos_one_le

added theorem Real.cos_one_pos

added theorem Real.cos_pos_of_le_one

added theorem Real.cos_sq'

added theorem Real.cos_sq_add_sin_sq

added theorem Real.cos_sq_le_one

added theorem Real.cos_sub

added theorem Real.cos_two_neg

added theorem Real.cos_zero

added theorem Real.cosh_abs

added theorem Real.cosh_add_sinh

added theorem Real.cosh_eq

added theorem Real.cosh_neg

added theorem Real.cosh_pos

added theorem Real.cosh_sq'

added theorem Real.cosh_sq_sub_sinh_sq

added theorem Real.cosh_sub

added theorem Real.cosh_sub_sinh

added theorem Real.cosh_zero

added theorem Real.expNear_sub

added theorem Real.expNear_succ

added theorem Real.expNear_zero

added theorem Real.exp_1_approx_succ_eq

added theorem Real.exp_approx_end'

added theorem Real.exp_approx_end

added theorem Real.exp_approx_start

added theorem Real.exp_approx_succ

added theorem Real.exp_bound'

added theorem Real.exp_bound_div_one_sub_of_interval

added theorem Real.exp_bound_div_one_sub_of_interval_approx

added theorem Real.exp_eq_exp

added theorem Real.exp_eq_one_iff

added theorem Real.exp_injective

added theorem Real.exp_le_exp

added theorem Real.exp_le_one_iff

added theorem Real.exp_list_sum

added theorem Real.exp_lt_exp

added theorem Real.exp_lt_one_iff

added theorem Real.exp_monotone

added theorem Real.exp_multiset_sum

added theorem Real.exp_pos

added theorem Real.exp_strictMono

added theorem Real.exp_sub

added theorem Real.exp_sub_cosh

added theorem Real.exp_sub_sinh

added theorem Real.exp_sum

added theorem Real.exp_zero

added theorem Real.inv_one_add_tan_sq

added theorem Real.inv_sqrt_one_add_tan_sq

added theorem Real.neg_one_le_cos

added theorem Real.neg_one_le_sin

added theorem Real.one_le_exp

added theorem Real.one_le_exp_iff

added theorem Real.one_lt_exp_iff

added theorem Real.one_sub_div_pow_le_exp_neg

added theorem Real.one_sub_le_exp_minus_of_pos

added theorem Real.sin_bound

added theorem Real.sin_le_one

added theorem Real.sin_neg

added theorem Real.sin_pos_of_pos_of_le_one

added theorem Real.sin_pos_of_pos_of_le_two

added theorem Real.sin_sq

added theorem Real.sin_sq_le_one

added theorem Real.sin_sub

added theorem Real.sin_zero

added theorem Real.sinh_add_cosh

added theorem Real.sinh_lt_cosh

added theorem Real.sinh_neg

added theorem Real.sinh_sub

added theorem Real.sinh_sub_cosh

added theorem Real.sinh_zero

added theorem Real.tan_div_sqrt_one_add_tan_sq

added theorem Real.tan_mul_cos

added theorem Real.tan_neg

added theorem Real.tan_sq_div_one_add_tan_sq

added theorem Real.tan_zero

added theorem Real.tanh_neg

added theorem Real.tanh_zero

added def Tactic.evalExp

added theorem abv_sum_le_sum_abv

added theorem cauchy_product

added theorem isCauSeq_geo_series

added theorem isCauSeq_geo_series_const

added theorem isCauSeq_of_decreasing_bounded

added theorem isCauSeq_of_mono_bounded

added theorem isCauSeq_series_of_abv_isCauSeq

added theorem isCauSeq_series_of_abv_le_of_isCauSeq

added theorem series_ratio_test

added theorem sum_range_diag_flip