Documentation Verification Report

OneVariable

📁 Source: Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean

Statistics

Metric	Count
Definitions `jacobiTheta`	1
Theorems `continuousAt_jacobiTheta`, `differentiableAt_jacobiTheta`, `hasSum_nat_jacobiTheta`, `isBigO_at_im_infty_jacobiTheta_sub_one`, `jacobiTheta_S_smul`, `jacobiTheta_T_sq_smul`, `jacobiTheta_eq_jacobiTheta₂`, `jacobiTheta_eq_tsum_nat`, `jacobiTheta_two_add`, `norm_exp_mul_sq_le`, `norm_jacobiTheta_sub_one_le`	11
Total	12

(root)

Definitions

Name	Category	Theorems
`jacobiTheta` 📖	CompOp	11 math math: `hasSum_nat_jacobiTheta`, `jacobiTheta_T_sq_smul`, `jacobiTheta_S_smul`, `norm_jacobiTheta_sub_one_le`, `isBigO_at_im_infty_jacobiTheta_sub_one`, `continuousAt_jacobiTheta`, `mdifferentiable_jacobiTheta`, `jacobiTheta_eq_jacobiTheta₂`, `jacobiTheta_eq_tsum_nat`, `jacobiTheta_two_add`, `differentiableAt_jacobiTheta`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_jacobiTheta` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.im`	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `jacobiTheta`	—	`DifferentiableAt.continuousAt` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `differentiableAt_jacobiTheta`
`differentiableAt_jacobiTheta` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.im`	`DifferentiableAt` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `jacobiTheta`	—	`jacobiTheta_eq_jacobiTheta₂` `differentiableAt_jacobiTheta₂_snd`
`hasSum_nat_jacobiTheta` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.im`	`HasSum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.exp` `Complex.instMul` `Complex.ofReal` `Real.pi` `Complex.I` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instAdd` `Complex.instNatCast` `Complex.instOne` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instSub` `jacobiTheta` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`hasSum_jacobiTheta₂_term` `HasSum.nat_add_neg` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `zero_add` `MulZeroClass.mul_zero` `Nat.instAtLeastTwoHAddOfNat` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass` `two_ne_zero'` `CharZero.NeZero.two` `Complex.instCharZero` `HasSum.div_const` `Nat.cast_one` `Nat.cast_add` `Mathlib.Meta.NormNum.isInt_eq_true` `Mathlib.Meta.NormNum.isInt_sub` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isInt_neg` `add_sub_assoc` `Complex.exp_zero` `neg_sq` `MulZeroClass.zero_mul` `sq` `Int.cast_zero` `neg_zero` `Nat.cast_zero` `Int.cast_natCast` `Int.cast_neg` `Finset.sum_range_one` `hasSum_nat_add_iff'` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`isBigO_at_im_infty_jacobiTheta_sub_one` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.comap` `Complex.im` `Filter.atTop` `Real.instPreorder` `Complex.instSub` `jacobiTheta` `Complex.instOne` `Real.exp` `Real.instMul` `Real.instNeg` `Real.pi`	—	`Asymptotics.IsBigO_def` `Asymptotics.IsBigOWith_def` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `norm_jacobiTheta_sub_one_le` `LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.norm_eq_abs` `Real.abs_exp` `neg_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `le_refl` `mul_one` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `sub_le_sub_left` `Real.exp_monotone` `neg_le_neg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.pi_pos` `Real.exp_pos`
`jacobiTheta_S_smul` 📖	mathematical	—	`jacobiTheta` `UpperHalfPlane.coe` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `ModularGroup.S` `Complex` `Complex.instMul` `Complex.instPow` `Complex.instNeg` `Complex.I` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instOne` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`ne_of_gt` `UpperHalfPlane.coe_im_pos` `Complex.zero_im` `Nat.instAtLeastTwoHAddOfNat` `Complex.cpow_eq_zero_iff` `not_and_or` `mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `neg_ne_zero` `Complex.I_ne_zero` `UpperHalfPlane.im_inv_neg_coe_pos` `UpperHalfPlane.modular_S_smul` `jacobiTheta_eq_jacobiTheta₂` `Nat.cast_zero` `Nat.cast_one` `jacobiTheta₂_functional_equation` `zero_pow` `two_ne_zero` `MulZeroClass.mul_zero` `zero_div` `Complex.exp_zero` `mul_one` `mul_one_div` `div_self` `one_mul` `inv_neg` `neg_div` `one_div`
`jacobiTheta_T_sq_smul` 📖	mathematical	—	`jacobiTheta` `UpperHalfPlane.coe` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `Monoid.toNatPow` `ModularGroup.T`	—	`Nat.instAtLeastTwoHAddOfNat` `UpperHalfPlane.modular_T_zpow_smul` `Int.cast_ofNat` `jacobiTheta_two_add`
`jacobiTheta_eq_jacobiTheta₂` 📖	mathematical	—	`jacobiTheta` `jacobiTheta₂` `Complex` `Complex.instZero`	—	`tsum_congr` `MulZeroClass.mul_zero` `zero_add`
`jacobiTheta_eq_tsum_nat` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.im`	`jacobiTheta` `Complex` `Complex.instAdd` `Complex.instOne` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `Complex.exp` `Complex.ofReal` `Real.pi` `Complex.I` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `HasSum.tsum_eq` `Complex.instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_nat_jacobiTheta` `mul_div_cancel₀` `two_ne_zero'` `CharZero.NeZero.two` `Complex.instCharZero` `add_sub_assoc` `add_sub_cancel_left`
`jacobiTheta_two_add` 📖	mathematical	—	`jacobiTheta` `Complex` `Complex.instAdd` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `jacobiTheta_eq_jacobiTheta₂` `add_comm` `jacobiTheta₂_add_right`
`norm_exp_mul_sq_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.im`	`Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Complex.exp` `Complex.instMul` `Complex.ofReal` `Real.pi` `Complex.I` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instIntCast` `Real.instMonoid` `Real.exp` `Real.instMul` `Real.instNeg`	—	`Real.exp_lt_one_iff` `mul_neg_of_neg_of_pos` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.pi_pos` `LE.le.trans` `le_of_eq` `Complex.norm_exp` `Complex.ofReal_mul` `Complex.ofReal_pow` `Mathlib.Tactic.Ring.of_eq` `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.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Complex.re_ofReal_mul` `Complex.mul_I_re` `Mathlib.Tactic.Ring.neg_congr` `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` `Mathlib.Tactic.Ring.mul_one` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Int.instAddLeftMono` `Real.exp_mul` `Int.cast_pow` `Real.rpow_intCast` `zpow_natCast` `Nat.cast_pow` `Int.natAbs_sq` `pow_le_pow_of_le_one` `Real.instIsOrderedRing` `LT.lt.le` `Real.exp_pos` `sq`
`norm_jacobiTheta_sub_one_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.im`	`Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instSub` `jacobiTheta` `Complex.instOne` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instSub` `Real.instOne` `Real.exp` `Real.instNeg` `Real.pi`	—	`Int.cast_add` `Int.cast_one` `norm_exp_mul_sq_le` `pow_succ'` `div_eq_mul_inv` `hasSum_mul_left_iff` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.exp_ne_zero` `hasSum_geometric_of_lt_one` `LT.lt.le` `Real.exp_pos` `Real.exp_lt_one_iff` `mul_neg_of_neg_of_pos` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.pi_pos` `Summable.of_nonneg_of_le` `norm_nonneg` `HasSum.summable` `LE.le.trans` `norm_tsum_le_tsum_norm` `LE.le.trans_eq` `Summable.tsum_mono` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Nat.instAtLeastTwoHAddOfNat` `sub_eq_iff_eq_add'` `jacobiTheta_eq_tsum_nat` `norm_mul` `NormedDivisionRing.toNormMulClass` `Complex.norm_two` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `div_mul_comm` `mul_comm`

---

← Back to Index