DedekindEta

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

Statistics

Metric	Count
Definitions eta, eta_q, termη	3
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	18

ModularForm

Definitions

Name	Category	Theorems
eta 📖	CompOp	3 math math: eta_comp_eq_csqrt_I_inv, logDeriv_eta_eq_E2, differentiableAt_eta_of_mem_upperHalfPlaneSet
eta_q 📖	CompOp	9 math math: eta_q_eq_pow, discriminant_bounded_factor, tsum_logDeriv_eta_q, eta_q_eq_cexp, differentiableAt_eta_tprod, discriminant_eq_q_prod, summable_logDeriv_one_sub_eta_q, summable_eta_q, multipliableLocallyUniformlyOn_eta
termη 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_eta_of_mem_upperHalfPlaneSet 📖	mathematical	Complex Set Set.instMembership UpperHalfPlane.upperHalfPlaneSet	DifferentiableAt Complex 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 Complex 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.add_assoc_rev Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one 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.toPow 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 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 Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing	—	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.const_mul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing 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 IsSemitopologicalRing.toContinuousNeg Continuous.comp_continuousOn' Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring 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 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	—	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