Exponential

📁 Source: Mathlib/Analysis/Complex/Exponential.lean

Statistics

Metric	Count
Definitions `exp`, `exp'`, `expMonoidHom`, `termCexp`, `evalExp`, `exp`, `expMonoidHom`, `expNear`, `termRexp`	9
Theorems `expMonoidHom_apply`, `exp_add`, `exp_bound`, `exp_bound'`, `exp_conj`, `exp_def`, `exp_int_mul`, `exp_list_sum`, `exp_multiset_sum`, `exp_nat_mul`, `exp_ne_zero`, `exp_neg`, `exp_nsmul`, `exp_nsmul'`, `exp_ofReal_im`, `exp_ofReal_re`, `exp_sub`, `exp_sum`, `exp_zero`, `isCauSeq_exp`, `isCauSeq_norm_exp`, `norm_exp_le_exp_norm`, `norm_exp_ofReal`, `norm_exp_sub_one_le`, `norm_exp_sub_one_sub_id_le`, `norm_exp_sub_sum_le_exp_norm_sub_sum`, `norm_exp_sub_sum_le_norm_mul_exp`, `ofReal_exp`, `ofReal_exp_ofReal_re`, `sum_div_factorial_le`, `abs_exp`, `abs_exp_sub_one_le`, `abs_exp_sub_one_sub_id_le`, `add_one_le_exp`, `add_one_lt_exp`, `expMonoidHom_apply`, `expNear_sub`, `expNear_succ`, `expNear_zero`, `exp_1_approx_succ_eq`, `exp_abs_le`, `exp_add`, `exp_approx_end`, `exp_approx_end'`, `exp_approx_start`, `exp_approx_succ`, `exp_bound`, `exp_bound'`, `exp_bound_div_one_sub_of_interval`, `exp_bound_div_one_sub_of_interval'`, `exp_eq_exp`, `exp_eq_one_iff`, `exp_injective`, `exp_le_exp`, `exp_le_exp_of_le`, `exp_le_one_iff`, `exp_list_sum`, `exp_lt_exp`, `exp_lt_exp_of_lt`, `exp_lt_one_iff`, `exp_monotone`, `exp_multiset_sum`, `exp_nat_mul`, `exp_ne_zero`, `exp_neg`, `exp_nonneg`, `exp_nsmul`, `exp_pos`, `exp_strictMono`, `exp_sub`, `exp_sum`, `exp_zero`, `le_inv_mul_exp`, `norm_exp_sub_one_sub_id_le`, `one_le_exp`, `one_le_exp_iff`, `one_lt_exp_iff`, `one_sub_div_pow_le_exp_neg`, `one_sub_le_exp_neg`, `one_sub_lt_exp_neg`, `pow_div_factorial_le_exp`, `prod_one_add_le_exp_sum`, `quadratic_le_exp_of_nonneg`, `sum_le_exp_of_nonneg`	84
Total	93

Complex

Definitions

