DerivativeTest

📁 Source: Mathlib/Analysis/Calculus/DerivativeTest.lean

Statistics

Metric	Count
Definitions	0
Theorems deriv_neg_left_of_sign_deriv, deriv_neg_right_of_sign_deriv, deriv_pos_left_of_sign_deriv, deriv_pos_right_of_sign_deriv, eventually_nhdsWithin_sign_eq_of_deriv_neg, eventually_nhdsWithin_sign_eq_of_deriv_pos, isLocalMax_of_deriv, isLocalMax_of_deriv', isLocalMax_of_deriv_Ioo, isLocalMax_of_deriv_deriv_neg, isLocalMax_of_sign_deriv, isLocalMin_of_deriv, isLocalMin_of_deriv', isLocalMin_of_deriv_Ioo, isLocalMin_of_deriv_deriv_pos, isLocalMin_of_sign_deriv	16
Total	16

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_neg_left_of_sign_deriv 📖	mathematical	Filter.Eventually Real SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT deriv 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.instSub nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	Real.instLT Set.Iio	—	Filter.mp_mem self_mem_nhdsWithin nhdsLT_le_nhdsNE Filter.univ_mem' sign_eq_neg_one_iff sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
deriv_neg_right_of_sign_deriv 📖	mathematical	Filter.Eventually Real SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT deriv 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.instSub nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	Real.instLT Set.Ioi	—	Filter.mp_mem self_mem_nhdsWithin nhdsGT_le_nhdsNE Filter.univ_mem' sign_eq_neg_one_iff sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
deriv_pos_left_of_sign_deriv 📖	mathematical	Filter.Eventually Real SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT deriv 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.instSub nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	Real.instLT Set.Iio	—	Filter.mp_mem self_mem_nhdsWithin nhdsLT_le_nhdsNE Filter.univ_mem' sign_eq_one_iff sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
deriv_pos_right_of_sign_deriv 📖	mathematical	Filter.Eventually Real SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT deriv 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.instSub nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	Real.instLT Set.Ioi	—	Filter.mp_mem self_mem_nhdsWithin nhdsGT_le_nhdsNE Filter.univ_mem' sign_eq_one_iff sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
eventually_nhdsWithin_sign_eq_of_deriv_neg 📖	mathematical	Real Real.instLT deriv 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.instZero	Filter.Eventually SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.decidableLT Real.instSub nhds	—	Left.sign_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_sub eventually_nhdsWithin_sign_eq_of_deriv_pos deriv.fun_neg'
eventually_nhdsWithin_sign_eq_of_deriv_pos 📖	mathematical	Real Real.instLT deriv 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.instZero	Filter.Eventually SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.decidableLT Real.instSub nhds	—	nhdsNE_sup_pure Filter.eventually_sup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivAt_iff_tendsto_slope DifferentiableAt.hasDerivAt differentiableAt_of_deriv_ne_zero ne_of_gt Filter.mp_mem self_mem_nhdsWithin Filter.Tendsto.eventually eventually_gt_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.univ_mem' Ne.lt_or_gt Ne.eq_def Set.mem_singleton_iff Set.mem_compl_iff sign_neg neg_of_slope_pos Real.instIsStrictOrderedRing sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sign_pos pos_of_slope_pos sub_pos sub_self sign_zero
isLocalMax_of_deriv 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Real.instLE Real.instZero deriv Set.Iio Real.instPreorder Set.Ioi	IsLocalMax	—	isLocalMax_of_deriv' nhdsLT_le_nhdsNE nhdsGT_le_nhdsNE
isLocalMax_of_deriv' 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace nhdsWithin Set.Iio Real.instPreorder Set.Ioi Real.instLE Real.instZero deriv	IsLocalMax	—	Filter.HasBasis.eventually_iff nhdsLT_basis instOrderTopologyReal instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and nhdsGT_basis instNoMaxOrderOfNontrivial isLocalMax_of_deriv_Ioo DifferentiableAt.differentiableWithinAt
isLocalMax_of_deriv_Ioo 📖	mathematical	Real Real.instLT ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Set.Ioo Real.instPreorder Real.instLE Real.instZero deriv	IsLocalMax	—	ContinuousOn.union_continuousAt isOpen_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul Set.Ioo_union_right Set.Ioo_union_left isLocalMax_of_mono_anti monotoneOn_of_deriv_nonneg convex_Ioc Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing interior_Ioc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial antitoneOn_of_deriv_nonpos convex_Ico interior_Ico instNoMinOrderOfNontrivial
isLocalMax_of_deriv_deriv_neg 📖	mathematical	Real Real.instLT deriv 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.instZero ContinuousAt	IsLocalMax Real.instPreorder	—	neg_neg IsLocalMin.neg Real.instIsOrderedAddMonoid isLocalMin_of_deriv_deriv_pos deriv.fun_neg' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono ContinuousAt.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal
isLocalMax_of_sign_deriv 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Eventually SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.instSub nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	IsLocalMax	—	deriv_pos_left_of_sign_deriv deriv_neg_right_of_sign_deriv Filter.eventually_sup Filter.Eventually.mono LT.lt.ne' LT.lt.ne nhdsLT_sup_nhdsGT isLocalMax_of_deriv differentiableAt_of_deriv_ne_zero le_of_lt
isLocalMin_of_deriv 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Real.instLE deriv Real.instZero Set.Iio Real.instPreorder Set.Ioi	IsLocalMin	—	isLocalMin_of_deriv' nhdsLT_le_nhdsNE nhdsGT_le_nhdsNE
isLocalMin_of_deriv' 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace nhdsWithin Set.Iio Real.instPreorder Set.Ioi Real.instLE deriv Real.instZero	IsLocalMin	—	Filter.HasBasis.eventually_iff nhdsLT_basis instOrderTopologyReal instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and nhdsGT_basis instNoMaxOrderOfNontrivial isLocalMin_of_deriv_Ioo DifferentiableAt.differentiableWithinAt
isLocalMin_of_deriv_Ioo 📖	mathematical	Real Real.instLT ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DifferentiableOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Set.Ioo Real.instPreorder Real.instLE deriv Real.instZero	IsLocalMin	—	isLocalMax_of_deriv_Ioo IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal DifferentiableOn.neg Left.nonneg_neg_iff IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid deriv.neg Left.neg_nonpos_iff IsLocalMax.neg neg_neg
isLocalMin_of_deriv_deriv_pos 📖	mathematical	Real Real.instLT deriv 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.instZero ContinuousAt	IsLocalMin Real.instPreorder	—	isLocalMin_of_sign_deriv nhdsWithin_le_nhds eventually_nhdsWithin_sign_eq_of_deriv_pos
isLocalMin_of_sign_deriv 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Eventually SignType DFunLike.coe OrderHom Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.instSub nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	IsLocalMin	—	IsLocalMax.neg Real.instIsOrderedAddMonoid isLocalMax_of_sign_deriv ContinuousAt.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal deriv.fun_neg' Left.sign_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono neg_sub neg_neg

---

← Back to Index