Commit 2023-05-16 00:41 4816740a

View on Github →

feat: port Analysis.SpecialFunctions.Exp (#3988)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Exp.lean

added theorem Complex.comap_exp_comap_abs_atTop

added theorem Complex.comap_exp_nhdsWithin_zero

added theorem Complex.comap_exp_nhds_zero

added theorem Complex.continuousOn_exp

added theorem Complex.continuous_exp

added theorem Complex.exp_bound_sq

added theorem Complex.locally_lipschitz_exp

added theorem Complex.tendsto_exp_comap_re_atBot

added theorem Complex.tendsto_exp_comap_re_atBot_nhdsWithin

added theorem Complex.tendsto_exp_comap_re_atTop

added theorem Complex.tendsto_exp_nhds_zero_iff

added theorem Continuous.cexp

added theorem Continuous.exp

added theorem ContinuousAt.cexp

added theorem ContinuousAt.exp

added theorem ContinuousOn.cexp

added theorem ContinuousOn.exp

added theorem ContinuousWithinAt.cexp

added theorem ContinuousWithinAt.exp

added theorem Filter.Tendsto.cexp

added theorem Filter.Tendsto.exp

added theorem Real.coe_comp_expOrderIso

added theorem Real.coe_expOrderIso_apply

added theorem Real.comap_exp_atTop

added theorem Real.comap_exp_nhdsWithin_Ioi_zero

added theorem Real.comap_exp_nhds_zero

added theorem Real.continuousOn_exp

added theorem Real.continuous_exp

added def Real.expOrderIso

added theorem Real.exp_half

added theorem Real.isBigO_exp_comp_exp_comp

added theorem Real.isBigO_exp_comp_one

added theorem Real.isBigO_one_exp_comp

added theorem Real.isBoundedUnder_ge_exp_comp

added theorem Real.isBoundedUnder_le_exp_comp

added theorem Real.isLittleO_exp_comp_exp_comp

added theorem Real.isLittleO_one_exp_comp

added theorem Real.isLittleO_pow_exp_atTop

added theorem Real.isTheta_exp_comp_exp_comp

added theorem Real.isTheta_exp_comp_one

added theorem Real.map_exp_atBot

added theorem Real.map_exp_atTop

added theorem Real.range_exp

added theorem Real.tendsto_comp_exp_atBot

added theorem Real.tendsto_comp_exp_atTop

added theorem Real.tendsto_div_pow_mul_exp_add_atTop

added theorem Real.tendsto_exp_atBot

added theorem Real.tendsto_exp_atBot_nhdsWithin

added theorem Real.tendsto_exp_atTop

added theorem Real.tendsto_exp_comp_atTop

added theorem Real.tendsto_exp_comp_nhds_zero

added theorem Real.tendsto_exp_div_pow_atTop

added theorem Real.tendsto_exp_neg_atTop_nhds_0

added theorem Real.tendsto_exp_nhds_0_nhds_1

added theorem Real.tendsto_mul_exp_add_div_pow_atTop

added theorem Real.tendsto_pow_mul_exp_neg_atTop_nhds_0