Commit 2023-06-05 02:03 2ac19d6f

View on Github →

feat: port Analysis.SpecialFunctions.CompareExp (#4412) I had to add several norm_cast to force coercion. My guess is that in Lean3 simp also tried norm_cast but here we need to invoke the tactic explicitly. There are two calc proofs that I'm having difficulty resolving, both because of type casting issues.

isLittleO_im_pow_exp_re
isLittleO_cpow_exp Please feel free to push to this branch.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/CompareExp.lean

added theorem Complex.IsExpCmpFilter.abs_im_pow_eventuallyLE_exp_re

added theorem Complex.IsExpCmpFilter.eventually_ne

added theorem Complex.IsExpCmpFilter.isLittleO_cpow_exp

added theorem Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp

added theorem Complex.IsExpCmpFilter.isLittleO_exp_cpow

added theorem Complex.IsExpCmpFilter.isLittleO_im_pow_exp_re

added theorem Complex.IsExpCmpFilter.isLittleO_log_abs_re

added theorem Complex.IsExpCmpFilter.isLittleO_log_re_re

added theorem Complex.IsExpCmpFilter.isLittleO_pow_mul_exp

added theorem Complex.IsExpCmpFilter.isLittleO_zpow_mul_exp

added theorem Complex.IsExpCmpFilter.of_boundedUnder_abs_im

added theorem Complex.IsExpCmpFilter.of_boundedUnder_im

added theorem Complex.IsExpCmpFilter.of_isBigO_im_re_pow

added theorem Complex.IsExpCmpFilter.of_isBigO_im_re_rpow

added theorem Complex.IsExpCmpFilter.tendsto_abs

added theorem Complex.IsExpCmpFilter.tendsto_abs_re

added structure Complex.IsExpCmpFilter