Deriv

📁 Source: Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean

Statistics

Metric	Count
Definitions	0
Theorems strictConvexOn_pow, prod_nonneg_of_card_nonpos_even, deriv2_sqrt_mul_log, deriv_sqrt_mul_log, deriv_sqrt_mul_log', hasDerivAt_sqrt_mul_log, int_prod_range_nonneg, int_prod_range_pos, strictConcaveOn_cos_Icc, strictConcaveOn_sin_Icc, strictConcaveOn_sqrt_mul_log_Ioi, strictConvexOn_pow, strictConvexOn_zpow	13
Total	13

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvexOn_pow 📖	mathematical	Even	StrictConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ Monoid.toNatPow Real.instMonoid	—	StrictMono.strictConvexOn_univ_of_deriv continuous_pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal deriv_pow_field StrictMono.const_mul IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Odd.strictMono_pow AddGroup.existsAddOfLE Nat.Even.sub_odd Nat.odd_iff Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_nonneg_of_card_nonpos_even 📖	mathematical	Even card filter Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	prod CommRing.toCommMonoid	—	prod_nonneg IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing neg_mul one_mul IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid 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.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.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.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt lt_of_not_ge prod_mul_distrib prod_ite prod_const_one mul_one prod_const neg_one_pow_eq_pow_mod_two Nat.even_iff pow_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv2_sqrt_mul_log 📖	mathematical	—	Nat.iterate deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat deriv_sqrt_mul_log' le_or_gt Real.sqrt_eq_zero_of_nonpos zero_pow three_ne_zero MulZeroClass.mul_zero div_zero HasDerivWithinAt.deriv_eq_zero HasDerivWithinAt.congr_of_mem hasDerivWithinAt_const uniqueDiffOn_Iic Real.sqrt_ne_zero' Real.mul_self_sqrt LT.lt.le 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.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul mul_neg 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.zpow'_ofNat Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.mul_pf_left Mathlib.Tactic.Ring.one_mul 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.Tactic.Ring.sub_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.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_pf_right HasDerivAt.deriv HasDerivAt.div HasDerivAt.const_add Real.hasDerivAt_log LT.lt.ne' HasDerivAt.const_mul Real.hasDerivAt_sqrt mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass two_ne_zero CharZero.NeZero.two
deriv_sqrt_mul_log 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat lt_or_ge HasDerivAt.deriv hasDerivAt_sqrt_mul_log LT.lt.ne' Real.sqrt_eq_zero_of_nonpos MulZeroClass.mul_zero div_zero HasDerivWithinAt.deriv_eq_zero HasDerivWithinAt.congr_of_mem hasDerivWithinAt_const MulZeroClass.zero_mul uniqueDiffOn_Iic
deriv_sqrt_mul_log' 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat deriv_sqrt_mul_log
hasDerivAt_sqrt_mul_log 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.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 Real.instMul Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul add_div div_mul_cancel_left₀ two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike div_eq_mul_inv Real.sqrt_div_self' add_comm one_div div_eq_inv_mul HasDerivAt.mul Real.hasDerivAt_sqrt Real.hasDerivAt_log
int_prod_range_nonneg 📖	mathematical	Even	Finset.prod Int.instCommMonoid Finset.range	—	Finset.prod_congr add_zero Int.instZeroLEOneClass Nat.instAtLeastTwoHAddOfNat two_mul mul_add Distrib.leftDistribClass mul_one one_add_one_eq_two add_assoc Finset.prod_range_succ mul_assoc mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing le_or_gt LE.le.trans LT.lt.le lt_add_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le sub_nonpos_of_le sub_nonneg_of_le
int_prod_range_pos 📖	mathematical	Even Set Set.instMembership Set.Ico PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder	Finset.prod Int.instCommMonoid Finset.range	—	LE.le.lt_of_ne int_prod_range_nonneg Finset.prod_eq_zero_iff Int.instNontrivial NormMulClass.toNoZeroDivisors Int.instNormMulClass sub_eq_zero Finset.mem_range
strictConcaveOn_cos_Icc 📖	mathematical	—	StrictConcaveOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc Real.instPreorder Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cos	—	strictConcaveOn_of_deriv2_neg Nat.instAtLeastTwoHAddOfNat convex_Icc Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Real.continuousOn_cos Function.iterate_one Real.deriv_cos' deriv.fun_neg' Real.deriv_sin IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.cos_pos_of_mem_Ioo interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMaxOrderOfNontrivial
strictConcaveOn_sin_Icc 📖	mathematical	—	StrictConcaveOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc Real.instPreorder Real.instZero Real.pi Real.sin	—	strictConcaveOn_of_deriv2_neg convex_Icc Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Real.continuousOn_sin Function.iterate_one Real.deriv_sin Real.deriv_cos' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.sin_pos_of_mem_Ioo interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMaxOrderOfNontrivial
strictConcaveOn_sqrt_mul_log_Ioi 📖	mathematical	—	StrictConcaveOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instOne Real.instMul Real.sqrt Real.log	—	strictConcaveOn_of_deriv2_neg' convex_Ioi Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing ContinuousOn.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.continuousOn Real.continuous_sqrt ContinuousOn.mono Real.continuousOn_log ne_of_gt LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat deriv2_sqrt_mul_log div_neg_of_neg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono neg_neg_of_pos Real.instIsOrderedAddMonoid Real.log_pos mul_pos four_pos IsOrderedAddMonoid.toAddLeftMono pow_pos Real.sqrt_pos
strictConvexOn_pow 📖	mathematical	—	StrictConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero Monoid.toNatPow Real.instMonoid	—	StrictMonoOn.strictConvexOn_of_deriv convex_Ici Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing continuousOn_pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal deriv_pow_field interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial mul_lt_mul_of_pos_left pow_lt_pow_left₀ IsOrderedRing.toMulPosMono LT.lt.le Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
strictConvexOn_zpow 📖	mathematical	—	StrictConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero DivInvMonoid.toZPow Real.instDivInvMonoid	—	strictConvexOn_of_deriv2_pos' convex_Ioi Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing ContinuousOn.mono continuousOn_zpow₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ne_of_gt iter_deriv_zpow mul_pos IsStrictOrderedRing.toPosMulStrictMono Nat.cast_zero Finset.prod_congr Int.cast_natCast Int.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike int_prod_range_pos Int.instCharZero Nat.instAtLeastTwoHAddOfNat Finset.coe_Ico CharP.cast_eq_zero CharP.ofCharZero add_zero Nat.cast_one zero_add zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Set.mem_Ioi

---

← Back to Index