Commit 2023-05-17 06:12 882c98b8

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.Basic (#4015)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

added theorem Complex.abs_exp_mul_exp_add_exp_neg_le_of_abs_im_le

added theorem Complex.continuousOn_cos

added theorem Complex.continuousOn_sin

added theorem Complex.continuous_cos

added theorem Complex.continuous_cosh

added theorem Complex.continuous_sin

added theorem Complex.continuous_sinh

added theorem Complex.cos_add_int_mul_two_pi

added theorem Complex.cos_add_nat_mul_two_pi

added theorem Complex.cos_add_pi

added theorem Complex.cos_add_pi_div_two

added theorem Complex.cos_add_two_pi

added theorem Complex.cos_antiperiodic

added theorem Complex.cos_int_mul_two_pi

added theorem Complex.cos_int_mul_two_pi_add_pi

added theorem Complex.cos_int_mul_two_pi_sub

added theorem Complex.cos_int_mul_two_pi_sub_pi

added theorem Complex.cos_nat_mul_two_pi

added theorem Complex.cos_nat_mul_two_pi_add_pi

added theorem Complex.cos_nat_mul_two_pi_sub

added theorem Complex.cos_nat_mul_two_pi_sub_pi

added theorem Complex.cos_periodic

added theorem Complex.cos_pi

added theorem Complex.cos_pi_div_two

added theorem Complex.cos_pi_div_two_sub

added theorem Complex.cos_pi_sub

added theorem Complex.cos_sub_int_mul_two_pi

added theorem Complex.cos_sub_nat_mul_two_pi

added theorem Complex.cos_sub_pi

added theorem Complex.cos_sub_pi_div_two

added theorem Complex.cos_sub_two_pi

added theorem Complex.cos_two_pi

added theorem Complex.cos_two_pi_sub

added theorem Complex.exp_add_pi_mul_I

added theorem Complex.exp_antiperiodic

added theorem Complex.exp_int_mul_two_pi_mul_I

added theorem Complex.exp_mul_I_antiperiodic

added theorem Complex.exp_mul_I_periodic

added theorem Complex.exp_nat_mul_two_pi_mul_I

added theorem Complex.exp_periodic

added theorem Complex.exp_pi_mul_I

added theorem Complex.exp_sub_pi_mul_I

added theorem Complex.exp_two_pi_mul_I

added theorem Complex.sin_add_int_mul_two_pi

added theorem Complex.sin_add_nat_mul_two_pi

added theorem Complex.sin_add_pi

added theorem Complex.sin_add_pi_div_two

added theorem Complex.sin_add_two_pi

added theorem Complex.sin_antiperiodic

added theorem Complex.sin_eq_zero_iff_cos_eq

added theorem Complex.sin_int_mul_pi

added theorem Complex.sin_int_mul_two_pi_sub

added theorem Complex.sin_nat_mul_pi

added theorem Complex.sin_nat_mul_two_pi_sub

added theorem Complex.sin_periodic

added theorem Complex.sin_pi

added theorem Complex.sin_pi_div_two

added theorem Complex.sin_pi_div_two_sub

added theorem Complex.sin_pi_sub

added theorem Complex.sin_sub_int_mul_two_pi

added theorem Complex.sin_sub_nat_mul_two_pi

added theorem Complex.sin_sub_pi

added theorem Complex.sin_sub_pi_div_two

added theorem Complex.sin_sub_two_pi

added theorem Complex.sin_two_pi

added theorem Complex.sin_two_pi_sub

added theorem Complex.tan_add_int_mul_pi

added theorem Complex.tan_add_nat_mul_pi

added theorem Complex.tan_add_pi

added theorem Complex.tan_int_mul_pi

added theorem Complex.tan_int_mul_pi_sub

added theorem Complex.tan_nat_mul_pi

added theorem Complex.tan_nat_mul_pi_sub

added theorem Complex.tan_periodic

added theorem Complex.tan_pi_div_two_sub

added theorem Complex.tan_pi_sub

added theorem Complex.tan_sub_int_mul_pi

added theorem Complex.tan_sub_nat_mul_pi

added theorem Complex.tan_sub_pi

added theorem NNReal.coe_real_pi

added theorem NNReal.pi_ne_zero

added theorem NNReal.pi_pos

added theorem Real.bijOn_cos

added theorem Real.bijOn_sin

added theorem Real.coe_sinOrderIso_apply

added theorem Real.continuousOn_cos

added theorem Real.continuousOn_sin

added theorem Real.continuous_cos

added theorem Real.continuous_cosh

added theorem Real.continuous_sin

added theorem Real.continuous_sinh

added theorem Real.cos_add_int_mul_two_pi

added theorem Real.cos_add_nat_mul_two_pi

added theorem Real.cos_add_pi

added theorem Real.cos_add_pi_div_two

added theorem Real.cos_add_two_pi

added theorem Real.cos_antiperiodic

added theorem Real.cos_eq_one_iff

added theorem Real.cos_eq_one_iff_of_lt_of_lt

added theorem Real.cos_eq_sqrt_one_sub_sin_sq

added theorem Real.cos_int_mul_two_pi

added theorem Real.cos_int_mul_two_pi_add_pi

added theorem Real.cos_int_mul_two_pi_sub

added theorem Real.cos_int_mul_two_pi_sub_pi

added theorem Real.cos_le_cos_of_nonneg_of_le_pi

added theorem Real.cos_lt_cos_of_nonneg_of_le_pi

added theorem Real.cos_lt_cos_of_nonneg_of_le_pi_div_two

added theorem Real.cos_mem_Icc

added theorem Real.cos_nat_mul_two_pi

added theorem Real.cos_nat_mul_two_pi_add_pi

added theorem Real.cos_nat_mul_two_pi_sub

added theorem Real.cos_nat_mul_two_pi_sub_pi

added theorem Real.cos_neg_of_pi_div_two_lt_of_lt

added theorem Real.cos_nonneg_of_mem_Icc

added theorem Real.cos_nonneg_of_neg_pi_div_two_le_of_le

added theorem Real.cos_nonpos_of_pi_div_two_le_of_le

added theorem Real.cos_periodic

added theorem Real.cos_pi

added theorem Real.cos_pi_div_eight

added theorem Real.cos_pi_div_four

added theorem Real.cos_pi_div_six

added theorem Real.cos_pi_div_sixteen

added theorem Real.cos_pi_div_thirty_two

added theorem Real.cos_pi_div_three

added theorem Real.cos_pi_div_two

added theorem Real.cos_pi_div_two_sub

added theorem Real.cos_pi_over_two_pow

added theorem Real.cos_pi_sub

added theorem Real.cos_pos_of_mem_Ioo

added theorem Real.cos_sub_int_mul_two_pi

added theorem Real.cos_sub_nat_mul_two_pi

added theorem Real.cos_sub_pi

added theorem Real.cos_sub_pi_div_two

added theorem Real.cos_sub_two_pi

added theorem Real.cos_two_pi

added theorem Real.cos_two_pi_sub

added theorem Real.exists_cos_eq_zero

added theorem Real.injOn_cos

added theorem Real.injOn_sin

added theorem Real.injOn_tan

added theorem Real.mapsTo_cos

added theorem Real.mapsTo_sin

added theorem Real.one_le_pi_div_two

added theorem Real.pi_div_two_le_two

added theorem Real.pi_div_two_pos

added theorem Real.pi_le_four

added theorem Real.pi_ne_zero

added theorem Real.pi_pos

added theorem Real.range_cos

added theorem Real.range_cos_infinite

added theorem Real.range_sin

added theorem Real.range_sin_infinite

added def Real.sinOrderIso

added theorem Real.sinOrderIso_apply

added theorem Real.sin_add_int_mul_two_pi

added theorem Real.sin_add_nat_mul_two_pi

added theorem Real.sin_add_pi

added theorem Real.sin_add_pi_div_two

added theorem Real.sin_add_two_pi

added theorem Real.sin_antiperiodic

added theorem Real.sin_eq_sqrt_one_sub_cos_sq

added theorem Real.sin_eq_zero_iff

added theorem Real.sin_eq_zero_iff_cos_eq

added theorem Real.sin_eq_zero_iff_of_lt_of_lt

added theorem Real.sin_int_mul_pi

added theorem Real.sin_int_mul_two_pi_sub

added theorem Real.sin_le_sin_of_le_of_le_pi_div_two

added theorem Real.sin_lt_sin_of_lt_of_le_pi_div_two

added theorem Real.sin_mem_Icc

added theorem Real.sin_nat_mul_pi

added theorem Real.sin_nat_mul_two_pi_sub

added theorem Real.sin_ne_zero_iff

added theorem Real.sin_neg_of_neg_of_neg_pi_lt

added theorem Real.sin_nonneg_of_mem_Icc

added theorem Real.sin_nonneg_of_nonneg_of_le_pi

added theorem Real.sin_nonpos_of_nonnpos_of_neg_pi_le

added theorem Real.sin_periodic

added theorem Real.sin_pi

added theorem Real.sin_pi_div_eight

added theorem Real.sin_pi_div_four

added theorem Real.sin_pi_div_six

added theorem Real.sin_pi_div_sixteen

added theorem Real.sin_pi_div_thirty_two

added theorem Real.sin_pi_div_three

added theorem Real.sin_pi_div_two

added theorem Real.sin_pi_div_two_sub

added theorem Real.sin_pi_over_two_pow_succ

added theorem Real.sin_pi_sub

added theorem Real.sin_pos_of_mem_Ioo

added theorem Real.sin_pos_of_pos_of_lt_pi

added theorem Real.sin_sq_pi_over_two_pow

added theorem Real.sin_sq_pi_over_two_pow_succ

added theorem Real.sin_sub_int_mul_two_pi

added theorem Real.sin_sub_nat_mul_two_pi

added theorem Real.sin_sub_pi

added theorem Real.sin_sub_pi_div_two

added theorem Real.sin_sub_two_pi

added theorem Real.sin_two_pi

added theorem Real.sin_two_pi_sub

added theorem Real.sq_cos_pi_div_six

added theorem Real.sq_sin_pi_div_three

added theorem Real.sqrtTwoAddSeries_lt_two

added theorem Real.sqrtTwoAddSeries_monotone_left

added theorem Real.sqrtTwoAddSeries_nonneg

added theorem Real.sqrtTwoAddSeries_one

added theorem Real.sqrtTwoAddSeries_succ

added theorem Real.sqrtTwoAddSeries_two

added theorem Real.sqrtTwoAddSeries_zero

added theorem Real.sqrtTwoAddSeries_zero_nonneg

added theorem Real.strictAntiOn_cos

added theorem Real.strictMonoOn_sin

added theorem Real.strictMonoOn_tan

added theorem Real.surjOn_cos

added theorem Real.surjOn_sin

added theorem Real.tan_add_int_mul_pi

added theorem Real.tan_add_nat_mul_pi

added theorem Real.tan_add_pi

added theorem Real.tan_inj_of_lt_of_lt_pi_div_two

added theorem Real.tan_int_mul_pi

added theorem Real.tan_int_mul_pi_sub

added theorem Real.tan_lt_tan_of_lt_of_lt_pi_div_two

added theorem Real.tan_lt_tan_of_nonneg_of_lt_pi_div_two

added theorem Real.tan_nat_mul_pi

added theorem Real.tan_nat_mul_pi_sub

added theorem Real.tan_neg_of_neg_of_pi_div_two_lt

added theorem Real.tan_nonneg_of_nonneg_of_le_pi_div_two

added theorem Real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le

added theorem Real.tan_periodic

added theorem Real.tan_pi_div_four

added theorem Real.tan_pi_div_two

added theorem Real.tan_pi_div_two_sub

added theorem Real.tan_pi_sub

added theorem Real.tan_pos_of_pos_of_lt_pi_div_two

added theorem Real.tan_sub_int_mul_pi

added theorem Real.tan_sub_nat_mul_pi

added theorem Real.tan_sub_pi

added theorem Real.tendsto_cos_neg_pi_div_two

added theorem Real.tendsto_cos_pi_div_two

added theorem Real.tendsto_sin_neg_pi_div_two

added theorem Real.tendsto_sin_pi_div_two

added theorem Real.tendsto_tan_neg_pi_div_two

added theorem Real.tendsto_tan_pi_div_two

added theorem Real.two_le_pi

added theorem Real.two_pi_pos

Modified Mathlib/Topology/Algebra/Group/Basic.lean