Documentation Verification Report

CharacteristicFunction

📁 Source: Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean

Statistics

Metric	Count
Definitions `characteristic`	1
Theorems `characteristic_add_top_eventuallyLE`, `characteristic_add_top_le`, `characteristic_congr_codiscrete`, `characteristic_even`, `characteristic_eventually_nonneg`, `characteristic_mul_top_eventuallyLE`, `characteristic_mul_top_le`, `characteristic_mul_zero_eventuallyLE`, `characteristic_mul_zero_le`, `characteristic_nonneg`, `characteristic_pow_top`, `characteristic_pow_zero`, `characteristic_sub_characteristic_eq_proximity_sub_proximity`, `characteristic_sum_top_eventuallyLE`, `characteristic_sum_top_le`, `characteristic_top_mul_eventually_le`, `characteristic_top_mul_le`, `characteristic_zero_mul_eventually_le`, `characteristic_zero_mul_le`	19
Total	20

ValueDistribution

Definitions

Name	Category	Theorems
`characteristic` 📖	CompOp	27 math math: `characteristic_even`, `characteristic_mul_top_le`, `isBigO_characteristic_sub_characteristic_shift`, `characteristic_sub_characteristic_eq_proximity_sub_proximity`, `characteristic_sub_characteristic_inv_of_ne_zero`, `characteristic_sub_characteristic_inv_at_zero`, `characteristic_sub_characteristic_inv_le`, `characteristic_eventually_nonneg`, `characteristic_add_top_eventuallyLE`, `characteristic_mul_zero_eventuallyLE`, `characteristic_pow_zero`, `characteristic_top_mul_le`, `characteristic_sub_characteristic_inv`, `characteristic_nonneg`, `isBigO_characteristic_sub_characteristic_inv`, `characteristic_sum_top_le`, `characteristic_add_top_le`, `characteristic_mul_zero_le`, `characteristic_pow_top`, `characteristic_congr_codiscrete`, `abs_characteristic_sub_characteristic_shift_eqO`, `characteristic_zero_mul_eventually_le`, `characteristic_zero_mul_le`, `characteristic_top_mul_eventually_le`, `characteristic_sum_top_eventuallyLE`, `abs_characteristic_sub_characteristic_shift_le`, `characteristic_mul_top_eventuallyLE`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`characteristic_add_top_eventuallyLE` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField`	`Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `characteristic` `Pi.instAdd` `Complex` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Top.top` `WithTop` `WithTop.top` `Real.instAdd` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Filter.mp_mem` `Nat.instAtLeastTwoHAddOfNat` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `characteristic_add_top_le`
`characteristic_add_top_le` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Real` `Real.instLE` `Real.instOne`	`Real` `Real.instLE` `characteristic` `Pi.instAdd` `Complex` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Top.top` `WithTop` `WithTop.top` `Real.instAdd` `Real.log` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Complex.instProperSpace` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `proximity_add_top_le` `logCounting_add_top_le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero`
`characteristic_congr_codiscrete` 📖	mathematical	`Filter.EventuallyEq` `Complex` `Filter.codiscrete` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`characteristic`	—	`Complex.instProperSpace` `logCounting_congr_codiscrete` `proximity_congr_codiscrete`
`characteristic_even` 📖	mathematical	—	`Function.Even` `Real` `Real.instNeg` `characteristic`	—	`Function.Even.add` `Complex.instProperSpace` `proximity_even` `logCounting_even`
`characteristic_eventually_nonneg` 📖	mathematical	—	`Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `Pi.instZero` `Real.instZero` `characteristic`	—	`Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `characteristic_nonneg`
`characteristic_mul_top_eventuallyLE` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `Top.top` `WithTop` `WithTop.top` `Pi.instAdd` `Real.instAdd`	—	`Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `characteristic_mul_top_le`
`characteristic_mul_top_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Real` `Real.instLE` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `Top.top` `WithTop` `WithTop.top` `Pi.instAdd` `Real.instAdd`	—	`Complex.instProperSpace` `add_add_add_comm` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `proximity_mul_top_le` `logCounting_mul_top_le`
`characteristic_mul_zero_eventuallyLE` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `WithTop` `WithTop.zero` `Complex.instZero` `Pi.instAdd` `Real.instAdd`	—	`Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `characteristic_mul_zero_le`
`characteristic_mul_zero_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Real` `Real.instLE` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `WithTop` `WithTop.zero` `Complex.instZero` `Pi.instAdd` `Real.instAdd`	—	`Complex.instProperSpace` `add_add_add_comm` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `proximity_mul_zero_le` `logCounting_mul_zero_le`
`characteristic_nonneg` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`Real` `Real.instLE` `Real.instZero` `characteristic`	—	`add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Complex.instProperSpace` `proximity_nonneg` `logCounting_nonneg`
`characteristic_pow_top` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instPow` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Top.top` `WithTop` `WithTop.top` `AddMonoid.toNSMul` `Pi.addMonoid` `Real` `Real.instAddMonoid`	—	`Complex.instProperSpace` `proximity_pow_top` `nsmul_eq_mul` `logCounting_pow_top` `smul_add`
`characteristic_pow_zero` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instPow` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `WithTop` `WithTop.zero` `Complex.instZero` `AddMonoid.toNSMul` `Pi.addMonoid` `Real` `Real.instAddMonoid`	—	`Complex.instProperSpace` `proximity_pow_zero` `nsmul_eq_mul` `logCounting_pow_zero` `smul_add`
`characteristic_sub_characteristic_eq_proximity_sub_proximity` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField`	`Pi.instSub` `Real` `Real.instSub` `characteristic` `Top.top` `WithTop` `WithTop.top` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `proximity`	—	`Complex.instProperSpace` `logCounting_sub_const` `add_sub_add_right_eq_sub`
`characteristic_sum_top_eventuallyLE` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField`	`Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `characteristic` `Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Top.top` `WithTop` `WithTop.top` `Pi.instAdd` `Real.instAdd` `Real.instAddCommMonoid` `Real.log` `Real.instNatCast` `Finset.card`	—	`Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `characteristic_sum_top_le`
`characteristic_sum_top_le` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Real` `Real.instLE` `Real.instOne`	`Real` `Real.instLE` `characteristic` `Finset.sum` `Pi.addCommMonoid` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Top.top` `WithTop` `WithTop.top` `Real.instAdd` `Real.instAddCommMonoid` `Real.log` `Real.instNatCast` `Finset.card`	—	`Complex.instProperSpace` `Finset.sum_congr` `Finset.sum_apply` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `proximity_sum_top_le` `logCounting_sum_top_le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Finset.sum_add_distrib`
`characteristic_top_mul_eventually_le` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `Top.top` `WithTop` `WithTop.top` `Pi.instAdd` `Real.instAdd`	—	`characteristic_mul_top_eventuallyLE`
`characteristic_top_mul_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Real` `Real.instLE` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `Top.top` `WithTop` `WithTop.top` `Pi.instAdd` `Real.instAdd`	—	`characteristic_mul_top_le`
`characteristic_zero_mul_eventually_le` 📖	mathematical	`Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Filter.EventuallyLE` `Real` `Real.instLE` `Filter.atTop` `Real.instPreorder` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `WithTop` `WithTop.zero` `Complex.instZero` `Pi.instAdd` `Real.instAdd`	—	`characteristic_mul_zero_eventuallyLE`
`characteristic_zero_mul_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Meromorphic` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace`	`Real` `Real.instLE` `characteristic` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Pi.instMul` `Complex.instMul` `WithTop` `WithTop.zero` `Complex.instZero` `Pi.instAdd` `Real.instAdd`	—	`characteristic_mul_zero_le`

---

← Back to Index