Name	Category	Theorems
`exp` 📖	CompOp	351 math math: `ProbabilityTheory.integrable_cexp_mul_of_re_mem_integrableExpSet`, `ProbabilityTheory.isGaussian_iff_gaussian_charFun`, `nnnorm_exp_I_mul_ofReal`, `continuousOn_exp`, `GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I`, `EisensteinSeries.hasSum_e2Summand_symmetricIcc`, `GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I`, `HurwitzZeta.hasSum_int_cosKernel₀`, `exp_eq_exp_iff_exists_int`, `Real.fourierIntegralInv_eq'`, `comap_exp_cobounded`, `cos_sub_sin_I`, `MeasureTheory.charFunDual_apply`, `isLittleO_exp_neg_mul_sq_cocompact`, `ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq`, `summableLocallyUniformlyOn_iteratedDerivWithin_cexp`, `isCoveringMap_exp`, `ContDiffWithinAt.cexp`, `ModularForm.eta_q_eq_pow`, `locally_lipschitz_exp`, `ZMod.LFunction_one_sub`, `exp_re`, `tsum_exp_neg_mul_int_sq`, `exp_add_mul_I`, `GaussianFourier.integral_cexp_neg_mul_sq_norm`, `angle_exp_one`, `GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace`, `norm_eq_one_iff'`, `ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet`, `fourierIntegral_gaussian_innerProductSpace'`, `sqrt_eq_exp`, `fourier_gaussian_pi'`, `iteratedDerivWithin_tsum_cexp_eq`, `jacobiTheta₂_functional_equation`, `ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq`, `exp_eq_exp_ℂ`, `GaussianFourier.integral_cexp_neg_mul_sq_norm_add`, `norm_cexp_neg_mul_sq`, `hasStrictFDerivAt_exp_real`, `Real.norm_exp_I_mul_ofReal_sub_one_le`, `Real.vector_fourierIntegral_eq_integral_exp_smul`, `HurwitzZeta.evenKernel_def`, `Real.fourier_real_eq_integral_exp_smul`, `hasSum_nat_jacobiTheta`, `exp_add`, `ZMod.stdAddChar_coe`, `Real.nnnorm_exp_I_mul_ofReal_sub_one_le`, `exp_def`, `HurwitzZeta.oddKernel_def'`, `fourier_gaussian_innerProductSpace`, `sinh_add_cosh`, `isPrimitiveRoot_exp_rat`, `tendsto_exp_nhds_zero_iff`, `mem_rootsOfUnity`, `MeasureTheory.charFun_apply`, `cexp_tsum_eq_tprod`, `ProbabilityTheory.charFun_multivariateGaussian`, `two_sinh`, `exp_zero`, `exp_antiperiodic`, `MeasureTheory.charFun_apply_real`, `exp_add_pi_mul_I`, `log_exp_eq_re_add_toIocMod`, `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace`, `LindemannWeierstrass.exp_polynomial_approx`, `MeasureTheory.iteratedFDeriv_charFun`, `Differentiable.cexp`, `cos_eq_iff_quadratic`, `integral_exp_mul_complex_Ioi`, `ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet`, `ContDiff.cexp`, `exp_eq_exp_iff_exp_sub_eq_one`, `tendsto_one_add_cpow_exp_of_tendsto`, `exp_nsmul`, `AnalyticWithinAt.cexp`, `tendsto_exp_comap_re_atTop`, `ofReal_cpow_of_nonpos`, `exp_ofReal_re`, `HurwitzZeta.expZeta_one_sub`, `ContinuousAt.cexp`, `fourierIntegral_gaussian_pi`, `tendsto_pow_exp_of_isLittleO_sub_add_div`, `norm_exp_I_mul_ofReal_sub_one`, `integral_exp_mul_complex`, `comap_exp_nhds_zero`, `HasSum.cexp`, `map_exp_comap_re_atTop`, `differentiable_exp`, `norm_eq_one_iff`, `exp_ofReal_mul_I_re`, `fourier_gaussian_innerProductSpace'`, `HurwitzZeta.hasSum_int_cosKernel`, `IsExpCmpFilter.isLittleO_exp_cpow`, `Real.tendsto_integral_gaussian_smul'`, `exp_neg_pi_div_two_mul_I`, `GaussianFourier.integrable_cexp_neg_mul_sum_add`, `exp_nsmul'`, `Continuous.cexp`, `Polynomial.int_cyclotomic_rw`, `tendsto_one_add_div_pow_exp`, `isIntegral_exp_rat_mul_pi_mul_I`, `riemannZeta_eulerProduct_exp_log`, `HasStrictFDerivAt.cexp`, `ProbabilityTheory.IsGaussian.charFun_eq'`, `integral_mul_cexp_neg_mul_sq`, `isPrimitiveRoot_iff`, `exp_periodic`, `norm_exp_mul_sq_le`, `comap_exp_nhdsNE`, `exp_nat_mul_two_pi_mul_I`, `log_exp_eq_sub_toIocDiv`, `norm_exp_sub_sum_le_norm_mul_exp`, `logDeriv_exp`, `ProbabilityTheory.complexMGF_gaussianReal`, `isPrimitiveRoot_exp_of_isCoprime`, `integral_exp_mul_I_eq_sinc`, `UpperHalfPlane.norm_exp_two_pi_I_lt_one`, `HurwitzZeta.hasSum_int_cosZeta`, `arg_exp_mul_I`, `ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero`, `BoundedContinuousFunction.innerProbChar_apply`, `Measurable.cexp`, `HasFDerivWithinAt.cexp`, `EisensteinSeries.hasSum_e2Summand_symmetricIco`, `ModularForm.eta_q_eq_cexp`, `EisensteinSeries.q_expansion_riemannZeta`, `Real.fourierIntegral_real_eq_integral_exp_smul`, `map_exp_comap_re_atBot`, `fourier_coe_apply`, `integral_exp_mul_I_eq_sin`, `HasStrictDerivAt.cexp`, `cos_add_sin_I`, `ProbabilityTheory.isGaussian_iff_charFun_eq`, `differentiableAt_exp`, `iter_deriv_exp`, `HasFDerivAt.cexp`, `HurwitzZeta.hasSum_expZeta_of_one_lt_re`, `UniformContinuousOn.cexp`, `exp_neg`, `continuous_exp`, `ModularForm.logDeriv_one_sub_mul_cexp_comp`, `tendsto_exp_comap_re_atBot`, `exp_list_sum`, `ofReal_exp`, `exp_ofReal_mul_I_im`, `AnalyticOnNhd.cexp`, `derivWithin_cexp`, `analyticOnNhd_cexp`, `ProbabilityTheory.IsGaussian.charFunDual_eq`, `tsum_exp_neg_quadratic`, `isAddQuotientCoveringMap_exp`, `cot_pi_eq_exp_ratio`, `exp_ofReal_im`, `contDiff_exp`, `HurwitzZeta.hasSum_int_sinKernel`, `two_cosh`, `HurwitzZeta.LSeriesHasSum_exp`, `deriv_cexp`, `isPrimitiveRoot_exp_of_coprime`, `MeasureTheory.charFunDual_map_const_add`, `MeasureTheory.charFunDual_map_add_const`, `exp_pi_div_two_mul_I`, `integral_cexp_quadratic`, `measurable_exp`, `norm_mul_exp_arg_mul_I`, `isPrimitiveRoot_exp_rat_of_even_num`, `isPrimitiveRoot_exp`, `ProbabilityTheory.isGaussian_iff_gaussian_charFunDual`, `ModularForm.logDeriv_one_sub_cexp`, `isIntegral_exp_neg_rat_mul_pi_mul_I`, `circleMap_zero`, `integrableOn_exp_mul_complex_Iic`, `Real.fourierIntegral_eq'`, `contDiffOn_tsum_cexp`, `fourierIntegral_gaussian_innerProductSpace`, `ProbabilityTheory.HasGaussianLaw.charFun_map_eq`, `cexp_neg_quadratic_isLittleO_abs_rpow_cocompact`, `EisensteinSeries.qExpansion_identity_pnat`, `isCoveringMapOn_exp`, `log_exp`, `norm_exp_ofReal`, `GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I'`, `ofReal_exp_ofReal_re`, `tendsto_one_add_div_cpow_exp`, `MeasureTheory.iteratedDeriv_charFun`, `jacobiTheta₂'_add_left'`, `jacobiTheta₂'_functional_equation`, `expMonoidHom_apply`, `exp_sub_sum_range_succ_isLittleO_pow`, `ProbabilityTheory.integrable_cexp_mul_of_re_mem_interior_integrableExpSet`, `AEMeasurable.cexp`, `exp_sub_sum_range_isBigO_pow`, `IsExpCmpFilter.isLittleO_zpow_mul_exp`, `exp_sub_cosh`, `enorm_exp_I_mul_ofReal`, `analyticOn_cexp`, `exp_bound`, `LindemannWeierstrass.integral_exp_mul_eval`, `Real.tendsto_integral_cexp_sq_smul`, `hasStrictDerivAt_exp`, `Real.enorm_exp_I_mul_ofReal_sub_one_le`, `EisensteinSeries.q_expansion_bernoulli`, `LogDeriv_exp`, `DirichletCharacter.LSeries_eulerProduct_exp_log`, `Real.fourierChar_apply`, `GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I`, `GaussianFourier.integral_cexp_neg_mul_sum_add`, `ProbabilityTheory.isGaussian_iff_charFunDual_eq`, `fourierIntegral_gaussian`, `norm_exp_sub_one_le`, `norm_exp`, `HurwitzZeta.hurwitzZeta_one_sub`, `integral_gaussian_sq_complex`, `exp_pi_mul_I`, `isPrimitiveRoot_exp_rat_of_odd_num`, `TendstoUniformlyOn.comp_cexp`, `ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun`, `exp_sub_pi_mul_I`, `Set.Countable.preimage_cexp`, `exp_conj`, `nnnorm_exp_ofReal_mul_I`, `HasDerivWithinAt.cexp`, `exp_sub_sinh`, `cexp_neg_quadratic_isLittleO_rpow_atTop`, `ProbabilityTheory.integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet`, `exp_bound'`, `ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet`, `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add`, `DifferentiableOn.cexp`, `ProbabilityTheory.charFun_stdGaussian`, `ProbabilityTheory.complexMGF_id_gaussianReal`, `exp_rat_mul_pi_mul_I_pow_two_mul_den`, `HasDerivAt.cexp`, `exp_mem_slitPlane`, `MeasureTheory.charFunDual_dirac`, `EisensteinSeries.G2_eq_tsum_cexp`, `EisensteinSeries.qExpansion_identity`, `norm_exp_eq_iff_re_eq`, `GaussianFourier.integral_cexp_neg_sum_mul_add`, `ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow`, `tendsto_one_add_pow_exp_of_tendsto`, `tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow`, `rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val`, `Filter.Tendsto.cexp`, `HurwitzZeta.hasSum_int_sinZeta`, `ZMod.toCircle_intCast`, `ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log`, `ZMod.toCircle_natCast`, `cpow_eq_nhds'`, `exp_eq_exp_re_mul_sin_add_cos`, `jacobiTheta_eq_tsum_nat`, `DifferentiableAt.cexp`, `ContDiffAt.cexp`, `cpow_def`, `Real.tendsto_integral_gaussian_smul`, `exp_sub`, `hasProd_of_hasSum_log`, `VectorFourier.fourierIntegral_probChar`, `MeasureTheory.charFun_dirac`, `cot_eq_exp_ratio`, `norm_exp_sub_one_sub_id_le`, `exp_nat_mul`, `fourier_coe_apply'`, `norm_exp_le_exp_norm`, `IsExpCmpFilter.isLittleO_cpow_exp`, `ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero`, `norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le`, `exp_sum`, `ProbabilityTheory.IsGaussian.charFun_eq`, `integral_gaussian_complex`, `DifferentiableWithinAt.cexp`, `ZMod.toCircle_apply`, `GaussianFourier.integrable_cexp_neg_sum_mul_add`, `integral_exp_mul_complex_Iic`, `norm_exp_sub_sum_le_exp_norm_sub_sum`, `iteratedDeriv_cexp_const_mul`, `range_exp`, `jacobiTheta₂_add_left'`, `norm_exp_ofReal_mul_I`, `Circle.coe_exp`, `exp_two_pi_mul_I`, `cpow_eq_nhds`, `arg_exp`, `IsExpCmpFilter.isLittleO_pow_mul_exp`, `exp_ofReal_mul_I`, `integrable_cexp_quadratic`, `image_exp_Ioc_eq_sphere`, `exp_eq_one_iff`, `analyticWithinAt_cexp`, `exp_mul_I_antiperiodic`, `cpow_def_of_ne_zero`, `exp_mul_I`, `hasDerivAt_exp`, `HurwitzZeta.hasSum_int_completedCosZeta`, `TorusIntegrable.function_integrable`, `exp_log`, `integrable_mul_cexp_neg_mul_sq`, `isOpenMap_exp`, `ProbabilityTheory.IsGaussian.charFunDual_eq'`, `enorm_exp_ofReal_mul_I`, `Real.probChar_apply`, `AnalyticAt.cexp'`, `ProbabilityTheory.charFun_gaussianReal`, `HurwitzZeta.hasSum_int_completedSinZeta`, `Real.fourierInv_eq'`, `norm_exp_I_mul_ofReal`, `integrable_cexp_quadratic'`, `ContinuousWithinAt.cexp`, `exp_mul_I_periodic`, `ContDiffOn.cexp`, `integral_cpow_mul_exp_neg_mul_Ioi`, `range_exp_mul_I`, `MeasureTheory.charFun_map_const_add`, `IsExpCmpFilter.isLittleO_cpow_mul_exp`, `exp_multiset_sum`, `summable_pow_mul_cexp`, `ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq`, `summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp`, `deriv_exp`, `Real.fourier_eq'`, `integrable_cexp_neg_mul_sq`, `LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv`, `exp_int_mul`, `exp_int_mul_two_pi_mul_I`, `log_exp_exists`, `AnalyticAt.cexp`, `CFC.complex_exp_eq_normedSpace_exp`, `fourier_gaussian_pi`, `sinh_sub_cosh`, `exp_im`, `continuousAt_gaussian_integral`, `cosh_sub_sinh`, `EulerProduct.exp_tsum_primes_log_eq_tsum`, `fourierIntegral_gaussian_pi'`, `integral_gaussian_complex_Ioi`, `ProbabilityTheory.charFunDual_stdGaussian`, `MeasureTheory.charFun_map_add_const`, `two_sin`, `differentiableAt_iteratedDerivWithin_cexp`, `pi_mul_cot_pi_q_exp`, `cosh_add_sinh`, `BoundedContinuousFunction.probCharDual_apply`, `ContinuousOn.cexp`, `exp_bound_sq`, `tendsto_exp_comap_re_atBot_nhdsNE`, `integrableOn_exp_mul_complex_Ioi`, `angle_exp_exp`, `two_cos`, `AnalyticOn.cexp`, `countable_preimage_exp`, `analyticAt_cexp`
`exp'` 📖	CompOp	1 math math: `exp_def`
`expMonoidHom` 📖	CompOp	1 math math: `expMonoidHom_apply`
`termCexp` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `Complex` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instSemiring` `MonoidHom.instFunLike` `expMonoidHom` `exp` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`exp_add` 📖	mathematical	—	`exp` `Complex` `instAdd` `instMul`	—	`Finset.sum_congr` `add_pow` `div_eq_mul_inv` `Finset.sum_mul` `Nat.cast_ne_zero` `instCharZero` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `Nat.choose_pos` `Finset.mem_range` `Nat.choose_mul_factorial_mul_factorial` `Nat.cast_mul` `mul_inv` `mul_assoc` `mul_left_comm` `mul_comm` `inv_mul_cancel₀` `mul_one` `Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete` `exp_def` `isCauSeq_exp` `CauSeq.lim_mul_lim` `CauSeq.lim_eq_lim_of_equiv` `cauchy_product` `isCauSeq_norm_exp`
`exp_bound` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `Real.instOne`	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `instSub` `exp` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `Real.instMul` `Real.instMonoid` `Real.instNatCast` `Real.instInv`	—	`Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete` `CauSeq.lim_const` `exp_def` `sub_eq_add_neg` `CauSeq.lim_neg` `CauSeq.lim_add` `IsAbsoluteValue.abs_isAbsoluteValue` `Real.instIsCompleteAbs` `lim_norm` `CauSeq.lim_le` `CauSeq.le_of_exists` `Finset.sum_range_sub_sum_range` `Finset.sum_congr` `mul_div_assoc` `pow_add` `add_tsub_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Finset.mem_range` `Finset.mem_filter` `IsAbsoluteValue.abv_sum` `Real.instIsOrderedRing` `norm_mul` `norm_pow` `norm_div` `norm_natCast` `Finset.sum_le_sum` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_le_one₀` `norm_nonneg` `le_of_lt` `Nat.cast_pos'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Nat.factorial_pos` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `one_div` `sum_div_factorial_le`
`exp_bound'` 📖	mathematical	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `Complex` `instNorm` `Real.instNatCast` `Real.instOne` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `instSub` `exp` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `Real.instMul` `Real.instDivInvMonoid` `Real.instMonoid` `Real.instNatCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete` `CauSeq.lim_const` `exp_def` `sub_eq_add_neg` `CauSeq.lim_neg` `CauSeq.lim_add` `IsAbsoluteValue.abs_isAbsoluteValue` `Real.instIsCompleteAbs` `lim_norm` `CauSeq.lim_le` `CauSeq.le_of_exists` `add_tsub_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Finset.sum_range_add_sub_sum_range` `IsAbsoluteValue.abv_sum` `Real.instIsOrderedRing` `Finset.sum_congr` `norm_div` `norm_pow` `norm_natCast` `instReflLe` `Finset.sum_le_sum` `Real.instIsOrderedAddMonoid` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `norm_nonneg` `le_refl` `mul_pos` `Nat.cast_pos'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Nat.factorial_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Nat.factorial_mul_pow_le_factorial` `pow_add` `div_eq_inv_mul` `mul_inv` `mul_assoc` `mul_left_comm` `Finset.mul_sum` `mul_le_mul_of_nonneg_left` `geom_sum_eq` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.mul_eq` `neg_eq_zero` `Mathlib.Tactic.Linarith.without_one_mul` `sub_eq_zero_of_eq` `div_le_iff_of_neg` `lt_of_not_ge` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.CancelDenoms.neg_subst` `Mathlib.Tactic.CancelDenoms.mul_subst` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Nat.cast_succ` `div_pow` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `Right.add_pos_of_nonneg_of_pos` `Nat.cast_nonneg'` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial`
`exp_conj` 📖	mathematical	—	`exp` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing`	—	`Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete` `exp_def` `lim_conj` `CauSeq.ext` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `instCharZero` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass` `Finset.sum_congr` `map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `ofReal_natCast` `conj_ofReal`
`exp_def` 📖	mathematical	—	`exp` `CauSeq.lim` `Real` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Complex` `instRing` `Norm.norm` `instNorm` `isAbsoluteValueNorm` `instIsComplete` `exp'`	—	`Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete`
`exp_int_mul` 📖	mathematical	—	`exp` `Complex` `instMul` `instIntCast` `DivInvMonoid.toZPow` `instDivInvMonoid`	—	`Int.cast_natCast` `exp_nat_mul` `zpow_natCast` `Int.cast_negSucc` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `add_mul` `Distrib.rightDistribClass` `neg_mul` `one_mul` `exp_add` `exp_neg` `zpow_negSucc` `pow_add` `pow_one` `mul_inv_rev`
`exp_list_sum` 📖	mathematical	—	`exp` `Complex` `instAdd` `instZero` `instMul` `instOne`	—	`map_list_prod` `MonoidHom.instMonoidHomClass`
`exp_multiset_sum` 📖	mathematical	—	`exp` `Multiset.sum` `Complex` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Multiset.prod` `CommRing.toCommMonoid` `Multiset.map`	—	`MonoidHom.map_multiset_prod`
`exp_nat_mul` 📖	mathematical	—	`exp` `Complex` `instMul` `instNatCast` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`Nat.cast_zero` `MulZeroClass.zero_mul` `exp_zero` `pow_zero` `pow_succ` `Nat.cast_add_one` `add_mul` `Distrib.rightDistribClass` `exp_add` `one_mul`
`exp_ne_zero` 📖	—	—	—	—	`zero_ne_one` `NeZero.charZero_one` `instCharZero` `exp_zero` `add_neg_cancel` `exp_add` `MulZeroClass.zero_mul`
`exp_neg` 📖	mathematical	—	`exp` `Complex` `instNeg` `instInv`	—	`mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Field.isDomain` `exp_ne_zero` `exp_add` `add_neg_cancel` `exp_zero` `mul_inv_cancel₀`
`exp_nsmul` 📖	mathematical	—	`exp` `Complex` `AddMonoid.toNSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `addGroupWithOne` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`MonoidHom.map_pow`
`exp_nsmul'` 📖	mathematical	—	`exp` `Complex` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `instNatCast` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`exp_nsmul` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `Mathlib.Tactic.Ring.nsmul_congr` `Mathlib.Tactic.Ring.smul_eq_cast` `Mathlib.Tactic.Ring.natCast_add` `Mathlib.Tactic.Ring.natCast_mul` `Mathlib.Tactic.Ring.natCast_nat` `Mathlib.Tactic.Ring.natCast_zero`
`exp_ofReal_im` 📖	mathematical	—	`im` `exp` `ofReal` `Real` `Real.instZero`	—	`ofReal_exp_ofReal_re` `ofReal_im`
`exp_ofReal_re` 📖	mathematical	—	`re` `exp` `ofReal` `Real.exp`	—	—
`exp_sub` 📖	mathematical	—	`exp` `Complex` `instSub` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`sub_eq_add_neg` `exp_add` `exp_neg` `div_eq_mul_inv`
`exp_sum` 📖	mathematical	—	`exp` `Finset.sum` `Complex` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.prod` `CommRing.toCommMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`exp_zero` 📖	mathematical	—	`exp` `Complex` `instZero` `instOne`	—	`Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete` `exp_def` `CauSeq.lim_eq_of_equiv_const` `not_le_of_gt` `zero_lt_one` `Nat.instZeroLEOneClass` `Finset.sum_congr` `zero_add` `Finset.sum_singleton` `pow_zero` `Nat.cast_one` `div_self` `NeZero.charZero_one` `instCharZero` `sub_self` `norm_zero` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Finset.sum_range_succ` `pow_succ` `MulZeroClass.mul_zero` `zero_div` `add_zero`
`isCauSeq_exp` 📖	mathematical	—	`IsCauSeq` `Real` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Complex` `instRing` `Norm.norm` `instNorm` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial`	—	`IsCauSeq.of_abv` `Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `isCauSeq_norm_exp`
`isCauSeq_norm_exp` 📖	mathematical	—	`IsCauSeq` `Real` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `Real.instRing` `abs` `Real.lattice` `Real.instAddGroup` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Norm.norm` `Complex` `instNorm` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial`	—	`Real.instIsStrictOrderedRing` `exists_nat_gt` `Real.instArchimedean` `lt_of_le_of_lt` `norm_nonneg` `IsCauSeq.series_ratio_test` `IsAbsoluteValue.abs_isAbsoluteValue` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `le_of_lt` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `one_mul` `abs_norm` `Nat.factorial_succ` `pow_succ'` `mul_comm` `Nat.cast_mul` `div_div` `mul_div_assoc` `mul_div_right_comm` `norm_mul` `norm_div` `norm_natCast` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `div_le_div₀` `le_refl` `Nat.mono_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `le_trans`
`norm_exp_le_exp_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `exp` `Real.exp`	—	`sub_zero` `norm_exp_sub_sum_le_exp_norm_sub_sum`
`norm_exp_ofReal` 📖	mathematical	—	`Norm.norm` `Complex` `instNorm` `exp` `ofReal` `Real.exp`	—	`ofReal_exp` `norm_of_nonneg` `le_of_lt` `Real.exp_pos`
`norm_exp_sub_one_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `Real.instOne`	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `instSub` `exp` `instOne` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_singleton` `pow_zero` `Nat.cast_one` `div_self` `NeZero.charZero_one` `instCharZero` `exp_bound` `pow_one` `zero_add` `mul_one` `inv_one` `mul_comm` `mul_two` `mul_add` `Distrib.leftDistribClass`
`norm_exp_sub_one_sub_id_le` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `Real.instOne`	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `instSub` `exp` `instOne` `Monoid.toPow` `Real.instMonoid`	—	`sub_eq_add_neg` `add_assoc` `Finset.sum_range_succ_comm` `pow_one` `zero_add` `mul_one` `Nat.cast_one` `div_one` `Finset.sum_singleton` `pow_zero` `div_self` `NeZero.charZero_one` `instCharZero` `neg_add_rev` `exp_bound` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_natSucc` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.raw_refl` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isRat_le_true` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul`
`norm_exp_sub_sum_le_exp_norm_sub_sum` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `instSub` `exp` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `Real.instSub` `Real.exp` `Real.instAddCommMonoid` `Real.instDivInvMonoid` `Real.instMonoid` `Real.instNatCast`	—	`Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete` `CauSeq.lim_const` `exp_def` `sub_eq_add_neg` `CauSeq.lim_neg` `CauSeq.lim_add` `IsAbsoluteValue.abs_isAbsoluteValue` `Real.instIsCompleteAbs` `lim_norm` `CauSeq.lim_le` `CauSeq.le_of_exists` `Finset.sum_range_sub_sum_range` `LE.le.trans_eq` `IsAbsoluteValue.abv_sum` `Real.instIsOrderedRing` `norm_div` `norm_pow` `norm_natCast` `sub_le_sub_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.sum_le_exp_of_nonneg` `norm_nonneg`
`norm_exp_sub_sum_le_norm_mul_exp` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `instNorm` `instSub` `exp` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `Real.instMul` `Real.instMonoid` `Real.exp`	—	`Real.instIsStrictOrderedRing` `isAbsoluteValueNorm` `instIsComplete` `CauSeq.lim_const` `exp_def` `sub_eq_add_neg` `CauSeq.lim_neg` `CauSeq.lim_add` `IsAbsoluteValue.abs_isAbsoluteValue` `Real.instIsCompleteAbs` `lim_norm` `CauSeq.lim_le` `CauSeq.le_of_exists` `Finset.sum_range_sub_sum_range` `Finset.sum_congr` `mul_div_assoc` `pow_add` `add_tsub_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Finset.mem_range` `Finset.mem_filter` `IsAbsoluteValue.abv_sum` `Real.instIsOrderedRing` `norm_mul` `norm_pow` `norm_div` `norm_natCast` `Finset.sum_le_sum` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `norm_nonneg` `le_refl` `Nat.cast_pos'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Nat.factorial_pos` `Nat.mono_cast` `Nat.factorial_le` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Finset.mul_sum` `Finset.sum_bij` `tsub_lt_tsub_iff_right` `tsub_add_cancel_of_le` `add_tsub_cancel_right` `Real.sum_le_exp_of_nonneg`
`ofReal_exp` 📖	mathematical	—	`ofReal` `Real.exp` `exp`	—	`ofReal_exp_ofReal_re`
`ofReal_exp_ofReal_re` 📖	mathematical	—	`ofReal` `re` `exp`	—	`conj_eq_iff_re` `exp_conj` `conj_ofReal`
`sum_div_factorial_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.filter` `Finset.range` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `AddMonoidWithOne.toNatCast` `Nat.factorial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_nbij'` `Nat.instOrderedSub` `tsub_add_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `add_tsub_cancel_right` `one_div` `Finset.sum_congr` `Finset.sum_le_sum` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `inv_anti₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_pos` `Nat.cast_pos'` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Nat.factorial_pos` `pow_pos` `Nat.cast_pow` `Nat.cast_mul` `Nat.cast_le` `add_comm` `Nat.factorial_mul_pow_le_factorial` `Nat.cast_add` `Nat.cast_one` `mul_inv_rev` `mul_comm` `inv_pow` `pos_iff_ne_zero` `ne_of_gt` `add_sub_cancel_right` `geom_sum_inv` `eq_div_iff_mul_eq` `mul_assoc` `mul_inv_cancel₀` `one_mul` `div_le_div_of_nonneg_right` `sub_le_self` `le_of_lt` `inv_pos_of_pos`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalExp` 📖	CompOp	—

Real

Definitions

Name	Category	Theorems
`exp` 📖	CompOp	516 math math: `Behrend.roth_lower_bound`, `HurwitzZeta.isBigO_atTop_evenKernel_sub`, `NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'`, `MeasureTheory.setIntegral_tilted`, `abs_exp_sub_one_le`, `Polynomial.mahlerMeasure_def_of_ne_zero`, `deriv_exp`, `map_exp_nhds`, `Continuous.rexp`, `sinh_eq`, `mellin_eq_fourier`, `Complex.isTheta_exp_arg_mul_im`, `ProbabilityTheory.gammaPDF_of_nonneg`, `ProbabilityTheory.measure_ge_le_exp_cgf`, `GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I`, `ProbabilityTheory.measure_sum_ge_le_of_HasCondSubgaussianMGF`, `HurwitzZeta.hasSum_int_cosKernel₀`, `ProbabilityTheory.aemeasurable_exp_mul`, `exp_sub_sinh`, `Stirling.factorial_isEquivalent_stirling`, `norm_jacobiTheta₂_term_le`, `ProbabilityTheory.mgf_const_add`, `Complex.GammaIntegral_eq_mellin`, `rpow_eq_nhds_of_neg`, `integrableOn_exp_mul_Iic`, `ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul`, `UpperHalfPlane.im_div_exp_dist_le`, `integral_exp_mul_Iic`, `ProbabilityTheory.hasSum_integral_poissonMeasure`, `ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop`, `Complex.exp_re`, `exp_mul`, `tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero`, `isBoundedUnder_le_exp_comp`, `isBoundedUnder_ge_exp_comp`, `Function.Periodic.norm_qParam_le_of_one_half_le_im`, `MeasureTheory.exp_llr_of_ac'`, `Behrend.roth_lower_bound_explicit`, `exp_lt_exp_of_lt`, `ProbabilityTheory.mgf_dirac`, `MeasureTheory.toReal_rnDeriv_tilted_left`, `tendsto_one_add_pow_exp_of_tendsto`, `log_exp`, `norm_exp_sub_one_sub_id_le`, `round_exp_one_eq_three`, `Complex.IsExpCmpFilter.isBigO_im_pow_re`, `exp_nsmul`, `norm_cexp_neg_mul_sq`, `rpow_def_of_pos`, `integral_exp`, `one_le_exp_iff`, `ProbabilityTheory.HasSubgaussianMGF.mgf_le`, `ProbabilityTheory.IsGaussian.integrable_exp_sq_of_conv_neg`, `MeasureTheory.integral_tilted`, `exp_eq_exp`, `tendsto_exp_atTop`, `integrableOn_exp_Iic`, `ProbabilityTheory.cdf_expMeasure_eq`, `Function.Periodic.norm_qParam_lt_iff`, `ProbabilityTheory.tilted_mul_apply_cgf`, `mulExpNegSq_apply`, `one_sub_le_exp_neg`, `integral_exp_neg_mul_rpow`, `HurwitzKernelBounds.isBigO_atTop_F_int_one`, `Stirling.log_stirlingSeq_formula`, `AnalyticOn.rexp`, `exp_bound`, `ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero`, `tendsto_exp_div_pow_atTop`, `AnalyticAt.rexp`, `Complex.integral_rpow_mul_exp_neg_rpow`, `AnalyticOnNhd.rexp`, `rpow_inv_log`, `expPartialHomeomorph_apply`, `integral_rpow_mul_exp_neg_rpow`, `analyticAt_rexp`, `GammaIntegral_convergent`, `MeasureTheory.measure_lt_one_eq_integral_div_gamma`, `UpperHalfPlane.isometry_vertical_line`, `ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_add_compProd`, `exp_one_lt_three`, `comap_exp_nhds_zero`, `ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul`, `Complex.hasDerivAt_GammaIntegral`, `isOpenEmbedding_exp`, `ProbabilityTheory.exp_cgf`, `strictConvexOn_exp`, `HasFDerivWithinAt.exp`, `ProbabilityTheory.mgf_const`, `AEMeasurable.exp`, `analyticOnNhd_rexp`, `exp_sub_sum_range_succ_isLittleO_pow`, `isTheta_exp_comp_one`, `gronwallBound_of_K_ne_0`, `exp_list_sum`, `ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le`, `ProbabilityTheory.integrable_exp_mul_abs`, `ProbabilityTheory.integrable_exp_mul_of_abs_le`, `comap_exp_nhds_exp`, `tendsto_exp_neg_atTop_nhds_zero`, `ProbabilityTheory.integrable_pow_mul_exp_of_integrable_exp_mul`, `UpperHalfPlane.im_le_im_mul_exp_dist`, `Complex.exp_ofReal_re`, `abs_exp_sub_one_sub_id_le`, `tsum_exp_neg_mul_int_sq`, `ContinuousWithinAt.rexp`, `MeasureTheory.integral_exp_tilted`, `ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf'`, `MeasureTheory.llr_tilted_right`, `Complex.GammaIntegral_ofReal`, `Complex.norm_cpow_of_ne_zero`, `exp_arcosh`, `Complex.integral_exp_neg_rpow`, `ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv`, `exp_monotone`, `le_exp_log`, `log_lt_iff_lt_exp`, `ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet`, `prod_one_add_le_exp_sum`, `tendsto_exp_comp_nhds_zero`, `Complex.partialGamma_add_one`, `coe_expOrderIso_apply`, `Complex.norm_cpow_of_imp`, `sigmoid_def`, `ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf`, `Stirling.stirlingSeq_one`, `isBigO_one_exp_comp`, `HurwitzZeta.hasSum_int_cosKernel`, `AnalyticAt.rexp'`, `isBigO_exp_comp_one`, `lt_log_iff_exp_lt`, `norm_jacobiTheta₂_term`, `LogDeriv_exp`, `exp_le_exp_of_le`, `exp_one_mul_le_exp`, `Behrend.lower_bound_le_one`, `sigmoid_mul_rexp_neg`, `le_log_iff_exp_le`, `ProbabilityTheory.integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet`, `ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le`, `Stirling.le_factorial_stirling`, `NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single`, `tendsto_exp_nhds_zero_nhds_one`, `ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul`, `ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul`, `exp_one_gt_d9`, `integral_exp_Iic`, `NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis`, `exp_eq_one_iff`, `ProbabilityTheory.exponentialPDF_eq`, `HurwitzZeta.hasSum_nat_sinKernel`, `HasStrictDerivAt.exp`, `UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left`, `differentiable_exp`, `norm_exp_mul_sq_le`, `isLittleO_exp_mul_rpow_of_lt`, `HurwitzKernelBounds.F_nat_one_le`, `Complex.norm_exp_sub_sum_le_norm_mul_exp`, `Filter.Tendsto.rexp`, `exp_one_rpow`, `ProbabilityTheory.integrable_exp_abs_mul_abs_add`, `isLittleO_pow_exp_atTop`, `two_mul_le_exp`, `exp_one_near_20`, `ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf'`, `sum_le_exp_of_nonneg`, `HurwitzKernelBounds.isBigO_atTop_F_nat_one`, `tendsto_comp_exp_atTop`, `ProbabilityTheory.exponentialPDF_of_nonneg`, `integral_rpow_mul_exp_neg_mul_rpow`, `HasDerivAt.exp`, `rpow_def_of_neg`, `exp_bound_div_one_sub_of_interval`, `MeasureTheory.integral_llr_tilted_left`, `Behrend.bound`, `Behrend.four_zero_nine_six_lt_exp_sixteen`, `Finset.norm_prod_one_add_sub_one_le`, `ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun`, `exp_abs_le`, `ProbabilityTheory.setIntegral_tilted_mul_eq_mgf'`, `deriv_mulExpNegMulSq`, `ProbabilityTheory.iIndepFun.integrable_exp_mul_sum`, `norm_jacobiTheta_sub_one_le`, `isLittleO_rpow_exp_pos_mul_atTop`, `NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq`, `ProbabilityTheory.HasSubgaussianMGF.memLp_exp_mul`, `NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow`, `ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self`, `exp_arsinh`, `ProbabilityTheory.tilted_mul_apply_mgf'`, `ProbabilityTheory.mgf_fun_id_gaussianReal`, `exp_mul_le_cosh_add_mul_sinh`, `HurwitzZeta.hasSum_int_evenKernel`, `summable_exp_neg_nat`, `hasStrictDerivAt_const_rpow_of_neg`, `ModularFormClass.exp_decay_sub_atImInfty`, `EReal.exp_coe`, `MeasureTheory.tilted_apply_eq_ofReal_integral`, `exp_strictMono`, `ProbabilityTheory.gaussianPDFReal_def`, `tendsto_comp_exp_atBot`, `UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty`, `Behrend.exp_neg_two_mul_le`, `isLittleO_exp_neg_mul_rpow_atTop`, `tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact`, `exp_sub_cosh`, `ProbabilityTheory.integrable_exp_mul_of_nonpos_of_ge`, `Complex.ofReal_exp`, `log_le_iff_le_exp`, `isBigO_at_im_infty_jacobiTheta_sub_one`, `HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub`, `ProbabilityTheory.Fernique.lintegral_closedBall_diff_exp_logRatio_mul_sq_le`, `exp_log_of_neg`, `ContDiff.exp`, `derivWithin_exp`, `range_exp`, `MeasureTheory.tilted_apply`, `Complex.integral_exp_neg_mul_rpow`, `Polynomial.hermite_eq_deriv_gaussian'`, `fderiv_exp`, `ProbabilityTheory.Fernique.measure_gt_normThreshold_le_exp`, `HurwitzZeta.hasSum_int_sinKernel`, `MeasureTheory.log_rnDeriv_tilted_left_self`, `ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self'`, `deriv_exp`, `exp_log`, `HurwitzZeta.isBigO_atTop_oddKernel`, `iter_deriv_exp`, `continuousOn_exp`, `ProbabilityTheory.setIntegral_tilted_mul_eq_cgf'`, `log_div_self_antitoneOn`, `Polynomial.deriv_gaussian_eq_hermite_mul_gaussian`, `ProbabilityTheory.aestronglyMeasurable_exp_mul_sum`, `integrable_rpow_mul_exp_neg_mul_sq`, `integral_exp_neg_rpow`, `integrable_mul_exp_neg_mul_sq`, `PhragmenLindelof.isBigO_sub_exp_exp`, `ProbabilityTheory.integrable_exp_mul_of_le_of_le`, `HasFDerivAt.exp`, `ProbabilityTheory.mgf_add_const`, `tendsto_exp_comp_atTop`, `cosh_le_exp_half_sq`, `ProbabilityTheory.integrable_exp_mul_gaussianReal`, `rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg`, `ceil_exp_one_eq_three`, `UpperHalfPlane.le_dist_coe`, `MeasureTheory.integrable_tilted_iff`, `log_div_sqrt_antitoneOn`, `mellin_eq_fourierIntegral`, `cosh_add_sinh`, `isLittleO_exp_comp_exp_comp`, `ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul`, `fderivWithin_exp`, `ProbabilityTheory.exp_neg_integrableOn_Ioc`, `isLittleO_rpow_exp_atTop`, `tendsto_exp_atBot`, `Polynomial.hermite_eq_deriv_gaussian`, `exp_half`, `isLittleO_zpow_exp_pos_mul_atTop`, `continuous_exp`, `intervalIntegral.intervalIntegrable_exp`, `ProbabilityTheory.hasDerivAt_neg_exp_mul_exp`, `summable_exp_nat_mul_of_ge`, `one_sub_lt_exp_neg`, `ProbabilityTheory.integrable_exp_mul_abs_add`, `logDeriv_exp`, `Complex.norm_exp_ofReal`, `integrableOn_rpow_mul_exp_neg_rpow`, `GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I'`, `integrableOn_exp_mul_Ioi`, `ProbabilityTheory.integrable_of_mem_integrableExpSet`, `ProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul`, `MeasureTheory.setLIntegral_tilted`, `ProbabilityTheory.integrable_exp_abs_mul_abs`, `ProbabilityTheory.integral_tilted_mul_eq_mgf`, `NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp`, `rpow_inv_log_le_exp_one`, `pow_div_factorial_le_exp`, `MeasureTheory.exp_neg_llr`, `integral_exp_neg_Ioi`, `ProbabilityTheory.HasSubgaussianMGF.measureReal_le_le_exp`, `MeasureTheory.exp_neg_llr'`, `AnalyticWithinAt.rexp`, `sinh_sub_cosh`, `exp_multiset_sum`, `exp_le_exp`, `Gamma_eq_integral`, `MeasureTheory.rnDeriv_tilted_left`, `ProbabilityTheory.poissonMeasure_singleton`, `ProbabilityTheory.integral_poissonMeasure`, `hasDerivAt_mulExpNegMulSq`, `one_lt_exp_iff`, `map_exp_atBot`, `ProbabilityTheory.measure_sum_ge_le_of_hasCondSubgaussianMGF`, `numDerangements_tendsto_inv_e`, `ProbabilityTheory.mgf_const'`, `Complex.IsExpCmpFilter.isLittleO_im_pow_exp_re`, `ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul`, `Differentiable.exp`, `integrableOn_exp_neg_Ioi`, `coe_comp_expOrderIso`, `isTheta_exp_comp_exp_comp`, `HurwitzZeta.hasSum_int_oddKernel`, `rpow_def_of_nonneg`, `exp_lt_one_iff`, `norm_jacobiTheta₂'_term_le`, `measurable_exp`, `one_sub_div_pow_le_exp_neg`, `NumberField.mixedEmbedding.fundamentalCone.expMap_apply`, `ProbabilityTheory.tilted_mul_apply_mgf`, `ContDiffWithinAt.exp`, `exp_neg_mul_rpow_isLittleO_exp_neg`, `MeasureTheory.setIntegral_tilted'`, `UpperHalfPlane.exp_half_dist`, `exp_neg_mul_sq_isLittleO_exp_neg`, `integral_exp_mul_Ioi`, `HurwitzKernelBounds.F_nat_zero_zero_sub_le`, `exp_one_lt_d9`, `exp_approx_start`, `exp_injective`, `isLittleO_pow_exp_pos_mul_atTop`, `Complex.norm_exp`, `comap_exp_nhdsGT_zero`, `ContDiffOn.exp`, `quadratic_le_exp_of_nonneg`, `summable_pow_mul_exp_neg_nat_mul`, `ProbabilityTheory.gammaPDF_eq`, `isBigO_exp_comp_exp_comp`, `PhragmenLindelof.isBigO_sub_exp_rpow`, `exp_lt_exp`, `ProbabilityTheory.HasSubgaussianMGF.measure_ge_le`, `ProbabilityTheory.rpow_abs_le_mul_max_exp`, `ProbabilityTheory.poissonMeasure_real_singleton`, `rexp_neg_quadratic_isLittleO_rpow_atTop`, `NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply''`, `iteratedDeriv_exp_const_mul`, `integrableOn_Ioi_exp_neg_mul_sq_iff`, `differentiableAt_exp`, `convexOn_exp`, `ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun`, `one_le_exp`, `ProbabilityTheory.rpow_abs_le_mul_exp_abs`, `tendsto_one_add_rpow_exp_of_tendsto`, `MeasureTheory.lintegral_tilted`, `ProbabilityTheory.integrable_pow_abs_mul_exp_of_integrable_exp_mul`, `tendsto_mul_exp_add_div_pow_atTop`, `tendsto_div_pow_mul_exp_add_atTop`, `MeasureTheory.llr_tilted_left`, `ProbabilityTheory.setIntegral_tilted_mul_eq_mgf`, `ProbabilityTheory.mgf_dirac'`, `ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf`, `exp_nonneg`, `exp_artanh`, `integral_gaussian`, `Function.Periodic.norm_qParam`, `comap_exp_atTop`, `hasDerivAt_exp`, `CuspFormClass.exp_decay_atImInfty'`, `ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos`, `Complex.integral_rpow_mul_exp_neg_mul_rpow`, `ProbabilityTheory.setIntegral_tilted_mul_eq_cgf`, `expMonoidHom_apply`, `analyticWithinAt_rexp`, `HurwitzKernelBounds.isBigO_exp_neg_mul_of_le`, `UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty'`, `rpow_eq_nhds_of_pos`, `Behrend.le_sqrt_log`, `Behrend.two_div_one_sub_two_div_e_le_eight`, `ProbabilityTheory.mgf_gaussianReal`, `add_one_lt_exp`, `Complex.IsExpCmpFilter.abs_im_pow_eventuallyLE_exp_re`, `cosh_sub_sinh`, `ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le`, `tanh_eq`, `ProbabilityTheory.mgf_id_gaussianReal`, `ProbabilityTheory.measure_le_le_exp_mul_mgf`, `ProbabilityTheory.integrable_exp_mul_of_le`, `exp_bound'`, `integral_rpow_mul_exp_neg_mul_Ioi`, `ProbabilityTheory.hasSum_one_poissonMeasure`, `sinh_add_cosh`, `ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul`, `log_comp_exp`, `ProbabilityTheory.measure_ge_le_exp_mul_mgf`, `MeasureTheory.exp_llr_of_ac`, `tendsto_exp_div_rpow_atTop`, `exp_zero`, `Gamma_integrand_isLittleO`, `Complex.norm_exp_le_exp_norm`, `Behrend.lower_bound_le_one'`, `HurwitzKernelBounds.F_nat_zero_le`, `Behrend.div_lt_floor`, `UpperHalfPlane.dist_coe_le`, `NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image`, `NumberField.mixedEmbedding.fundamentalCone.expMap_single_apply`, `exp_neg_one_gt_d9`, `exp_neg_integrableOn_Ioi`, `Complex.norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le`, `exp_one_near_10`, `exp_le_one_iff`, `summable_pow_mul_jacobiTheta₂_term_bound`, `integrable_exp_neg_mul_sq_iff`, `ProbabilityTheory.IndepFun.integrable_exp_mul_add`, `MeasureTheory.setLIntegral_tilted'`, `ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet`, `dist_le_of_trajectories_ODE`, `Complex.norm_exp_sub_sum_le_exp_norm_sub_sum`, `exp_one_pow`, `exp_approx_end`, `integrableOn_rpow_mul_exp_neg_mul_sq`, `ProbabilityTheory.aestronglyMeasurable_exp_mul_add`, `NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis`, `DifferentiableOn.exp`, `rpow_def_of_nonpos`, `exp_sub`, `exp_approx_succ`, `ProbabilityTheory.integrable_pow_abs_mul_exp_add_of_integrable_exp_mul`, `floor_exp_one_eq_two`, `integral_exp_neg_Ioi_zero`, `abs_rpow_le_exp_log_mul`, `ruzsaSzemerediNumberNat_lower_bound`, `exp_approx_end'`, `MeasureTheory.tilted_eq_withDensity_nnreal`, `Measurable.exp`, `DifferentiableAt.exp`, `exp_eq_exp_ℝ`, `integral_gaussian_Ioi`, `cosh_eq`, `integrable_exp_neg_mul_sq`, `GaussianFourier.verticalIntegral_norm_le`, `le_inv_mul_exp`, `MeasureTheory.rnDeriv_tilted_right`, `ProbabilityTheory.IndepFun.exp_mul`, `CuspFormClass.exp_decay_atImInfty`, `ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure`, `contDiff_exp`, `exp_bound_div_one_sub_of_interval'`, `HasSum.rexp`, `ProbabilityTheory.integrable_exp_mul_of_mem_Icc`, `ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self`, `Complex.norm_cpow_le`, `Polynomial.tendsto_div_exp_atTop`, `HurwitzZeta.isBigO_atTop_cosKernel_sub`, `ContinuousOn.rexp`, `add_one_le_exp`, `ruzsaSzemerediNumberNat_asymptotic_lower_bound`, `hasStrictFDerivAt_rpow_of_neg`, `exp_one_gt_two`, `ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul`, `Complex.GammaIntegral_convergent`, `rexp_tsum_eq_tprod`, `map_exp_atTop`, `integral_exp_Iic_zero`, `MeasureTheory.tilted_apply_eq_ofReal_integral'`, `UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right`, `HasDerivWithinAt.exp`, `MeasureTheory.integral_llr_tilted_right`, `ProbabilityTheory.integrable_poissonMeasure_iff`, `exp_neg`, `MeasureTheory.rnDeriv_tilted_left_self`, `MeasureTheory.measure_unitBall_eq_integral_div_gamma`, `exp_neg_one_lt_half`, `log_div_self_rpow_antitoneOn`, `ProbabilityTheory.measure_le_le_exp_cgf`, `HurwitzZeta.hasSum_nat_cosKernel₀`, `DifferentiableWithinAt.exp`, `hasProd_of_hasSum_log`, `ContDiffAt.exp`, `exp_sum`, `ContinuousAt.rexp`, `CFC.real_exp_eq_normedSpace_exp`, `ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_integrable_exp_mul`, `MeasureTheory.exp_llr`, `ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le`, `exp_sub_sum_range_isBigO_pow`, `analyticOn_rexp`, `exp_log_eq_abs`, `exp_nat_mul`, `exp_add`, `Complex.IsExpCmpFilter.isTheta_cpow_exp_re_mul_log`, `tendsto_one_add_div_rpow_exp`, `ProbabilityTheory.integral_poissonMeasure'`, `ModularFormClass.exp_decay_sub_atImInfty'`, `tendsto_exp_mul_div_rpow_atTop`, `tendsto_exp_atBot_nhdsGT`, `hasStrictDerivAt_exp`, `MeasureTheory.integral_exp_pos`, `dist_le_of_trajectories_ODE_of_mem`, `summable_exp_nat_mul_iff`, `MeasureTheory.toReal_rnDeriv_tilted_right`, `Complex.exp_im`, `mul_exp_neg_le_exp_neg_one`, `ProbabilityTheory.mgf_pos_iff`, `ProbabilityTheory.tilted_mul_apply_cgf'`, `HasStrictFDerivAt.exp`, `exp_neg_one_lt_d9`, `isLittleO_one_exp_comp`, `exp_1_approx_succ_eq`, `HurwitzZeta.isBigO_atTop_sinKernel`, `Behrend.exp_four_lt`, `MeasureTheory.tilted_apply'`, `Function.Periodic.exp_decay_sub_of_bounded_at_inf`, `HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub`, `tendsto_one_add_div_pow_exp`, `tendsto_pow_mul_exp_neg_atTop_nhds_zero`, `exp_pos`, `Function.Periodic.exp_decay_of_zero_at_inf`, `gronwallBound_ε0`, `GaussianFourier.integral_rexp_neg_mul_sq_norm`, `HurwitzZeta.hasSum_int_evenKernel₀`, `integrableOn_rpow_mul_exp_neg_mul_rpow`, `ProbabilityTheory.IsGaussian.exists_integrable_exp_sq`, `abs_exp`, `ProbabilityTheory.integral_tilted_mul_eq_cgf`, `rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg`, `ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet`
`expMonoidHom` 📖	CompOp	1 math math: `expMonoidHom_apply`
`expNear` 📖	CompOp	7 math math: `expNear_succ`, `expNear_zero`, `expNear_sub`, `exp_approx_end`, `exp_approx_succ`, `exp_approx_end'`, `exp_1_approx_succ_eq`
`termRexp` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_exp` 📖	mathematical	—	`abs` `Real` `lattice` `instAddGroup` `exp`	—	`abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `exp_pos`
`abs_exp_sub_one_le` 📖	mathematical	`Real` `instLE` `abs` `lattice` `instAddGroup` `instOne`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `instOne` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.cast_one` `Complex.norm_real` `Nat.instAtLeastTwoHAddOfNat` `Complex.norm_exp_sub_one_le`
`abs_exp_sub_one_sub_id_le` 📖	mathematical	`Real` `instLE` `abs` `lattice` `instAddGroup` `instOne`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `instOne` `Monoid.toPow` `instMonoid`	—	`sq_abs` `Nat.cast_one` `Complex.norm_real` `Complex.norm_exp_sub_one_sub_id_le`
`add_one_le_exp` 📖	mathematical	—	`Real` `instLE` `instAdd` `instOne` `exp`	—	`eq_or_ne` `zero_add` `exp_zero` `instReflLe` `LT.lt.le` `add_one_lt_exp`
`add_one_lt_exp` 📖	mathematical	—	`Real` `instLT` `instAdd` `instOne` `exp`	—	`Ne.lt_or_gt` `le_or_gt` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_nonpos` `instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `exp_pos` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `exp_neg` `sub_neg_eq_add` `add_comm` `one_div` `inv_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `exp_bound_div_one_sub_of_interval'` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`expMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `Real` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `instAddMonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `semiring` `MonoidHom.instFunLike` `expMonoidHom` `exp` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`expNear_sub` 📖	mathematical	—	`Real` `instSub` `expNear` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial`	—	`add_sub_add_left_eq_sub` `mul_sub`
`expNear_succ` 📖	mathematical	—	`expNear` `Real` `instAdd` `instOne` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `instNatCast`	—	`Finset.sum_congr` `Finset.range_add_one` `div_eq_mul_inv` `Finset.sum_insert` `pow_succ` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one` `mul_inv_rev` `add_assoc` `mul_add` `Distrib.leftDistribClass` `mul_one` `add_left_comm` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `instIsOrderedCancelAddMonoid` `AddSemigroup.to_isAssociative` `AddCommMagma.to_isCommutative` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative`
`expNear_zero` 📖	mathematical	—	`expNear`	—	`pow_zero` `Nat.cast_one` `div_self` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `one_mul` `zero_add`
`exp_1_approx_succ_eq` 📖	mathematical	`Real` `instNatCast` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `instOne` `expNear` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `Nat.factorial`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `instOne` `expNear` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial`	—	`exp_approx_succ` `one_div` `abs_one` `instIsOrderedRing` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Nat.cast_zero` `IsStrictOrderedRing.toCharZero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `mul_one` `zero_lt_one` `instZeroLEOneClass` `NeZero.one` `GroupWithZero.toNontrivial` `add_sub_cancel` `sub_self` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `MulZeroClass.mul_zero` `instReflLe`
`exp_abs_le` 📖	mathematical	—	`Real` `instLE` `exp` `abs` `lattice` `instAddGroup` `instAdd` `instNeg`	—	`le_total` `abs_of_nonpos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `abs_of_nonneg`
`exp_add` 📖	mathematical	—	`exp` `Real` `instAdd` `instMul`	—	`Complex.ofReal_add` `Complex.exp_add` `Complex.exp_ofReal_im` `MulZeroClass.mul_zero` `sub_zero`
`exp_approx_end` 📖	mathematical	`Real` `instLE` `abs` `lattice` `instAddGroup` `instOne`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `expNear` `instZero` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial` `instAdd` `instOne`	—	`MulZeroClass.mul_zero` `add_zero` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Nat.cast_nonneg'` `instZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_pos'` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `exp_bound`
`exp_approx_end'` 📖	mathematical	`Real` `instNatCast` `instLE` `abs` `lattice` `instAddGroup` `instOne` `instSub` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `instAdd`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `expNear` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial`	—	`exp_approx_succ` `MulZeroClass.mul_zero` `add_zero` `exp_approx_end`
`exp_approx_start` 📖	mathematical	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `expNear` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp`	—	`expNear_zero` `pow_zero` `Nat.cast_one` `div_self` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `one_mul`
`exp_approx_succ` 📖	mathematical	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `instAdd` `instOne` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `instNatCast` `exp` `expNear` `Monoid.toPow` `instMonoid` `Nat.factorial`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `expNear` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial`	—	`le_imp_le_of_le_of_le` `abs_sub_le` `instIsOrderedAddMonoid` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `expNear_succ` `expNear_sub` `abs_mul` `instIsOrderedRing` `pow_succ'` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one` `div_eq_mul_inv` `mul_inv_rev` `abs_pow` `abs_inv` `instIsStrictOrderedRing` `Nat.abs_cast` `mul_add` `Distrib.leftDistribClass` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `AddSemigroup.to_isAssociative` `AddCommMagma.to_isCommutative` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_sub_iff_add_le'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instZeroLEOneClass`
`exp_bound` 📖	mathematical	`Real` `instLE` `abs` `lattice` `instAddGroup` `instOne`	`Real` `instLE` `abs` `lattice` `instAddGroup` `instSub` `exp` `Finset.sum` `instAddCommMonoid` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial` `instMul`	—	`Nat.cast_one` `Complex.norm_real` `Finset.sum_congr` `Complex.exp_bound`
`exp_bound'` 📖	mathematical	`Real` `instLE` `instZero` `instOne`	`Real` `instLE` `exp` `instAdd` `Finset.sum` `instAddCommMonoid` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial` `instMul` `instOne`	—	`instIsOrderedAddMonoid` `exp_bound` `abs_sub_le_iff` `sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `mul_div_assoc` `Nat.cast_add` `Nat.cast_one`
`exp_bound_div_one_sub_of_interval` 📖	mathematical	`Real` `instLE` `instZero` `instLT` `instOne`	`Real` `instLE` `exp` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instSub`	—	`eq_or_lt_of_le` `exp_zero` `sub_zero` `div_self` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `instReflLe` `LT.lt.le` `exp_bound_div_one_sub_of_interval'`
`exp_bound_div_one_sub_of_interval'` 📖	mathematical	`Real` `instLT` `instZero` `instOne`	`Real` `instLT` `exp` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instSub`	—	`pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Nat.instAtLeastTwoHAddOfNat` `exp_bound'` `LT.lt.le` `zero_lt_three` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.sum_range_succ` `Mathlib.Meta.NormNum.instAtLeastTwo` `pow_zero` `div_self` `Mathlib.Meta.NormNum.isNat_eq_false` `IsStrictOrderedRing.toCharZero` `Nat.cast_zero` `zero_add` `pow_one` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsNat.raw_refl` `mul_one` `div_one` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_mul` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.CancelDenoms.add_subst` `Mathlib.Tactic.CancelDenoms.pow_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.one_natPow` `Mathlib.Tactic.CancelDenoms.div_subst` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Tactic.CancelDenoms.mul_subst` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `sq_nonneg` `IsOrderedRing.toPosMulMono` `le_of_lt` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `lt_of_not_ge`
`exp_eq_exp` 📖	mathematical	—	`exp`	—	`exp_injective`
`exp_eq_one_iff` 📖	mathematical	—	`exp` `Real` `instOne` `instZero`	—	`exp_injective` `exp_zero`
`exp_injective` 📖	mathematical	—	`Real` `exp`	—	`StrictMono.injective` `exp_strictMono`
`exp_le_exp` 📖	mathematical	—	`Real` `instLE` `exp`	—	`StrictMono.le_iff_le` `exp_strictMono`
`exp_le_exp_of_le` 📖	mathematical	`Real` `instLE`	`Real` `instLE` `exp`	—	`exp_monotone`
`exp_le_one_iff` 📖	mathematical	—	`Real` `instLE` `exp` `instOne` `instZero`	—	`exp_le_exp` `exp_zero`
`exp_list_sum` 📖	mathematical	—	`exp` `Real` `instAdd` `instZero` `instMul` `instOne`	—	`map_list_prod` `MonoidHom.instMonoidHomClass`
`exp_lt_exp` 📖	mathematical	—	`Real` `instLT` `exp`	—	`StrictMono.lt_iff_lt` `exp_strictMono`
`exp_lt_exp_of_lt` 📖	mathematical	`Real` `instLT`	`Real` `instLT` `exp`	—	`exp_strictMono`
`exp_lt_one_iff` 📖	mathematical	—	`Real` `instLT` `exp` `instOne` `instZero`	—	`exp_zero` `exp_lt_exp`
`exp_monotone` 📖	mathematical	—	`Monotone` `Real` `instPreorder` `exp`	—	`StrictMono.monotone` `exp_strictMono`
`exp_multiset_sum` 📖	mathematical	—	`exp` `Multiset.sum` `Real` `instAddCommMonoid` `Multiset.prod` `instCommMonoid` `Multiset.map`	—	`MonoidHom.map_multiset_prod`
`exp_nat_mul` 📖	mathematical	—	`exp` `Real` `instMul` `instNatCast` `Monoid.toPow` `instMonoid`	—	`Complex.ofReal_injective` `Complex.ofReal_exp` `Complex.ofReal_mul` `Complex.exp_nat_mul` `Complex.ofReal_pow`
`exp_ne_zero` 📖	—	—	—	—	`Complex.exp_ne_zero` `Complex.ofReal_exp_ofReal_re` `exp.eq_1`
`exp_neg` 📖	mathematical	—	`exp` `Real` `instNeg` `instInv`	—	`Complex.ofReal_injective` `Complex.ofReal_exp` `Complex.ofReal_neg` `Complex.exp_neg` `Complex.ofReal_inv`
`exp_nonneg` 📖	mathematical	—	`Real` `instLE` `instZero` `exp`	—	`LT.lt.le` `exp_pos`
`exp_nsmul` 📖	mathematical	—	`exp` `Real` `AddMonoid.toNSMul` `instAddMonoid` `Monoid.toPow` `instMonoid`	—	`MonoidHom.map_pow`
`exp_pos` 📖	mathematical	—	`Real` `instLT` `instZero` `exp`	—	`le_total` `lt_of_lt_of_le` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `one_le_exp` `neg_neg` `exp_neg` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `neg_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`exp_strictMono` 📖	mathematical	—	`StrictMono` `Real` `instPreorder` `exp`	—	`sub_add_cancel` `exp_add` `lt_mul_iff_one_lt_left` `IsStrictOrderedRing.toMulPosStrictMono` `instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `exp_pos` `lt_of_lt_of_le` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_neg`
`exp_sub` 📖	mathematical	—	`exp` `Real` `instSub` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`sub_eq_add_neg` `exp_add` `exp_neg` `div_eq_mul_inv`
`exp_sum` 📖	mathematical	—	`exp` `Finset.sum` `Real` `instAddCommMonoid` `Finset.prod` `instCommMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`exp_zero` 📖	mathematical	—	`exp` `Real` `instZero` `instOne`	—	`Complex.exp_zero`
`le_inv_mul_exp` 📖	mathematical	`Real` `instLT` `instZero`	`Real` `instLE` `instMul` `instInv` `exp`	—	`le_inv_mul_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `zero_le_one` `instZeroLEOneClass` `add_one_le_exp`
`norm_exp_sub_one_sub_id_le` 📖	mathematical	`Real` `instLE` `Norm.norm` `norm` `instOne`	`Real` `instLE` `Norm.norm` `norm` `instSub` `exp` `instOne` `Monoid.toPow` `instMonoid`	—	`Complex.norm_real` `Nat.cast_one` `Complex.ofReal_exp` `Complex.norm_exp_sub_one_sub_id_le` `sq_abs`
`one_le_exp` 📖	mathematical	`Real` `instLE` `instZero`	`Real` `instLE` `instOne` `exp`	—	`le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt`
`one_le_exp_iff` 📖	mathematical	—	`Real` `instLE` `instOne` `exp` `instZero`	—	`exp_le_exp` `exp_zero`
`one_lt_exp_iff` 📖	mathematical	—	`Real` `instLT` `instOne` `exp` `instZero`	—	`exp_zero` `exp_lt_exp`
`one_sub_div_pow_le_exp_neg` 📖	mathematical	`Real` `instLE` `instNatCast`	`Real` `instLE` `Monoid.toPow` `instMonoid` `instSub` `instOne` `DivInvMonoid.toDiv` `instDivInvMonoid` `instNatCast` `exp` `instNeg`	—	`eq_or_ne` `CharP.cast_eq_zero` `CharP.ofCharZero` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `div_zero` `sub_zero` `pow_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Nat.cast_zero` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `IsOrderedRing.toMulPosMono` `sub_nonneg` `covariant_swap_add_of_covariant_add` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `instZeroLEOneClass` `Nat.cast_nonneg` `one_sub_le_exp_neg` `exp_nat_mul` `mul_neg` `mul_comm` `div_mul_cancel₀` `ne_of_gt` `Nat.cast_pos'` `NeZero.charZero_one` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd`
`one_sub_le_exp_neg` 📖	mathematical	—	`Real` `instLE` `instSub` `instOne` `exp` `instNeg`	—	`Eq.trans_le` `sub_eq_neg_add` `add_one_le_exp`
`one_sub_lt_exp_neg` 📖	mathematical	—	`Real` `instLT` `instSub` `instOne` `exp` `instNeg`	—	`Eq.trans_lt` `sub_eq_neg_add` `add_one_lt_exp` `neg_ne_zero`
`pow_div_factorial_le_exp` 📖	mathematical	`Real` `instLE` `instZero`	`Real` `instLE` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial` `exp`	—	`Finset.single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `IsOrderedRing.toPosMulMono` `Nat.cast_pos'` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Nat.factorial_pos` `Finset.self_mem_range_succ` `sum_le_exp_of_nonneg`
`prod_one_add_le_exp_sum` 📖	mathematical	`Real` `instLE` `instZero`	`Real` `instLE` `Finset.prod` `instCommMonoid` `instAdd` `instOne` `exp` `Finset.sum` `instAddCommMonoid`	—	`LE.le.trans` `Finset.prod_le_prod` `instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `zero_le_one` `Eq.le` `add_comm` `add_one_le_exp` `exp_sum`
`quadratic_le_exp_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`Real` `instLE` `instAdd` `instOne` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `exp`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_range_succ` `Finset.sum_singleton` `pow_zero` `Nat.cast_succ` `pow_one` `mul_one` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `Mathlib.Tactic.RingNF.nnrat_rawCast` `add_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isNat_add` `sum_le_exp_of_nonneg`
`sum_le_exp_of_nonneg` 📖	mathematical	`Real` `instLE` `instZero`	`Real` `instLE` `Finset.sum` `instAddCommMonoid` `Finset.range` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toPow` `instMonoid` `instNatCast` `Nat.factorial` `exp`	—	`instIsStrictOrderedRing` `IsAbsoluteValue.abs_isAbsoluteValue` `instIsCompleteAbs` `Complex.isCauSeq_re` `CauSeq.le_lim` `CauSeq.le_of_exists` `Complex.re_sum` `Finset.sum_congr` `Finset.sum_le_sum_of_subset_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Finset.range_mono` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `IsOrderedRing.toPosMulMono` `Nat.cast_pos'` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Nat.factorial_pos` `exp.eq_1` `Complex.isAbsoluteValueNorm` `Complex.instIsComplete` `Complex.exp_def` `Complex.cauSeqRe.eq_1` `Complex.lim_re`

---

← Back to Index