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	Real instLE abs lattice instAddGroup instAdd Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toPow instMonoid instNatCast instOne 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid 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 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 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring 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 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 instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instSub DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instAdd Finset.sum instAddCommMonoid Finset.range Monoid.toPow 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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 instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring 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 instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid hasStrictDerivAt_neg
hasStrictDerivAt_log_of_pos 📖	mathematical	Real instLT instZero	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 instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring 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 Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instOne instAdd Monoid.toPow 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 Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instOne instAdd Monoid.toPow 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 Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instOne instAdd Monoid.toPow 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.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.add_assoc_rev add_zero 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing
hasSum_pow_div_log_of_abs_lt_one 📖	mathematical	Real instLT abs lattice instAddGroup instOne	HasSum Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid Monoid.toPow instMonoid instAdd instNatCast instOne 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 IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring 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	Real instLE 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	Real instLE instMul DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instAdd instSub Finset.sum instAddCommMonoid Finset.range Monoid.toPow 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	Real instLT 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le 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	Real instLE Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toPow instMonoid instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne 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	Real instLE abs lattice instAddGroup instSub instMul DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instAdd Finset.sum instAddCommMonoid Finset.range Monoid.toPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Set.Icc_subset_Ioo IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le 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 instReflLe 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