Documentation Verification Report

CompareExp

📁 Source: Mathlib/Analysis/SpecialFunctions/CompareExp.lean

Statistics

Metric	Count
Definitions `IsExpCmpFilter`	1
Theorems `abs_im_pow_eventuallyLE_exp_re`, `eventually_ne`, `isBigO_im_pow_re`, `isLittleO_cpow_exp`, `isLittleO_cpow_mul_exp`, `isLittleO_exp_cpow`, `isLittleO_im_pow_exp_re`, `isLittleO_log_norm_re`, `isLittleO_log_re_re`, `isLittleO_pow_mul_exp`, `isLittleO_zpow_mul_exp`, `isTheta_cpow_exp_re_mul_log`, `of_boundedUnder_abs_im`, `of_boundedUnder_im`, `of_isBigO_im_re_pow`, `of_isBigO_im_re_rpow`, `tendsto_abs_re`, `tendsto_norm`, `tendsto_re`	19
Total	20

Complex

Definitions

Name	Category	Theorems
`IsExpCmpFilter` 📖	CompData	4 math math: `IsExpCmpFilter.of_boundedUnder_im`, `IsExpCmpFilter.of_isBigO_im_re_pow`, `IsExpCmpFilter.of_isBigO_im_re_rpow`, `IsExpCmpFilter.of_boundedUnder_abs_im`

