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, quadratic_le_exp_of_nonneg, sum_le_exp_of_nonneg	83
Total	92

Complex

Definitions

Name	Category	Theorems
exp 📖	CompOp	342 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', 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, 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, 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, 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, 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.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, 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, 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, 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	instSub exp Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow 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	instSub exp Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Finset.range instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instNatCast Nat.factorial Real.instMul Real.instMonoid	—	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 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 CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul CancelDenoms.sub_subst 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 CancelDenoms.neg_subst 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add 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.toNatPow 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.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne addGroupWithOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	MonoidHom.map_pow
exp_nsmul' 📖	mathematical	—	exp Complex DivInvMonoid.toDiv instDivInvMonoid instMul instNatCast Monoid.toNatPow 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.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add 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.toNatPow 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.toNatPow 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	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	instSub exp instOne Monoid.toNatPow 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.toNatPow 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.toNatPow 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd 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	462 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, 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, 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, MeasureTheory.integral_tilted, exp_eq_exp, tendsto_exp_atTop, integrableOn_exp_Iic, ProbabilityTheory.cdf_expMeasure_eq, Function.Periodic.norm_qParam_lt_iff, 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, 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, comap_exp_nhds_exp, tendsto_exp_neg_atTop_nhds_zero, 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', 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, 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.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, isLittleO_pow_exp_atTop, two_mul_le_exp, exp_one_near_20, 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, 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, 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, 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, ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self', deriv_exp, exp_log, HurwitzZeta.isBigO_atTop_oddKernel, iter_deriv_exp, continuousOn_exp, log_div_self_antitoneOn, Polynomial.deriv_gaussian_eq_hermite_mul_gaussian, integrable_rpow_mul_exp_neg_mul_sq, integral_exp_neg_rpow, integrable_mul_exp_neg_mul_sq, 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, log_div_sqrt_antitoneOn, mellin_eq_fourierIntegral, cosh_add_sinh, isLittleO_exp_comp_exp_comp, 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, 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.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, ProbabilityTheory.exponentialCDFReal_eq, Gamma_eq_integral, MeasureTheory.rnDeriv_tilted_left, 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, 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_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, exp_lt_exp, ProbabilityTheory.HasSubgaussianMGF.measure_ge_le, ProbabilityTheory.rpow_abs_le_mul_max_exp, 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, tendsto_mul_exp_add_div_pow_atTop, tendsto_div_pow_mul_exp_add_atTop, ProbabilityTheory.setIntegral_tilted_mul_eq_mgf, ProbabilityTheory.mgf_dirac', 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, 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.integrable_exp_mul_of_le, exp_bound', integral_rpow_mul_exp_neg_mul_Ioi, sinh_add_cosh, ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul, log_comp_exp, 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, 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, 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, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, DifferentiableOn.exp, rpow_def_of_nonpos, exp_sub, 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, 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, exp_neg, MeasureTheory.rnDeriv_tilted_left_self, MeasureTheory.measure_unitBall_eq_integral_div_gamma, exp_neg_one_lt_half, log_div_self_rpow_antitoneOn, 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, ModularFormClass.exp_decay_sub_atImInfty', tendsto_exp_mul_div_rpow_atTop, tendsto_exp_atBot_nhdsGT, hasStrictDerivAt_exp, dist_le_of_trajectories_ODE_of_mem, summable_exp_nat_mul_iff, Complex.exp_im, mul_exp_neg_le_exp_neg_one, ProbabilityTheory.mgf_pos_iff, HasStrictFDerivAt.exp, exp_neg_one_lt_d9, isLittleO_one_exp_comp, 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, 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	5 math math: expNear_succ, expNear_zero, expNear_sub, exp_approx_end, exp_approx_end'
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	instSub exp 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	instSub exp Monoid.toNatPow 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 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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.toNatPow 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 📖	—	Real instNatCast instLE abs lattice instAddGroup instSub exp instOne expNear instMul DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid 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
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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le abs_of_nonneg IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd
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	instSub exp expNear instZero instMul DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instNatCast Nat.factorial instAdd	—	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	exp expNear Monoid.toNatPow instMonoid Nat.factorial	—	exp_approx_succ MulZeroClass.mul_zero add_zero exp_approx_end
exp_approx_start 📖	—	Real instLE abs lattice instAddGroup instSub exp expNear instMul DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instNatCast Nat.factorial	—	—	expNear_zero pow_zero Nat.cast_one div_self NeZero.charZero_one IsStrictOrderedRing.toCharZero instIsStrictOrderedRing one_mul
exp_approx_succ 📖	—	Real instLE abs lattice instAddGroup instSub instAdd instOne instMul DivInvMonoid.toDiv instDivInvMonoid instNatCast exp expNear Monoid.toNatPow instMonoid 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 AddRightCancelSemigroup.toIsRightCancelAdd 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	instSub exp Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instNatCast Nat.factorial instMul	—	Nat.cast_one Complex.norm_real Finset.sum_congr Complex.exp_bound
exp_bound' 📖	mathematical	Real instLE instZero instOne	exp instAdd Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instNatCast Nat.factorial instMul	—	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	exp DivInvMonoid.toDiv instDivInvMonoid instSub	—	eq_or_lt_of_le exp_zero sub_zero div_self NeZero.charZero_one IsStrictOrderedRing.toCharZero instIsStrictOrderedRing LT.lt.le exp_bound_div_one_sub_of_interval'
exp_bound_div_one_sub_of_interval' 📖	mathematical	Real instLT instZero instOne	exp DivInvMonoid.toDiv instDivInvMonoid 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 CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow 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 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add 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	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	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.toNatPow 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.toNatSMul instAddMonoid Monoid.toNatPow 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	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	instSub exp Monoid.toNatPow 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	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	Monoid.toNatPow instMonoid instSub instOne DivInvMonoid.toDiv instDivInvMonoid 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	DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow 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
quadratic_le_exp_of_nonneg 📖	mathematical	Real instLE instZero	instAdd instOne DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow 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.nat_rawCast_1 Mathlib.Tactic.RingNF.nnrat_rawCast add_zero Mathlib.Tactic.RingNF.add_assoc_rev 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	Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow 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