Positivity

📁 Source: Mathlib/Analysis/Complex/Positivity.lean

Statistics

Metric	Count
Definitions	0
Theorems apply_le_of_iteratedDeriv_alternating, apply_le_of_iteratedDeriv_nonneg, nonneg_of_iteratedDeriv_nonneg, nonneg_of_iteratedDeriv_nonneg	4
Total	4

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_le_of_iteratedDeriv_alternating 📖	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Preorder.toLE PartialOrder.toPreorder Complex.partialOrder Complex.instZero Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne iteratedDeriv Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	—	—	neg_neg apply_le_of_iteratedDeriv_nonneg comp differentiable_neg iteratedDeriv_comp_neg neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono RCLike.toIsOrderedAddMonoid covariant_swap_add_of_covariant_add
apply_le_of_iteratedDeriv_nonneg 📖	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Preorder.toLE PartialOrder.toPreorder Complex.partialOrder Complex.instZero iteratedDeriv Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	—	—	iteratedDeriv_zero sub_self iteratedDeriv_succ' deriv_sub_const sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono RCLike.toIsOrderedAddMonoid nonneg_of_iteratedDeriv_nonneg sub_const
nonneg_of_iteratedDeriv_nonneg 📖	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Preorder.toLE PartialOrder.toPreorder Complex.partialOrder Complex.instZero iteratedDeriv Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	—	—	DifferentiableOn.nonneg_of_iteratedDeriv_nonneg differentiableOn Metric.mem_ball Complex.dist_eq Complex.eq_re_of_ofReal_le sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono RCLike.toIsOrderedAddMonoid Complex.norm_of_nonneg Complex.nonneg_iff lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Real.instIsOrderedAddMonoid

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonneg_of_iteratedDeriv_nonneg 📖	—	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Metric.ball Preorder.toLE PartialOrder.toPreorder Complex.partialOrder Complex.instZero iteratedDeriv Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set Set.instMembership	—	—	Complex.taylorSeries_eq_on_ball' Complex.eq_re_of_ofReal_le sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono RCLike.toIsOrderedAddMonoid tsum_nonneg Complex.orderClosedTopology Complex.ofReal_natCast Complex.ofReal_pow Complex.ofReal_inv Complex.ofReal_mul Nat.cast_zero Complex.le_def Complex.zero_re mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt inv_pos_of_pos RCLike.toPosMulReflectLT Nat.cast_pos' Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.factorial_pos pow_nonneg IsOrderedRing.toZeroLEOneClass

---

← Back to Index