NegMulLog

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

Statistics

Metric	Count
Definitions `negMulLog`	1
Theorems `mul_log`, `concaveOn_negMulLog`, `continuous_mul_log`, `continuous_negMulLog`, `convexOn_mul_log`, `deriv2_mul_log`, `deriv2_negMulLog`, `deriv_mul_log`, `deriv_mul_log_zero`, `deriv_negMulLog`, `differentiableAt_negMulLog`, `differentiableAt_negMulLog_iff`, `differentiableOn_mul_log`, `differentiableOn_negMulLog`, `hasDerivAt_mul_log`, `hasDerivAt_negMulLog`, `leftDeriv_mul_log`, `mul_log_nonneg`, `mul_log_nonpos`, `negMulLog_def`, `negMulLog_eq_neg`, `negMulLog_mul`, `negMulLog_nonneg`, `negMulLog_one`, `negMulLog_zero`, `not_DifferentiableAt_log_mul_zero`, `not_continuousAt_deriv_mul_log_zero`, `rightDeriv_mul_log`, `strictConcaveOn_negMulLog`, `strictConvexOn_mul_log`, `tendsto_deriv_mul_log_atTop`, `tendsto_rightDeriv_mul_log_atTop`	32
Total	33

Real

Definitions

Name	Category	Theorems
`negMulLog` 📖	CompOp	17 math math: `deriv_negMulLog`, `negMulLog_mul`, `continuous_negMulLog`, `negMulLog_nonneg`, `concaveOn_negMulLog`, `differentiableOn_negMulLog`, `binEntropy_eq_negMulLog_add_negMulLog_one_sub'`, `negMulLog_one`, `negMulLog_eq_neg`, `negMulLog_def`, `differentiableAt_negMulLog`, `negMulLog_zero`, `strictConcaveOn_negMulLog`, `binEntropy_eq_negMulLog_add_negMulLog_one_sub`, `deriv2_negMulLog`, `differentiableAt_negMulLog_iff`, `hasDerivAt_negMulLog`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`concaveOn_negMulLog` 📖	mathematical	—	`ConcaveOn` `Real` `semiring` `partialOrder` `instAddCommMonoid` `Algebra.toSMul` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Ici` `instPreorder` `instZero` `negMulLog`	—	`StrictConcaveOn.concaveOn` `strictConcaveOn_negMulLog`
`continuous_mul_log` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul` `log`	—	`continuous_iff_continuousAt` `ne_or_eq` `ContinuousAt.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.continuousAt` `continuous_id'` `continuousAt_log` `ContinuousAt.eq_1` `MulZeroClass.zero_mul` `mul_comm` `nhdsWithin_univ` `Set.ext` `Set.Iio_union_Ioi` `Set.union_singleton` `nhdsWithin_union` `nhdsWithin_singleton` `tendsto_log_mul_self_nhdsLT_zero` `rpow_one` `tendsto_log_mul_rpow_nhdsGT_zero` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `log_zero` `MulZeroClass.mul_zero` `tendsto_pure_nhds`
`continuous_negMulLog` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `negMulLog`	—	`negMulLog_eq_neg` `Continuous.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `continuous_mul_log`
`convexOn_mul_log` 📖	mathematical	—	`ConvexOn` `Real` `semiring` `partialOrder` `instAddCommMonoid` `Algebra.toSMul` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Ici` `instPreorder` `instZero` `instMul` `log`	—	`StrictConvexOn.convexOn` `strictConvexOn_mul_log`
`deriv2_mul_log` 📖	mathematical	—	`Nat.iterate` `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` `instMul` `log` `instInv`	—	`inv_zero` `deriv_zero_of_not_differentiableAt` `not_continuousAt_deriv_mul_log_zero` `DifferentiableAt.continuousAt` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `Filter.mp_mem` `eventually_ne_nhds` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal` `Filter.univ_mem'` `deriv_mul_log` `Filter.EventuallyEq.deriv_eq` `deriv_add_const` `deriv_log`
`deriv2_negMulLog` 📖	mathematical	—	`Nat.iterate` `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` `negMulLog` `instNeg` `instInv`	—	`negMulLog_eq_neg` `deriv2_mul_log` `deriv.fun_neg'`
`deriv_mul_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` `instMul` `log` `instAdd` `instOne`	—	`deriv_fun_mul` `deriv_id''` `one_mul` `deriv_log'` `mul_inv_cancel₀`
`deriv_mul_log_zero` 📖	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` `instMul` `log` `instZero`	—	`deriv_zero_of_not_differentiableAt` `not_DifferentiableAt_log_mul_zero`
`deriv_negMulLog` 📖	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` `negMulLog` `instSub` `instNeg` `log` `instOne`	—	`negMulLog_eq_neg` `deriv.fun_neg` `deriv_mul_log` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_mul` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf`
`differentiableAt_negMulLog` 📖	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` `negMulLog`	—	`differentiableAt_negMulLog_iff`
`differentiableAt_negMulLog_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` `negMulLog`	—	`not_DifferentiableAt_log_mul_zero` `neg_mul` `differentiableOn_negMulLog` `DifferentiableWithinAt.differentiableAt` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal`
`differentiableOn_mul_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` `instMul` `log` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `instZero`	—	`DifferentiableOn.mul` `Differentiable.differentiableOn` `differentiable_id` `differentiableOn_log`
`differentiableOn_negMulLog` 📖	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` `negMulLog` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `instZero`	—	`negMulLog_eq_neg` `DifferentiableOn.neg` `differentiableOn_mul_log`
`hasDerivAt_mul_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` `instMul` `log` `instAdd` `instOne`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `deriv_mul_log` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `hasDerivAt_deriv_iff` `DifferentiableOn.differentiableAt` `differentiableOn_mul_log` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal`
`hasDerivAt_negMulLog` 📖	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` `negMulLog` `instSub` `instNeg` `log` `instOne`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `deriv_negMulLog` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `hasDerivAt_deriv_iff` `DifferentiableOn.differentiableAt` `differentiableOn_negMulLog` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal`
`leftDeriv_mul_log` 📖	mathematical	—	`derivWithin` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul` `log` `Set.Iio` `instPreorder` `instAdd` `instOne`	—	`HasDerivWithinAt.derivWithin` `HasDerivAt.hasDerivWithinAt` `hasDerivAt_mul_log` `uniqueDiffWithinAt_Iio`
`mul_log_nonneg` 📖	mathematical	`Real` `instLE` `instOne`	`instZero` `instMul` `log`	—	`mul_nonneg` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `LE.le.trans` `zero_le_one` `instZeroLEOneClass` `log_nonneg`
`mul_log_nonpos` 📖	mathematical	`Real` `instLE` `instZero` `instOne`	`instMul` `log`	—	`mul_nonpos_of_nonneg_of_nonpos` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `log_nonpos`
`negMulLog_def` 📖	mathematical	—	`negMulLog` `Real` `instMul` `instNeg` `log`	—	—
`negMulLog_eq_neg` 📖	mathematical	—	`negMulLog` `Real` `instNeg` `instMul` `log`	—	`neg_mul`
`negMulLog_mul` 📖	mathematical	—	`negMulLog` `Real` `instMul` `instAdd`	—	`neg_mul` `MulZeroClass.zero_mul` `log_zero` `MulZeroClass.mul_zero` `neg_zero` `mul_neg` `add_zero` `log_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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`
`negMulLog_nonneg` 📖	mathematical	`Real` `instLE` `instZero` `instOne`	`negMulLog`	—	`negMulLog_eq_neg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `mul_log_nonpos`
`negMulLog_one` 📖	mathematical	—	`negMulLog` `Real` `instOne` `instZero`	—	`log_one` `MulZeroClass.mul_zero`
`negMulLog_zero` 📖	mathematical	—	`negMulLog` `Real` `instZero`	—	`neg_zero` `log_zero` `MulZeroClass.mul_zero`
`not_DifferentiableAt_log_mul_zero` 📖	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` `instMul` `log` `instZero`	—	`not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi` `DifferentiableAt.differentiableWithinAt`
`not_continuousAt_deriv_mul_log_zero` 📖	mathematical	—	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `deriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `instMul` `log` `instZero`	—	`not_continuousAt_of_tendsto` `nhdsGT_neBot` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `instIsOrderedRing` `instNontrivial` `nhdsWithin_le_nhds` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `instNoBotOrderOfNoMinOrder` `instNoMinOrderOfNontrivial`
`rightDeriv_mul_log` 📖	mathematical	—	`derivWithin` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul` `log` `Set.Ioi` `instPreorder` `instAdd` `instOne`	—	`HasDerivWithinAt.derivWithin` `HasDerivAt.hasDerivWithinAt` `hasDerivAt_mul_log` `uniqueDiffWithinAt_Ioi`
`strictConcaveOn_negMulLog` 📖	mathematical	—	`StrictConcaveOn` `Real` `semiring` `partialOrder` `instAddCommMonoid` `Algebra.toSMul` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Ici` `instPreorder` `instZero` `negMulLog`	—	`negMulLog_eq_neg` `StrictConvexOn.neg` `instIsOrderedAddMonoid` `strictConvexOn_mul_log`
`strictConvexOn_mul_log` 📖	mathematical	—	`StrictConvexOn` `Real` `semiring` `partialOrder` `instAddCommMonoid` `Algebra.toSMul` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Ici` `instPreorder` `instZero` `instMul` `log`	—	`strictConvexOn_of_deriv2_pos` `convex_Ici` `instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instIsStrictOrderedRing` `Continuous.continuousOn` `continuous_mul_log` `deriv2_mul_log` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `interior_Ici'` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `instNoMinOrderOfNontrivial` `instIsOrderedRing` `instNontrivial`
`tendsto_deriv_mul_log_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `deriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul` `log` `Filter.atTop` `instPreorder`	—	`Filter.tendsto_congr'` `Filter.EventuallyEq.eq_1` `Filter.eventually_atTop` `instIsDirectedOrder` `instIsOrderedRing` `instArchimedean` `deriv_mul_log` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Filter.Tendsto.atTop_add` `instIsOrderedAddMonoid` `instOrderTopologyReal` `tendsto_log_atTop` `tendsto_const_nhds`
`tendsto_rightDeriv_mul_log_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `derivWithin` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul` `log` `Set.Ioi` `instPreorder` `Filter.atTop`	—	`Filter.tendsto_congr'` `Filter.EventuallyEq.eq_1` `Filter.eventually_atTop` `instIsDirectedOrder` `instIsOrderedRing` `instArchimedean` `rightDeriv_mul_log` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Filter.Tendsto.atTop_add` `instIsOrderedAddMonoid` `instOrderTopologyReal` `tendsto_log_atTop` `tendsto_const_nhds`

Real.Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_log` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.instMul` `Real.log`	—	`Continuous.comp` `Real.continuous_mul_log`

---

← Back to Index