Deriv

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_log_sub_add_sum_range_le, contDiffAt_log, contDiffOn_log, deriv_log, deriv_log', deriv_log_comp_eq_logDeriv, differentiableAt_log, differentiableAt_log_iff, differentiableOn_log, hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range, hasDerivAt_log, hasStrictDerivAt_log, hasStrictDerivAt_log_of_pos, hasSum_log_one_add, hasSum_log_one_add_inv, hasSum_log_sub_log_of_abs_lt_one, hasSum_pow_div_log_of_abs_lt_one, le_log_one_add_of_nonneg, log_div_le_sum_range_add, lt_log_one_add_of_pos, sum_range_le_log_div, sum_range_sub_log_div_le	22
Total	22

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_log_sub_add_sum_range_le 📖	mathematical	Real instLT abs lattice instAddGroup instOne	instLE instAdd Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instNatCast log instSub	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.add HasDerivAt.fun_sum HasDerivAt.div_const hasDerivAt_pow HasDerivAt.log HasDerivAt.const_sub hasDerivAt_id sub_ne_zero LT.lt.ne' geom_sum_eq LT.lt.ne Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub 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.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.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval mul_neg Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial neg_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval sub_add_cancel Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right 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 Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_gt Mathlib.Tactic.Ring.neg_mul 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 Nat.cast_succ mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass Nat.cast_add_one_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike abs_div instIsStrictOrderedRing abs_neg abs_pow instIsOrderedRing abs_le le_trans le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.add_congr 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_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le le_abs_self div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_nonneg IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono abs_nonneg covariant_swap_add_of_covariant_add pow_le_pow_left₀ IsOrderedRing.toMulPosMono sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Convex.norm_image_sub_le_of_norm_hasDerivWithin_le HasDerivAt.hasDerivWithinAt Set.Icc_subset_Ioo neg_lt_neg convex_Icc IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule neg_le neg_le_abs Finset.sum_congr pow_succ MulZeroClass.mul_zero zero_div Finset.sum_const_zero sub_zero log_one add_zero div_mul_eq_mul_div
contDiffAt_log 📖	mathematical	—	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField log	—	continuousAt_log_iff ContDiffAt.continuousAt OpenPartialHomeomorph.contDiffAt_symm_deriv instCompleteSpace LT.lt.ne' ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instIsTopologicalRingReal exp_log hasDerivAt_exp AnalyticAt.contDiffAt analyticAt_rexp Ne.lt_or_gt ContDiffAt.comp Left.neg_pos_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid ContDiffAt.neg contDiffAt_id log_neg_eq_log
contDiffOn_log 📖	mathematical	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField log Compl.compl Set Set.instCompl Set.instSingletonSet instZero	—	ContDiffAt.contDiffWithinAt contDiffAt_log
deriv_log 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log instInv	—	deriv_zero_of_not_differentiableAt Iff.not_left differentiableAt_log_iff inv_zero HasDerivAt.deriv hasDerivAt_log
deriv_log' 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log instInv	—	deriv_log
deriv_log_comp_eq_logDeriv 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	deriv log logDeriv RCLike.toNormedAlgebra instRCLike	—	deriv.log
differentiableAt_log 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log	—	HasDerivAt.differentiableAt hasDerivAt_log
differentiableAt_log_iff 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log	—	continuousAt_log_iff DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul differentiableAt_log
differentiableOn_log 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log Compl.compl Set Set.instCompl Set.instSingletonSet instZero	—	DifferentiableAt.differentiableWithinAt differentiableAt_log
hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range 📖	mathematical	Real instLT instNeg instOne	HasDerivAt DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal instSub instMul DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instAdd Finset.sum instAddCommMonoid Finset.range Monoid.toNatPow instMonoid	—	HasDerivAt.congr_deriv Nat.instAtLeastTwoHAddOfNat HasDerivAt.sub HasDerivAt.const_mul HasDerivAt.log HasDerivAt.div HasDerivAt.const_add hasDerivAt_id HasDerivAt.const_sub HasDerivAt.fun_sum HasDerivAt.div_const hasDerivAt_pow mul_comm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one 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 div_one 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.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing Nat.cast_nonneg' instZeroLEOneClass le_of_lt Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one one_ne_zero NeZero.one GroupWithZero.toNontrivial NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne LT.lt.ne' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos 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_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.zero_mul 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 Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero one_div mul_neg neg_add_rev Finset.sum_congr Nat.cast_add Nat.cast_mul add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instIsOrderedAddMonoid geom_sum_eq Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg 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.zpow'_ofNat Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap
hasDerivAt_log 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal log instInv	—	HasStrictDerivAt.hasDerivAt hasStrictDerivAt_log
hasStrictDerivAt_log 📖	mathematical	—	HasStrictDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal log instInv	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Ne.lt_or_gt IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul log_neg_eq_log Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_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 RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_inv_neg Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul HasStrictDerivAt.comp hasStrictDerivAt_log_of_pos neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid hasStrictDerivAt_neg
hasStrictDerivAt_log_of_pos 📖	mathematical	Real instLT instZero	HasStrictDerivAt DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal log instInv	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasStrictDerivAt.of_local_left_inverse continuousAt_log LT.lt.ne' hasStrictDerivAt_exp ne_of_gt exp_pos Filter.Eventually.mono lt_mem_nhds instOrderTopologyReal exp_log
hasSum_log_one_add 📖	mathematical	Real instLE instZero	HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instOne instAdd Monoid.toNatPow instMonoid log SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne one_div zero_add zero_div zero_pow IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.instCharZero MulZeroClass.mul_zero add_zero log_one add_comm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval 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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_of_le_of_ne' Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo one_ne_zero NeZero.one GroupWithZero.toNontrivial inv_inv hasSum_log_one_add_inv inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing lt_of_le_of_ne
hasSum_log_one_add_inv 📖	mathematical	Real instLT instZero	HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instOne instAdd Monoid.toNatPow instMonoid log instInv SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat abs_of_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing one_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl 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.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt 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 Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_nonpos_of_le div_lt_one Mathlib.Tactic.Linarith.lt_of_lt_of_eq sub_eq_zero_of_eq LT.lt.ne' log_div Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' ne_of_gt add_pos' mul_pos Mathlib.Meta.Positivity.pos_of_isNat instNontrivial one_div Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial add_sub_cancel_right MulZeroClass.mul_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add hasSum_log_sub_log_of_abs_lt_one
hasSum_log_sub_log_of_abs_lt_one 📖	mathematical	Real instLT abs lattice instAddGroup instOne	HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instAdd Monoid.toNatPow instMonoid instSub log SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Odd.neg_pow Nat.cast_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_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.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast 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.mul_pf_left Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one add_zero Mathlib.Tactic.RingNF.mul_assoc_rev Function.Injective.hasSum_iff mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero two_ne_zero' Even.neg_pow Nat.even_add_one Set.mem_setOf_eq range_two_mul neg_one_mul neg_add_cancel HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal hasSum_pow_div_log_of_abs_lt_one Eq.trans_lt abs_neg Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg HasSum.add IsTopologicalSemiring.toContinuousAdd
hasSum_pow_div_log_of_abs_lt_one 📖	mathematical	Real instLT abs lattice instAddGroup instOne	HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instAdd instNatCast instNeg log instSub SummationFilter.unconditional	—	Summable.hasSum_iff_tendsto_nat TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Summable.of_norm_bounded instCompleteSpace summable_geometric_of_lt_one abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_of_lt Nat.cast_add_one_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike norm_eq_abs abs_div instIsStrictOrderedRing pow_abs instIsOrderedRing abs_of_nonneg div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_nonneg IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono le_refl Right.add_pos_of_nonneg_of_pos Mathlib.Meta.Positivity.nonneg_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Nat.cast_one add_le_add_left Nat.cast_nonneg pow_succ zero_add div_one mul_le_of_le_one_right tendsto_iff_norm_sub_tendsto_zero sub_neg_eq_add squeeze_zero abs_log_sub_add_sum_range_le pow_succ' Filter.Tendsto.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.mul tendsto_const_nhds tendsto_pow_atTop_nhds_zero_of_lt_one AddGroup.existsAddOfLE instArchimedean instOrderTopologyReal MulZeroClass.mul_zero zero_div
le_log_one_add_of_nonneg 📖	mathematical	Real instLE instZero	DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd log instOne	—	Nat.instAtLeastTwoHAddOfNat CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike MulZeroClass.mul_zero zero_add div_self NeZero.charZero_one mul_one pow_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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ 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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval 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 Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_eq_false Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial le_hasSum HasSolidNorm.orderClosedTopology instHasSolidNormReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional hasSum_log_one_add mul_nonneg IsOrderedRing.toPosMulMono le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Nat.cast_one add_pos' Nat.cast_pos' instZeroLEOneClass lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd pow_nonneg IsOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos
log_div_le_sum_range_add 📖	mathematical	Real instLE instZero instLT instOne	instMul DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instAdd instSub Finset.sum instAddCommMonoid Finset.range Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat sum_range_sub_log_div_le abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sub_le_iff_le_add' sub_nonneg_of_le covariant_swap_add_of_covariant_add sum_range_le_log_div
lt_log_one_add_of_pos 📖	mathematical	Real instLT instZero	DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instAdd log instOne	—	Nat.instAtLeastTwoHAddOfNat CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike MulZeroClass.mul_zero zero_add div_self NeZero.charZero_one mul_one pow_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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ 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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_eq_false Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial lt_hasSum HasSolidNorm.orderClosedTopology instHasSolidNormReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add hasSum_log_one_add LT.lt.le le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Nat.cast_one Nat.cast_pos' instZeroLEOneClass lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd pow_pos IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial
sum_range_le_log_div 📖	mathematical	Real instLE instZero instLT instOne	Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instSub	—	Nat.instAtLeastTwoHAddOfNat ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range monotoneOn_of_hasDerivWithinAt_nonneg convex_Icc instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing ContinuousAt.continuousWithinAt HasDerivAt.continuousAt HasDerivAt.hasDerivWithinAt interior_subset covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono abs_of_nonneg LT.lt.le sub_le_sub_left pow_le_pow_left₀ IsOrderedRing.toPosMulMono instIsOrderedRing IsOrderedRing.toMulPosMono interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial instNontrivial instNoMaxOrderOfNontrivial div_nonneg pow_nonneg IsOrderedRing.toZeroLEOneClass Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul one_div add_zero sub_zero div_self NeZero.charZero_one RCLike.charZero_rclike log_one MulZeroClass.mul_zero Finset.sum_congr zero_pow IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.instCharZero zero_div Finset.sum_const_zero sub_self le_rfl
sum_range_sub_log_div_le 📖	mathematical	Real instLT abs lattice instAddGroup instOne	instLE instSub instMul DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instAdd Finset.sum instAddCommMonoid Finset.range Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Set.Icc_subset_Ioo IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range sq_le_sq instIsStrictOrderedRing abs_le norm_div norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass sq_abs abs_of_pos div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_nonneg IsOrderedRing.toZeroLEOneClass instIsOrderedRing IsOrderedRing.toPosMulMono Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul pow_le_pow_left₀ IsOrderedRing.toMulPosMono sub_le_sub_left pow_mul Convex.norm_image_sub_le_of_norm_hasDerivWithin_le HasDerivAt.hasDerivWithinAt convex_Icc IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule neg_le_abs one_div Finset.sum_congr pow_succ pow_zero one_mul add_zero sub_zero div_self NeZero.charZero_one RCLike.charZero_rclike log_one MulZeroClass.mul_zero zero_div Finset.sum_const_zero sub_self div_mul_eq_mul_div

---

← Back to Index