Documentation Verification Report

DedekindEta

📁 Source: Mathlib/NumberTheory/ModularForms/DedekindEta.lean

Statistics

Metric	Count
Definitions `eta`, `eta_q`	2
Theorems `differentiableAt_eta_of_mem_upperHalfPlaneSet`, `differentiableAt_eta_tprod`, `eta_ne_zero`, `eta_q_eq_cexp`, `eta_q_eq_pow`, `eta_tprod_ne_zero`, `logDeriv_eta_eq_E2`, `logDeriv_one_sub_cexp`, `logDeriv_one_sub_mul_cexp_comp`, `logDeriv_qParam`, `multipliableLocallyUniformlyOn_eta`, `one_sub_eta_q_ne_zero`, `summable_eta_q`, `summable_logDeriv_one_sub_eta_q`, `tsum_logDeriv_eta_q`	15
Total	17

ModularForm

Definitions

Name	Category	Theorems
`eta` 📖	CompOp	2 math math: `logDeriv_eta_eq_E2`, `differentiableAt_eta_of_mem_upperHalfPlaneSet`
`eta_q` 📖	CompOp	7 math math: `eta_q_eq_pow`, `tsum_logDeriv_eta_q`, `eta_q_eq_cexp`, `differentiableAt_eta_tprod`, `summable_logDeriv_one_sub_eta_q`, `summable_eta_q`, `multipliableLocallyUniformlyOn_eta`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableAt_eta_of_mem_upperHalfPlaneSet` 📖	mathematical	`Complex` `Set` `Set.instMembership` `UpperHalfPlane.upperHalfPlaneSet`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `eta`	—	`DifferentiableAt.mul` `Differentiable.differentiableAt` `Function.Periodic.differentiable_qParam` `differentiableAt_eta_tprod`
`differentiableAt_eta_tprod` 📖	mathematical	`Complex` `Set` `Set.instMembership` `UpperHalfPlane.upperHalfPlaneSet`	`DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `tprod` `CommRing.toCommMonoid` `Complex.commRing` `Complex.instSub` `Complex.instOne` `eta_q` `SummationFilter.unconditional`	—	`DifferentiableWithinAt.differentiableAt` `TendstoLocallyUniformlyOn.differentiableOn` `Complex.instCompleteSpace` `Filter.atTop_neBot` `Finset.isDirected_le` `MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn` `multipliableLocallyUniformlyOn_eta` `Filter.univ_mem'` `Finset.prod_fn` `DifferentiableOn.finset_prod` `DifferentiableOn.const_sub` `DifferentiableOn.fun_pow` `Differentiable.differentiableOn` `Function.Periodic.differentiable_qParam` `UpperHalfPlane.isOpen_upperHalfPlaneSet` `IsOpen.mem_nhds`
`eta_ne_zero` 📖	—	`Complex` `Set` `Set.instMembership` `UpperHalfPlane.upperHalfPlaneSet`	—	—	`mul_ne_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Function.Periodic.qParam_ne_zero` `eta_tprod_ne_zero`
`eta_q_eq_cexp` 📖	mathematical	—	`eta_q` `Complex.exp` `Complex` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Complex.instAdd` `Complex.instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `div_one` `nsmul_eq_mul` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add`
`eta_q_eq_pow` 📖	mathematical	—	`eta_q` `Complex` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.exp` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`Nat.instAtLeastTwoHAddOfNat` `div_one`
`eta_tprod_ne_zero` 📖	—	`Complex` `Set` `Set.instMembership` `UpperHalfPlane.upperHalfPlaneSet`	—	—	`tprod_one_add_ne_zero_of_summable` `NormedDivisionRing.to_normOneClass` `Complex.instCompleteSpace` `NormedDivisionRing.toNormMulClass` `one_sub_eta_q_ne_zero` `norm_neg` `norm_pow` `FiniteDimensional.rclike_to_real` `norm_norm` `summable_eta_q`
`logDeriv_eta_eq_E2` 📖	mathematical	—	`logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `instCommCStarAlgebraComplex` `eta` `UpperHalfPlane.coe` `Complex.instMul` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.ofReal` `Real.pi` `Complex.I` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `EisensteinSeries.E2`	—	`Nat.instAtLeastTwoHAddOfNat` `logDeriv_mul` `Function.Periodic.qParam_ne_zero` `eta_tprod_ne_zero` `UpperHalfPlane.coe_im_pos` `Differentiable.differentiableAt` `Function.Periodic.differentiable_qParam` `differentiableAt_eta_tprod` `logDeriv_tprod_eq_tsum` `UpperHalfPlane.isOpen_upperHalfPlaneSet` `one_sub_eta_q_ne_zero` `DifferentiableOn.const_sub` `DifferentiableOn.fun_pow` `Differentiable.differentiableOn` `summable_logDeriv_one_sub_eta_q` `multipliableLocallyUniformlyOn_eta` `logDeriv_qParam` `tsum_logDeriv_eta_q` `one_div` `mul_inv_rev` `EisensteinSeries.G2_eq_tsum_cexp` `riemannZeta_two` `tsum_pow_div_one_sub_eq_tsum_sigma` `Complex.instCompleteSpace` `RCLike.instNormSMulClassInt` `UpperHalfPlane.norm_exp_two_pi_I_lt_one` `mul_sub` `sub_eq_add_neg` `mul_add` `Distrib.leftDistribClass` `eta_q_eq_pow` `mul_neg` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instT2Space` `inv_div` `pow_one` `tsum_pnat_eq_tsum_succ` `Nat.cast_add` `Nat.cast_one` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`logDeriv_one_sub_cexp` 📖	mathematical	—	`logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `instCommCStarAlgebraComplex` `Complex.instSub` `Complex.instOne` `Complex.instMul` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg`	—	`deriv_fun_sub` `deriv_const'` `deriv_fun_mul` `MulZeroClass.zero_mul` `Complex.deriv_exp` `zero_add` `zero_sub` `neg_mul`
`logDeriv_one_sub_mul_cexp_comp` 📖	mathematical	`Differentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex`	`logDeriv` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `Complex.instSub` `Complex.instOne` `Complex.instMul` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg` `deriv`	—	`logDeriv_comp` `DifferentiableAt.const_sub` `DifferentiableAt.const_mul` `DifferentiableAt.cexp` `differentiableAt_id` `logDeriv_one_sub_cexp` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.atom_pf'`
`logDeriv_qParam` 📖	mathematical	—	`logDeriv` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `instCommCStarAlgebraComplex` `Function.Periodic.qParam` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I`	—	`Nat.instAtLeastTwoHAddOfNat` `logDeriv_comp` `DifferentiableAt.cexp` `differentiableAt_id` `DifferentiableAt.const_mul` `deriv_const_mul` `Complex.logDeriv_exp` `deriv_id''` `mul_one` `one_mul`
`multipliableLocallyUniformlyOn_eta` 📖	mathematical	—	`MultipliableLocallyUniformlyOn` `Complex` `CommRing.toCommMonoid` `Complex.commRing` `Complex.instSub` `Complex.instOne` `eta_q` `UpperHalfPlane.upperHalfPlaneSet` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `UniformSpace.toTopologicalSpace`	—	`sub_eq_add_neg` `hasProdLocallyUniformlyOn_of_forall_compact` `UpperHalfPlane.isOpen_upperHalfPlaneSet` `locallyCompact_of_proper` `Complex.instProperSpace` `Nat.instAtLeastTwoHAddOfNat` `ContinuousOn.norm` `ContinuousOn.cexp` `ContinuousOn.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuousOn_const` `continuousOn_id'` `IsCompact.exists_sSup_image_eq_and_ge` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Summable.hasProdUniformlyOn_nat_one_add` `NormedDivisionRing.to_normOneClass` `Complex.instCompleteSpace` `summable_eta_q` `Filter.univ_mem'` `eta_q_eq_pow` `norm_neg` `norm_pow` `NormedDivisionRing.toNormMulClass` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `ContinuousOn.neg` `IsTopologicalRing.toContinuousNeg` `Continuous.comp_continuousOn'` `Continuous.pow` `continuous_id'` `Continuous.div_const` `hasProdUniformlyOn_iff_tendstoUniformlyOn` `Set.not_nonempty_iff_eq_empty` `tendstoUniformlyOn_empty`
`one_sub_eta_q_ne_zero` 📖	—	`Complex` `Set` `Set.instMembership` `UpperHalfPlane.upperHalfPlaneSet`	—	—	`Nat.instAtLeastTwoHAddOfNat` `eta_q_eq_cexp` `sub_ne_zero` `nsmul_eq_mul` `Nat.cast_add` `Nat.cast_one` `add_zero` `MulZeroClass.zero_mul` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `CStarRing.norm_of_mem_unitary` `CStarAlgebra.toCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `UpperHalfPlane.norm_exp_two_pi_I_lt_one`
`summable_eta_q` 📖	mathematical	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instNeg` `eta_q` `UpperHalfPlane.coe` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `eta_q_eq_pow` `norm_neg` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `summable_nat_add_iff` `instIsTopologicalAddGroupReal` `norm_norm` `UpperHalfPlane.norm_exp_two_pi_I_lt_one`
`summable_logDeriv_one_sub_eta_q` 📖	mathematical	`Complex` `Set` `Set.instMembership` `UpperHalfPlane.upperHalfPlaneSet`	`Summable` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `logDeriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `Complex.instSub` `Complex.instOne` `eta_q` `SummationFilter.unconditional`	—	`summable_norm_pow_mul_geometric_div_one_sub` `Complex.instCompleteSpace` `UpperHalfPlane.norm_qParam_lt_one` `Nat.instAtLeastTwoHAddOfNat` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `summable_nat_add_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`tsum_logDeriv_eta_q` 📖	mathematical	—	`tsum` `Complex` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `logDeriv` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `Complex.instSub` `Complex.instOne` `eta_q` `SummationFilter.unconditional` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instAdd` `Complex.instNeg`	—	`Nat.instAtLeastTwoHAddOfNat` `tsum_congr` `tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instT2Space`

---

← Back to Index