Documentation Verification Report

Series

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean

Statistics

Metric	Count
Definitions	0
Theorems `cos_eq_tsum`, `cos_eq_tsum'`, `cosh_eq_tsum`, `hasSum_cos`, `hasSum_cos'`, `hasSum_cosh`, `hasSum_sin`, `hasSum_sin'`, `hasSum_sinh`, `sin_eq_tsum`, `sin_eq_tsum'`, `sinh_eq_tsum`, `cos_eq_tsum`, `cosh_eq_tsum`, `cosh_le_exp_half_sq`, `hasSum_cos`, `hasSum_cosh`, `hasSum_sin`, `hasSum_sinh`, `sin_eq_tsum`, `sinh_eq_tsum`	21
Total	21

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cos_eq_tsum` 📖	mathematical	—	`cos` `tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNeg` `instOne` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_cos`
`cos_eq_tsum'` 📖	mathematical	—	`cos` `tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instMul` `I` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_cos'`
`cosh_eq_tsum` 📖	mathematical	—	`cosh` `tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_cosh`
`hasSum_cos` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNeg` `instOne` `instNatCast` `Nat.factorial` `cos` `SummationFilter.unconditional`	—	`mul_pow` `pow_mul` `I_sq` `mul_comm` `hasSum_cos'`
`hasSum_cos'` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instMul` `I` `instNatCast` `Nat.factorial` `cos` `SummationFilter.unconditional`	—	`cos.eq_1` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `exp_eq_exp_ℂ` `Nat.instAtLeastTwoHAddOfNat` `HasSum.div_const` `IsTopologicalRing.toIsTopologicalSemiring` `HasSum.add` `IsTopologicalSemiring.toContinuousAdd` `NormedSpace.expSeries_div_hasSum_exp` `instCharZero` `instCompleteSpace` `Equiv.hasSum_iff` `HasSum.prod_fiberwise` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `mul_comm` `Fin.sum_univ_two` `add_zero` `pow_succ` `pow_mul` `mul_pow` `neg_sq` `neg_mul` `mul_neg` `neg_div` `add_neg_cancel` `zero_div` `mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `two_ne_zero` `CharZero.NeZero.two` `hasSum_fintype` `SummationFilter.instLeAtTopUnconditional`
`hasSum_cosh` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `cosh` `SummationFilter.unconditional`	—	`mul_assoc` `I_mul_I` `mul_neg` `mul_one` `Even.neg_pow` `Distrib.rightDistribClass` `Nat.instAtLeastTwoHAddOfNat` `cos_mul_I` `hasSum_cos'`
`hasSum_sin` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNeg` `instOne` `instNatCast` `Nat.factorial` `sin` `SummationFilter.unconditional`	—	`mul_pow` `pow_succ` `pow_mul` `I_sq` `mul_div_assoc` `div_right_comm` `div_self` `I_ne_zero` `mul_comm` `mul_one_div` `mul_assoc` `hasSum_sin'`
`hasSum_sin'` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instMul` `I` `instNatCast` `Nat.factorial` `sin` `SummationFilter.unconditional`	—	`sin.eq_1` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `exp_eq_exp_ℂ` `Nat.instAtLeastTwoHAddOfNat` `HasSum.div_const` `IsTopologicalRing.toIsTopologicalSemiring` `HasSum.mul_right` `HasSum.sub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NormedSpace.expSeries_div_hasSum_exp` `instCharZero` `instCompleteSpace` `Equiv.hasSum_iff` `HasSum.prod_fiberwise` `IsTopologicalSemiring.toContinuousAdd` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `mul_comm` `Fin.sum_univ_two` `add_zero` `pow_succ` `pow_mul` `mul_pow` `neg_sq` `sub_self` `MulZeroClass.zero_mul` `zero_div` `zero_add` `neg_mul` `mul_neg` `neg_div` `mul_assoc` `mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `two_ne_zero` `CharZero.NeZero.two` `div_I` `hasSum_fintype` `SummationFilter.instLeAtTopUnconditional`
`hasSum_sinh` 📖	mathematical	—	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `sinh` `SummationFilter.unconditional`	—	`pow_add` `pow_mul` `pow_one` `mul_assoc` `I_mul_I` `mul_neg` `mul_one` `neg_pow` `Even.neg_pow` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `neg_mul` `one_mul` `neg_div` `div_I` `neg_neg` `sin_mul_I` `HasSum.mul_right` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `hasSum_sin'`
`sin_eq_tsum` 📖	mathematical	—	`sin` `tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNeg` `instOne` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_sin`
`sin_eq_tsum'` 📖	mathematical	—	`sin` `tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instMul` `I` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_sin'`
`sinh_eq_tsum` 📖	mathematical	—	`sinh` `tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroup` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_sinh`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cos_eq_tsum` 📖	mathematical	—	`cos` `tsum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `instMonoid` `instNeg` `instOne` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_cos`
`cosh_eq_tsum` 📖	mathematical	—	`cosh` `tsum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_cosh`
`cosh_le_exp_half_sq` 📖	mathematical	—	`Real` `instLE` `cosh` `exp` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `cosh_eq_tsum` `instIsTopologicalRingReal` `exp_eq_exp_ℝ` `NormedSpace.exp_eq_tsum` `RCLike.charZero_rclike` `Summable.tsum_le_tsum` `instIsOrderedAddMonoid` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `pow_mul` `div_pow` `inv_mul_eq_div` `div_div` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `IsOrderedRing.toPosMulMono` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `le_refl` `mul_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instZeroLEOneClass` `NeZero.charZero_one` `Nat.factorial_pos` `Nat.two_pow_mul_factorial_le_factorial_two_mul` `HasSum.summable` `hasSum_cosh` `NormedSpace.expSeries_summable'` `NNRat.instContinuousSMulRatReal` `instCompleteSpace`
`hasSum_cos` 📖	mathematical	—	`HasSum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `instMonoid` `instNeg` `instOne` `instNatCast` `Nat.factorial` `cos` `SummationFilter.unconditional`	—	`Nat.cast_one` `Int.cast_pow` `Int.cast_neg` `Int.cast_one` `Complex.ofReal_pow` `Complex.ofReal_neg` `Complex.hasSum_cos`
`hasSum_cosh` 📖	mathematical	—	`HasSum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instNatCast` `Nat.factorial` `cosh` `SummationFilter.unconditional`	—	`Complex.hasSum_cosh`
`hasSum_sin` 📖	mathematical	—	`HasSum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `instMonoid` `instNeg` `instOne` `instNatCast` `Nat.factorial` `sin` `SummationFilter.unconditional`	—	`Nat.cast_one` `Int.cast_pow` `Int.cast_neg` `Int.cast_one` `Complex.ofReal_pow` `Complex.ofReal_neg` `Complex.hasSum_sin`
`hasSum_sinh` 📖	mathematical	—	`HasSum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instNatCast` `Nat.factorial` `sinh` `SummationFilter.unconditional`	—	`Complex.hasSum_sinh`
`sin_eq_tsum` 📖	mathematical	—	`sin` `tsum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `Monoid.toNatPow` `instMonoid` `instNeg` `instOne` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_sin`
`sinh_eq_tsum` 📖	mathematical	—	`sinh` `tsum` `Real` `instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `DivInvMonoid.toDiv` `instDivInvMonoid` `Monoid.toNatPow` `instMonoid` `instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_sinh`

---

← Back to Index