Complex.IsExpCmpFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_im_pow_eventuallyLE_exp_re` 📖	mathematical	`Complex.IsExpCmpFilter`	`Filter.EventuallyLE` `Complex` `Real` `Real.instLE` `Monoid.toNatPow` `Real.instMonoid` `abs` `Real.lattice` `Real.instAddGroup` `Complex.im` `Real.exp` `Complex.re`	—	`norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Real.abs_exp` `one_mul` `Asymptotics.IsLittleO.bound` `isLittleO_im_pow_exp_re` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`eventually_ne` 📖	mathematical	`Complex.IsExpCmpFilter`	`Filter.Eventually` `Complex` `Complex.instZero`	—	`Filter.Tendsto.eventually_ne_atTop'` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `tendsto_re`
`isBigO_im_pow_re` 📖	mathematical	`Complex.IsExpCmpFilter`	`Asymptotics.IsBigO` `Complex` `Real` `Real.norm` `Monoid.toNatPow` `Real.instMonoid` `Complex.im` `Real.exp` `Complex.re`	—	—
`isLittleO_cpow_exp` 📖	mathematical	`Complex.IsExpCmpFilter` `Real` `Real.instLT` `Real.instZero`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Complex.instPow` `Complex.exp` `Complex.instMul` `Complex.ofReal`	—	`isTheta_cpow_exp_re_mul_log` `Asymptotics.IsLittleO.of_norm_right` `Complex.norm_exp` `Complex.re_ofReal_mul` `Asymptotics.IsEquivalent.tendsto_atTop` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Asymptotics.IsEquivalent.symm` `Asymptotics.IsEquivalent.sub_isLittleO` `Asymptotics.IsEquivalent.refl` `Asymptotics.IsLittleO.const_mul_right` `NormedDivisionRing.toNormMulClass` `LT.lt.ne'` `Asymptotics.IsLittleO.const_mul_left` `isLittleO_log_norm_re` `Filter.Tendsto.const_mul_atTop` `tendsto_re`
`isLittleO_cpow_mul_exp` 📖	mathematical	`Complex.IsExpCmpFilter` `Real` `Real.instLT`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Complex.instMul` `Complex.instPow` `Complex.exp` `Complex.ofReal`	—	`Filter.Eventually.mono` `eventually_ne` `mul_right_comm` `Complex.cpow_add` `add_sub_cancel` `Asymptotics.IsBigO.mul_isLittleO` `NormedDivisionRing.toNormMulClass` `Asymptotics.isBigO_refl` `isLittleO_cpow_exp` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Complex.ofReal_sub` `sub_mul` `mul_assoc` `Filter.EventuallyEq.refl`
`isLittleO_exp_cpow` 📖	mathematical	`Complex.IsExpCmpFilter` `Real` `Real.instLT` `Real.instZero`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Complex.exp` `Complex.instMul` `Complex.ofReal` `Complex.instPow`	—	`Complex.cpow_zero` `one_mul` `MulZeroClass.zero_mul` `Complex.exp_zero` `mul_one` `isLittleO_cpow_mul_exp`
`isLittleO_im_pow_exp_re` 📖	mathematical	`Complex.IsExpCmpFilter`	`Asymptotics.IsLittleO` `Complex` `Real` `Real.norm` `Monoid.toNatPow` `Real.instMonoid` `Complex.im` `Real.exp` `Complex.re`	—	`Asymptotics.IsLittleO.of_pow` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass` `two_ne_zero` `pow_mul'` `isBigO_im_pow_re` `pow_one` `Asymptotics.IsLittleO.comp_tendsto` `Nat.instAtLeastTwoHAddOfNat` `Asymptotics.isLittleO_pow_pow_atTop_of_lt` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Filter.Tendsto.comp` `Real.tendsto_exp_atTop` `tendsto_re`
`isLittleO_log_norm_re` 📖	mathematical	`Complex.IsExpCmpFilter`	`Asymptotics.IsLittleO` `Complex` `Real` `Real.norm` `Real.log` `Norm.norm` `Complex.instNorm` `Complex.re`	—	`Nat.instAtLeastTwoHAddOfNat` `Asymptotics.IsBigO.of_norm_eventuallyLE` `Filter.Eventually.mono` `Filter.Tendsto.eventually_ge_atTop` `tendsto_re` `Real.instIsOrderedRing` `Real.instNontrivial` `LE.le.trans` `Complex.re_le_norm` `lt_max_iff` `LT.lt.trans_le` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.norm_of_nonneg` `Real.log_nonneg` `Real.log_mul` `LT.lt.ne'` `Real.log_le_log_iff` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_trans` `zero_le_one` `Complex.norm_le_sqrt_two_mul_max` `Asymptotics.IsLittleO.add` `Asymptotics.isLittleO_const_left` `tendsto_abs_re` `Asymptotics.isLittleO_iff_nat_mul_le` `Filter.mp_mem` `Filter.Tendsto.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `abs_im_pow_eventuallyLE_exp_re` `Asymptotics.isLittleO_iff_nat_mul_le'` `isLittleO_log_re_re` `Filter.univ_mem'` `le_total` `max_eq_left` `max_eq_right` `Real.norm_eq_abs` `abs_of_pos` `Real.log_pos` `Nat.cast_one` `Real.log_pow` `Real.log_le_iff_le_exp` `pow_pos` `LT.lt.trans`
`isLittleO_log_re_re` 📖	mathematical	`Complex.IsExpCmpFilter`	`Asymptotics.IsLittleO` `Complex` `Real` `Real.norm` `Real.log` `Complex.re`	—	`Asymptotics.IsLittleO.comp_tendsto` `Real.isLittleO_log_id_atTop` `tendsto_re`
`isLittleO_pow_mul_exp` 📖	mathematical	`Complex.IsExpCmpFilter` `Real` `Real.instLT`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Complex.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.exp` `Complex.ofReal`	—	`Complex.cpow_natCast` `isLittleO_cpow_mul_exp`
`isLittleO_zpow_mul_exp` 📖	mathematical	`Complex.IsExpCmpFilter` `Real` `Real.instLT`	`Asymptotics.IsLittleO` `Complex` `Complex.instNorm` `Complex.instMul` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `Complex.exp` `Complex.ofReal`	—	`Complex.cpow_intCast` `isLittleO_cpow_mul_exp`
`isTheta_cpow_exp_re_mul_log` 📖	mathematical	`Complex.IsExpCmpFilter`	`Asymptotics.IsTheta` `Complex` `Real` `Complex.instNorm` `Real.norm` `Complex.instPow` `Real.exp` `Real.instMul` `Complex.re` `Real.log` `Norm.norm`	—	`Complex.isTheta_cpow_const_rpow` `eventually_ne` `Filter.Eventually.mono` `Real.rpow_def_of_pos` `norm_pos_iff` `mul_comm`
`of_boundedUnder_abs_im` 📖	mathematical	`Filter.Tendsto` `Complex` `Real` `Complex.re` `Filter.atTop` `Real.instPreorder` `Filter.IsBoundedUnder` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Complex.im`	`Complex.IsExpCmpFilter`	—	`of_isBigO_im_re_pow` `pow_zero` `Filter.IsBoundedUnder.isBigO_const` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`of_boundedUnder_im` 📖	mathematical	`Filter.Tendsto` `Complex` `Real` `Complex.re` `Filter.atTop` `Real.instPreorder` `Filter.IsBoundedUnder` `Real.instLE` `Complex.im`	`Complex.IsExpCmpFilter`	—	`of_boundedUnder_abs_im` `Filter.isBoundedUnder_le_abs` `Real.instIsOrderedAddMonoid`
`of_isBigO_im_re_pow` 📖	mathematical	`Filter.Tendsto` `Complex` `Real` `Complex.re` `Filter.atTop` `Real.instPreorder` `Asymptotics.IsBigO` `Real.norm` `Complex.im` `Monoid.toNatPow` `Real.instMonoid`	`Complex.IsExpCmpFilter`	—	`of_isBigO_im_re_rpow` `Real.rpow_natCast`
`of_isBigO_im_re_rpow` 📖	mathematical	`Filter.Tendsto` `Complex` `Real` `Complex.re` `Filter.atTop` `Real.instPreorder` `Asymptotics.IsBigO` `Real.norm` `Complex.im` `Real.instPow`	`Complex.IsExpCmpFilter`	—	`Asymptotics.IsLittleO.isBigO` `Asymptotics.IsBigO.pow` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass` `Filter.Eventually.mono` `Filter.Tendsto.eventually_ge_atTop` `Real.rpow_mul` `Real.rpow_natCast` `Asymptotics.IsLittleO.comp_tendsto` `isLittleO_rpow_exp_atTop`
`tendsto_abs_re` 📖	mathematical	`Complex.IsExpCmpFilter`	`Filter.Tendsto` `Complex` `Real` `abs` `Real.lattice` `Real.instAddGroup` `Complex.re` `Filter.atTop` `Real.instPreorder`	—	`Filter.Tendsto.comp` `Filter.tendsto_abs_atTop_atTop` `tendsto_re`
`tendsto_norm` 📖	mathematical	`Complex.IsExpCmpFilter`	`Filter.Tendsto` `Complex` `Real` `Norm.norm` `Complex.instNorm` `Filter.atTop` `Real.instPreorder`	—	`Filter.tendsto_atTop_mono` `Complex.abs_re_le_norm` `tendsto_abs_re`
`tendsto_re` 📖	mathematical	`Complex.IsExpCmpFilter`	`Filter.Tendsto` `Complex` `Real` `Complex.re` `Filter.atTop` `Real.instPreorder`	—	—

---

← Back to Index