Basic

📁 Source: Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

Statistics

Metric	Count
Definitions evalUpperHalfPlaneCoe, evalUpperHalfPlaneIm, UpperHalfPlane, I, im, instAddActionReal, instCoeOutComplex, instInhabited, posRealAction, re, termℍ, upperHalfPlaneSet	12
Theorems I_im, I_re, canLift, coe_I, coe_im, coe_im_pos, coe_inj, coe_injective, coe_mk, coe_mk_subtype, coe_pos_real_smul, coe_re, coe_vadd, exists, ext, ext', ext_iff, ext_iff', ext_re_im, forall, im_inv_neg_coe_pos, im_ne_zero, im_pnat_div_pos, im_pos, instInfinite, instNontrivial, isOpen_upperHalfPlaneSet, mem_slitPlane, mk_coe, mk_im, mk_re, ne_int, ne_intCast, ne_nat, ne_natCast, ne_ofReal, ne_zero, normSq_ne_zero, normSq_pos, pos_real_im, pos_real_re, pos_real_smul_injective, range_coe, re_add_im, vadd_im, vadd_left_injective, vadd_re, vadd_right_cancel_iff	48
Total	60

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalUpperHalfPlaneCoe 📖	CompOp	—
evalUpperHalfPlaneIm 📖	CompOp	—

UpperHalfPlane

Definitions

Name	Category	Theorems
I 📖	CompOp	5 math math: isProperMap_smul_I, coe_I, I_re, I_im, toSL2R_smul_I
im 📖	CompOp	77 math math: image_coe_sphere, im_div_exp_dist_le, dist_le_iff_dist_coe_center_le, im_pos, im_smul_eq_div_normSq, isOpenMap_im, EisensteinSeries.r1_aux_bound, re_add_im, dist_eq_iff_eq_sinh, dist_log_im_le, ModularGroup.exists_max_im, ModularGroup.exists_bound_of_subgroup_invariant_of_isBigO, im_le_im_mul_exp_dist, dist_eq_iff_eq_sq_sinh, ModularGroup.im_T_smul, coe_toSL2R, image_coe_ball, dist_of_re_eq, center_im, volume_def, cosh_dist, image_coe_closedBall, dist_coe_center, IsZeroAtImInfty.petersson_exp_decay_left, lt_dist_iff_lt_dist_coe_center, dist_lt_iff_dist_coe_center_lt, SlashInvariantForm.exists_one_half_le_im_and_norm_le, dist_self_center, im_smul, ModularFormClass.exp_decay_sub_atImInfty, ModularFormClass.exists_petersson_le, IsZeroAtImInfty.exp_decay_atImInfty, dist_eq, ModularFormClass.exists_bound, ModularGroup.im_lt_im_S_smul, ModularGroup.im_T_zpow_smul, dist_eq_iff_dist_coe_center_eq, cmp_dist_eq_cmp_dist_coe_center, EisensteinSeries.r1_eq, le_dist_coe, ModularGroup.exists_one_half_le_im_smul, ModularGroup.exists_bound_fundamental_domain_of_isBigO, le_dist_iff_le_dist_coe_center, dist_center_dist, dist_le_dist_coe_div_sqrt, CuspFormClass.exists_bound, continuous_im, atImInfty_basis, ModularGroup_T_zpow_mem_verticalStrip, ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO, ModularGroup.exists_bound_of_invariant_of_isBigO, ModularGroup.im_smul_eq_div_normSq, cosh_half_dist, exp_half_dist, mk_im, sinh_half_dist_add_dist, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, CuspFormClass.exp_decay_atImInfty', ModularGroup.three_le_four_mul_im_sq_of_mem_fd, IsZeroAtImInfty.exp_decay_atImInfty', ModularGroup.im_T_inv_smul, dist_coe_le, pos_real_im, sinh_half_dist, dist_le_iff_le_sinh, dist_coe_center_sq, mem_verticalStrip_iff, I_im, cosh_dist', CuspFormClass.exp_decay_atImInfty, ModularGroup.three_lt_four_mul_im_sq_of_mem_fdo, coe_im, IsZeroAtImInfty.petersson_exp_decay_right, toSL2R_apply, c_mul_im_sq_le_normSq_denom, ModularFormClass.exp_decay_sub_atImInfty', vadd_im
instAddActionReal 📖	CompOp	12 math math: isometry_real_vadd, vadd_re, exists_SL2_smul_eq_of_apply_zero_one_ne_zero, exists_SL2_smul_eq_of_apply_zero_one_eq_zero, vadd_right_cancel_iff, SlashInvariantForm.vAdd_width_periodic, coe_vadd, modular_T_zpow_smul, SlashInvariantForm.vAdd_apply_of_mem_strictPeriods, vadd_im, modular_T_smul, vadd_left_injective
instCoeOutComplex 📖	CompOp	—
instInhabited 📖	CompOp	2 math math: ofComplex_apply_of_im_nonpos, ofComplex_apply_eq_ite
posRealAction 📖	CompOp	7 math math: coe_pos_real_smul, exists_SL2_smul_eq_of_apply_zero_one_ne_zero, pos_real_smul_injective, exists_SL2_smul_eq_of_apply_zero_one_eq_zero, pos_real_re, pos_real_im, isometry_pos_mul
re 📖	CompOp	22 math math: re_smul, center_re, EisensteinSeries.r1_aux_bound, isOpenMap_re, re_add_im, ModularGroup.tendsto_abs_re_smul, vadd_re, coe_toSL2R, ModularGroup.re_T_smul, ModularGroup.re_T_inv_smul, ModularGroup.exists_row_one_eq_and_min_re, ModularGroup.re_T_zpow_smul, EisensteinSeries.r1_eq, pos_real_re, ModularGroup.abs_two_mul_re_lt_one_of_mem_fdo, I_re, coe_re, mem_verticalStrip_iff, cosh_dist', mk_re, toSL2R_apply, continuous_re
termℍ 📖	CompOp	—
upperHalfPlaneSet 📖	CompOp	15 math math: summableLocallyUniformlyOn_iteratedDerivWithin_cexp, iteratedDerivWithin_tsum_cexp_eq, differentiableOn_iteratedDerivWithin_cotTerm, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow, ModularForm.eta_comp_eq_csqrt_I_inv, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow, contDiffOn_tsum_cexp, cot_pi_mul_contDiffWithinAt, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum, range_coe, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, isOpen_upperHalfPlaneSet, ModularForm.multipliableLocallyUniformlyOn_eta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
I_im 📖	mathematical	—	im I Real Real.instOne	—	—
I_re 📖	mathematical	—	re I Real Real.instZero	—	—
canLift 📖	mathematical	—	CanLift Complex UpperHalfPlane coe Real Real.instLT Real.instZero Complex.im	—	—
coe_I 📖	mathematical	—	coe I Complex.I	—	—
coe_im 📖	mathematical	—	Complex.im coe im	—	—
coe_im_pos 📖	mathematical	—	Real Real.instLT Real.instZero Complex.im coe	—	—
coe_inj 📖	mathematical	—	coe	—	ext_iff
coe_injective 📖	mathematical	—	UpperHalfPlane Complex coe	—	ext
coe_mk 📖	mathematical	Real Real.instLT Real.instZero Complex.im	coe	—	—
coe_mk_subtype 📖	mathematical	Real Real.instLT Real.instZero Complex.im	coe	—	—
coe_pos_real_smul 📖	mathematical	—	coe Real Real.instLT Real.instZero UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Positive.instMonoidSubtypeLtOfNat Real.semiring Real.partialOrder Real.instIsStrictOrderedRing MulAction.toSemigroupAction posRealAction Complex Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra Complex.instRCLike	—	Real.instIsStrictOrderedRing
coe_re 📖	mathematical	—	Complex.re coe re	—	—
coe_vadd 📖	mathematical	—	coe HVAdd.hVAdd Real UpperHalfPlane instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal Complex Complex.instAdd Complex.ofReal	—	—
exists 📖	mathematical	—	UpperHalfPlane Complex Real Real.instLT Real.instZero Complex.im	—	—
ext 📖	—	coe	—	—	—
ext' 📖	—	re im	—	—	ext_re_im
ext_iff 📖	mathematical	—	coe	—	ext
ext_iff' 📖	mathematical	—	coe	—	—
ext_re_im 📖	—	re im	—	—	ext Complex.ext
forall 📖	—	—	—	—	coe_im_pos
im_inv_neg_coe_pos 📖	mathematical	—	Real Real.instLT Real.instZero Complex.im Complex Complex.instInv Complex.instNeg coe	—	inv_neg Complex.inv_im neg_div neg_neg div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing im_pos normSq_pos
im_ne_zero 📖	—	—	—	—	LT.lt.ne' im_pos
im_pnat_div_pos 📖	mathematical	—	Real Real.instLT Real.instZero Complex.im Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.instNatCast coe	—	normSq_pos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd im_pos neg_div Complex.div_im MulZeroClass.zero_mul zero_div zero_sub neg_neg
im_pos 📖	mathematical	—	Real Real.instLT Real.instZero im	—	coe_im_pos
instInfinite 📖	mathematical	—	Infinite UpperHalfPlane	—	Infinite.of_injective NoMinOrder.infinite instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial vadd_left_injective
instNontrivial 📖	mathematical	—	Nontrivial UpperHalfPlane	—	Infinite.instNontrivial instInfinite
isOpen_upperHalfPlaneSet 📖	mathematical	—	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField upperHalfPlaneSet	—	isOpen_lt OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_const Complex.continuous_im
mem_slitPlane 📖	mathematical	—	Complex Set Set.instMembership Complex.slitPlane coe	—	im_ne_zero
mk_coe 📖	mathematical	Real Real.instLT Real.instZero Complex.im coe coe_im_pos	coe	—	—
mk_im 📖	mathematical	Real Real.instLT Real.instZero Complex.im	im Complex.im	—	—
mk_re 📖	mathematical	Real Real.instLT Real.instZero Complex.im	re Complex.re	—	—
ne_int 📖	—	—	—	—	ne_intCast
ne_intCast 📖	—	—	—	—	ne_ofReal
ne_nat 📖	—	—	—	—	ne_natCast
ne_natCast 📖	—	—	—	—	Int.cast_natCast ne_intCast
ne_ofReal 📖	—	—	—	—	—
ne_zero 📖	—	—	—	—	im_ne_zero
normSq_ne_zero 📖	—	—	—	—	LT.lt.ne' normSq_pos
normSq_pos 📖	mathematical	—	Real Real.instLT Real.instZero DFunLike.coe MonoidWithZeroHom Complex NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring Real.semiring MonoidWithZeroHom.funLike Complex.normSq coe	—	Complex.normSq_pos ne_zero
pos_real_im 📖	mathematical	—	im Real Real.instLT Real.instZero UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Positive.instMonoidSubtypeLtOfNat Real.semiring Real.partialOrder Real.instIsStrictOrderedRing MulAction.toSemigroupAction posRealAction Real.instMul	—	Complex.smul_im
pos_real_re 📖	mathematical	—	re Real Real.instLT Real.instZero UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Positive.instMonoidSubtypeLtOfNat Real.semiring Real.partialOrder Real.instIsStrictOrderedRing MulAction.toSemigroupAction posRealAction Real.instMul	—	Complex.smul_re
pos_real_smul_injective 📖	mathematical	—	Real Real.instLT Real.instZero UpperHalfPlane SemigroupAction.toSMul Monoid.toSemigroup Positive.instMonoidSubtypeLtOfNat Real.semiring Real.partialOrder Real.instIsStrictOrderedRing MulAction.toSemigroupAction posRealAction	—	Real.instIsStrictOrderedRing IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero instIsDomain
range_coe 📖	mathematical	—	Set.range Complex UpperHalfPlane coe upperHalfPlaneSet	—	Set.ext
re_add_im 📖	mathematical	—	Complex Complex.instAdd Complex.ofReal re Complex.instMul im Complex.I coe	—	Complex.re_add_im
vadd_im 📖	mathematical	—	im HVAdd.hVAdd Real UpperHalfPlane instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal	—	zero_add
vadd_left_injective 📖	mathematical	—	Real UpperHalfPlane HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal	—	—
vadd_re 📖	mathematical	—	re HVAdd.hVAdd Real UpperHalfPlane instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal Real.instAdd	—	—
vadd_right_cancel_iff 📖	mathematical	—	HVAdd.hVAdd Real UpperHalfPlane instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup Real.instAddMonoid AddAction.toAddSemigroupAction instAddActionReal	—	AddRightCancelSemigroup.toIsRightCancelAdd

(root)

Definitions

Name	Category	Theorems
UpperHalfPlane 📖	CompData	438 math math: CuspFormClass.qExpansion_isBigO, ModularForm.coe_mul, UpperHalfPlane.instSFiniteComapComplexCoeVolume, Derivative.serreDerivative_smul, UpperHalfPlane.mdifferentiable_num, ModularForm.mul_slash_SL2, ModularGroup.SLOnGLPos_smul_apply, ModularForm.smul_slash, CuspFormClass.holo, SlashInvariantForm.coe_prodEqualWeights, ModularFormClass.differentiableAt_comp_ofComplex, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, ModularFormClass.hasFPowerSeries_cuspFunction, CuspForm.toFun_eq_coe, qExpansion_eq_zero_iff, SlashInvariantForm.slash_action_eq', ModularForm.mul_slash, UpperHalfPlane.instContinuousSMulGL2R, qExpansionRingHom_apply, CuspFormClass.zero_at_infty_comp_ofComplex, UpperHalfPlane.image_coe_sphere, ModularGroup.coe_fd, ModularForm.constℝ_apply, UpperHalfPlane.im_div_exp_dist_le, UpperHalfPlane.re_smul, OnePoint.isBoundedAt_iff_exists_SL2Z, UpperHalfPlane.analyticAt_smul, UpperHalfPlane.isOpenEmbedding_coe, UpperHalfPlane.instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume, UpperHalfPlane.deriv_smul, UpperHalfPlane.comp_ofComplex_of_im_pos, UpperHalfPlane.tendsto_smul_atImInfty, UpperHalfPlane.dist_le_iff_dist_coe_center_le, UpperHalfPlane.subset_verticalStrip_of_isCompact, UpperHalfPlane.isOpenMap_norm, SlashInvariantForm.quotientFunc_mk, ModularForm.SL_slash, UpperHalfPlane.im_smul_eq_div_normSq, UpperHalfPlane.instSigmaFiniteComapComplexCoeVolume, UpperHalfPlane.specialLinearGroup_apply, SlashInvariantForm.coe_constℝ, SlashInvariantForm.smul_applyℝ, UpperHalfPlane.isOpenMap_im, UpperHalfPlane.canLift, Derivative.normalizedDerivOfComplex_smul, ModularForm.coe_constℝ, Derivative.normalizedDerivOfComplex_sub, ModularForm.prod_slash, ModularGroup.one_lt_normSq_T_zpow_smul, UpperHalfPlane.isometry_real_vadd, UpperHalfPlane.prod_eq_zero_iff, SlashInvariantForm.add_apply, CuspForm.zero_apply, ModularForm.discriminant_bounded_factor, ModularForm.norm_eq_zero_iff, Continuous.upperHalfPlaneMk, SlashInvariantFormClass.eq_cuspFunction, ModularForm.prod_slash_sum_weights, jacobiTheta_T_sq_smul, OnePoint.isBoundedAt_iff_forall_SL2Z, SlashInvariantForm.quotientFunc_smul, SlashInvariantForm.constℝ_toFun, ModularGroup.sl_moeb, CuspFormClass.zero_at_cusps, SlashInvariantForm.one_coe_eq_one, OnePoint.isZeroAt_iff_exists_SL2Z, SlashInvariantForm.smul_apply, SlashInvariantForm.coe_smulℝ, EisensteinSeries.E2_slash_action, UpperHalfPlane.isometry_vertical_line, CuspForm.coe_trace, UpperHalfPlane.glPos_smul_def, UpperHalfPlane.coe_pos_real_smul, ModularGroup.coe_T_zpow_smul_eq, UpperHalfPlane.comp_ofComplex, ModularForm.coe_neg, CuspForm.coeHom_apply, EisensteinSeries.G2_slash_action, SlashInvariantForm.const_toFun, UpperHalfPlane.denom_cocycle_σ, UpperHalfPlane.isOpenMap_re, UpperHalfPlane.mdifferentiable_inv_denom, ModularGroup.tendsto_abs_re_smul, UpperHalfPlane.dist_eq_iff_eq_sinh, SlashInvariantForm.coe_translate, UpperHalfPlane.ofComplex_apply_of_im_nonpos, UpperHalfPlane.dist_log_im_le, SlashInvariantForm.ext_iff, ModularGroup.exists_max_im, ModularFormClass.levelOne_neg_weight_eq_zero, ModularFormClass.continuous, UpperHalfPlane.im_le_im_mul_exp_dist, qExpansion_of_mul, UpperHalfPlane.contMDiff_coe, CuspForm.holo', UpperHalfPlane.vadd_re, UpperHalfPlane.dist_eq_iff_eq_sq_sinh, ModularGroup.im_T_smul, CuspFormClass.petersson_bounded_left, UpperHalfPlane.isPretransitiveGL2R, UpperHalfPlane.zero_form_isBoundedAtImInfty, UpperHalfPlane.instLocPathConnectedSpace, ModularForm.coe_natCast, UpperHalfPlane.image_coe_ball, cuspFunction_smul, UpperHalfPlane.contMDiff_inv_denom, ModularForm.coe_prodEqualWeights, UpperHalfPlane.dist_triangle, UpperHalfPlane.dist_of_re_eq, UpperHalfPlane.instT4Space, Derivative.normalizedDerivOfComplex_const, Derivative.serreDerivative_add, UpperHalfPlane.volume_def, ModularGroup.fdo_subset_fd, UpperHalfPlane.cosh_dist, UpperHalfPlane.image_coe_closedBall, EisensteinSeries.G2_S_transform, UpperHalfPlane.isProperMap_smul_I, UpperHalfPlane.instNoncompactSpace, SlashInvariantForm.sub_apply, ModularGroup.SL_to_GL_tower, ModularForm.zero_apply, UpperHalfPlane.dist_coe_center, UpperHalfPlane.ofComplex_apply_of_im_pos, qExpansion_one, jacobiTheta_S_smul, CuspForm.coe_smul, UpperHalfPlane.instContractibleSpace, cuspFunction_neg, ModularGroup.re_T_smul, UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left, UpperHalfPlane.hasStrictDerivAt_smul, UpperHalfPlane.exists, ModularForm.toSlashInvariantForm_coe, SlashInvariantForm.coe_mk, UpperHalfPlane.lt_dist_iff_lt_dist_coe_center, UpperHalfPlane.coe_smul_of_det_pos, CuspFormClass.zero_at_infty, CuspForm.coe_neg, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero, UpperHalfPlane.modular_S_smul, ModularGroup.re_T_inv_smul, EisensteinSeries.D2_inv, UpperHalfPlane.dist_lt_iff_dist_coe_center_lt, SlashInvariantForm.exists_one_half_le_im_and_norm_le, SlashInvariantForm.slash_action_generators, EisensteinSeries.q_expansion_riemannZeta, SlashInvariantFormClass.periodic_comp_ofComplex, OnePoint.isZeroAt_iff_forall_SL2Z, UpperHalfPlane.contMDiff_num, UpperHalfPlane.mdifferentiable_denom, OnePoint.isBoundedAt_iff, ModularForm.one_coe_eq_one, ModularGroup.fd_eq_closure_fdo, UpperHalfPlane.im_smul, OnePoint.IsZeroAt.smul_iff, ModularGroup.normSq_S_smul_lt_one, ModularFormClass.exp_decay_sub_atImInfty, ModularForm.sub_apply, ModularFormClass.exists_petersson_le, UpperHalfPlane.coe_smul, UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty, ModularGroup.exists_row_one_eq_and_min_re, UpperHalfPlane.ofComplex_apply_eq_of_im_nonpos, UpperHalfPlane.instIsFiniteMeasureOnCompactsComapComplexCoeVolume, ModularForm.ext_iff, UpperHalfPlane.instProperSMul, SlashInvariantForm.coe_sub, ModularForm.const_toFun, ModularGroup.re_T_zpow_smul, UpperHalfPlane.dist_eq, MDifferentiable.slash, Derivative.normalizedDerivOfComplex_mul, CuspForm.coe_translate, CuspFormClass.petersson_bounded_right, ModularFormClass.bdd_at_infty, OnePoint.IsZeroAt.add, ModularFormClass.exists_bound, ModularForm.neg_apply, ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo, ModularGroup.im_lt_im_S_smul, ModularForm.eq_const_of_weight_zero, qExpansion_sub, SlashInvariantForm.coe_prod, SlashInvariantForm.coe_natCast, Derivative.serreDerivative_sub, UpperHalfPlane.ofComplex_apply_eq_ite, UpperHalfPlane.volume_eq_lintegral, UpperHalfPlane.isPretransitiveSL2R, ModularGroup.im_T_zpow_smul, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, UpperHalfPlane.qParam_tendsto_atImInfty, UpperHalfPlane.dist_eq_iff_dist_coe_center_eq, ModularForm.coe_eq_zero_iff, ModularForm.coeHom_apply, ModularForm.slash_action_eq'_iff, UpperHalfPlane.petersson_continuous, UpperHalfPlane.pos_real_smul_injective, cuspFunction_mul, UpperHalfPlane.J_smul, SlashInvariantForm.slash_action_eqn'', UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center, ModularFormClass.qExpansion_coeff_zero, EisensteinSeries.eisensteinSeries_SIF_apply, CuspForm.coe_sub, UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left, UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal, CuspForm.neg_apply, UpperHalfPlane.le_dist_coe, UpperHalfPlane.instSFiniteVolume, ModularFormClass.differentiableAt_cuspFunction, ModularGroup.exists_one_half_le_im_smul, UpperHalfPlane.contMDiff_denom_zpow, qExpansion_add, ModularGroup.fdo_eq_interior_fd, UpperHalfPlane.petersson_slash_SL, ModularGroup.isOpen_fdo, UpperHalfPlane.le_dist_iff_le_dist_coe_center, SlashInvariantForm.toFun_eq_coe, ModularForm.SL_slash_def, UpperHalfPlane.ofComplex_apply, UpperHalfPlane.instLocallyCompactSpace, UpperHalfPlane.continuous_toSL2R, cuspFunction_add, SlashInvariantForm.coe_zero, UpperHalfPlane.coe_J_smul, ModularForm.IsGLPos.coe_smul, UpperHalfPlane.dist_comm, UpperHalfPlane.dist_center_dist, UpperHalfPlane.atImInfty_mem, UpperHalfPlane.instIsLocallyFiniteMeasureVolume, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero, UpperHalfPlane.eq_zero_of_frequently, UpperHalfPlane.dist_le_dist_coe_div_sqrt, OnePoint.IsBoundedAt.smul_iff, CuspFormClass.exists_bound, UpperHalfPlane.pos_real_re, UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex, ModularForm.IsGLPos.smul_apply, SlashInvariantForm.coe_trace, EisensteinSeries.E_qExpansion_coeff, UpperHalfPlane.eventuallyEq_coe_comp_ofComplex, SlashInvariantForm.coe_neg, CuspForm.ext_iff, SlashInvariantForm.slash_action_eqn_SL'', UpperHalfPlane.comp_ofComplex_of_im_le_zero, UpperHalfPlane.continuous_im, ModularFormClass.hasSum_qExpansion_of_abs_lt, UpperHalfPlane.atImInfty_basis, UpperHalfPlane.meromorphicOrderAt_comp_smul, UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip, UpperHalfPlane.verticalStrip_anti_right, EisensteinSeries.q_expansion_bernoulli, UpperHalfPlane.coe_specialLinearGroup_apply, EisensteinSeries.D2_one, ModularFormClass.levelOne_weight_zero_const, ModularGroup.im_smul_eq_div_normSq, UpperHalfPlane.cosh_half_dist, Derivative.serreDerivative_mul, SlashInvariantForm.slash_action_generators_SL2Z, hasFPowerSeriesOnBall_cuspFunction, UpperHalfPlane.exp_half_dist, ModularFormClass.qExpansion_coeff_eq_circleIntegral, UpperHalfPlane.vadd_right_cancel_iff, CuspForm.coe_zero, ModularForm.coe_prod, EisensteinSeries.tendsto_double_sum_S_act, ModularForm.smul_apply, UpperHalfPlane.coe_injective, Derivative.normalizedDerivOfComplex_mdifferentiable, ModularForm.discriminant_T_invariant, qExpansion_neg, ModularForm.const_apply, OnePoint.IsBoundedAt.add, SlashInvariantForm.slash_S_apply, ModularForm.coe_intCast, UpperHalfPlane.instSigmaFiniteVolume, UpperHalfPlane.verticalStrip_mono, UpperHalfPlane.sinh_half_dist_add_dist, ModularForm.coe_norm, UpperHalfPlane.instNeBotAtImInfty, UpperHalfPlane.mul_eq_zero_iff, ModularFormClass.qExpansion_isBigO, UpperHalfPlane.instBorelSpace, UpperHalfPlane.instT3Space, CuspForm.IsGLPos.smul_apply, qExpansion_mul, mdifferentiable_jacobiTheta, ModularForm.coe_add, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, cuspFunction_sub, CuspForm.sub_apply, ModularFormClass.bdd_at_cusps, Derivative.normalizedDerivOfComplex_neg, ModularForm.coe_const, qExpansion_mul_coeff_zero, ModularForm.cuspFunction_mul, UpperHalfPlane.contMDiffAt_ofComplex, ModularForm.prod_fintype_slash, ModularFormClass.bounded_at_infty_comp_ofComplex, CuspFormClass.exp_decay_atImInfty', ModularForm.holo', CuspForm.IsGLPos.coe_smul, ModularForm.discriminant_S_invariant, Derivative.normalizedDerivOfComplex_add, SlashInvariantForm.vAdd_width_periodic, UpperHalfPlane.coe_vadd, UpperHalfPlane.instSecondCountableTopology, ModularGroup.exists_smul_mem_fd, ModularFormClass.hasSum_qExpansion_of_norm_lt, ModularFormClass.bdd_at_infty_slash, UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty', ModularFormClass.cuspFunction_apply_zero, qExpansion_coeff_unique, UpperHalfPlane.contMDiffAt_iff, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, UpperHalfPlane.instProperSpace, CuspFormClass.cuspFunction_apply_zero, ModularForm.slash_def, UpperHalfPlane.instContinuousGLSMul, CuspFormClass.zero_at_infty_slash, ModularForm.is_invariant_one', UpperHalfPlane.measurableEmbedding_coe, EisensteinSeries.eisensteinSeriesSIF_apply, ModularGroup.im_T_inv_smul, UpperHalfPlane.mdifferentiable_coe, SlashInvariantFormClass.norm_petersson_smul, EisensteinSeries.eisSummand_extension_differentiableOn, ModularFormClass.analyticAt_cuspFunction_zero, UpperHalfPlane.modular_T_zpow_smul, SlashInvariantForm.coe_add, UpperHalfPlane.dist_coe_le, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, ModularFormClass.differentiableOn_cuspFunction_ball, ModularFormClass.holo, UpperHalfPlane.pos_real_im, UpperHalfPlane.sinh_half_dist, UpperHalfPlane.dist_le_iff_le_sinh, ModularForm.is_invariant_const, ModularForm.SL_slash_apply, UpperHalfPlane.dist_coe_center_sq, EisensteinSeries.eisSummand_SL2_apply, UpperHalfPlane.mem_verticalStrip_iff, UpperHalfPlane.tendsto_coe_atImInfty, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, UpperHalfPlane.instInfinite, SlashInvariantForm.slash_action_eqn', UpperHalfPlane.cosh_dist', SlashInvariantForm.coe_smul, ModularForm.qExpansion_mul, UpperHalfPlane.mdifferentiableAt_iff, UpperHalfPlane.IsZeroAtImInfty.slash, EisensteinSeries.E_qExpansion_coeff_zero, CuspFormClass.exp_decay_atImInfty, qExpansion_zero, UpperHalfPlane.tanh_half_dist, ModularForm.coe_translate, ModularForm.coe_smul, UpperHalfPlane.neg_smul, ModularForm.coe_sub, Derivative.normalizedDerivOfComplex_pow, ModularForm.toFun_eq_coe, SlashInvariantFormClass.petersson_smul, SlashInvariantForm.neg_apply, UpperHalfPlane.verticalStrip_mono_left, ModularForm.coe_trace, ModularGroup.coe_fdo, UpperHalfPlane.range_coe, SlashInvariantForm.coe_const, SlashInvariantForm.coeHom_injective, EisensteinSeries.eisensteinSeries_slash_apply, UpperHalfPlane.instContinuousSMulSL2R, SlashInvariantForm.coe_mul, UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right, ModularGroup.isClosed_coe_fd, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, ModularForm.coe_zero, UpperHalfPlane.contMDiff_smul, UpperHalfPlane.tendsto_comap_im_ofComplex, UpperHalfPlane.contMDiff_denom, E2_mdifferentiable, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, UpperHalfPlane.isometry_pos_mul, qExpansion_of_pow, UpperHalfPlane.toSL2R_smul_I, OnePoint.isZeroAt_iff, ModularForm.add_apply, qExpansion_smul, UpperHalfPlane.mdifferentiable_denom_zpow, UpperHalfPlane.instIsLocallyFiniteMeasureComapComplexCoeVolume, SlashInvariantFormClass.slash_action_eq, SlashInvariantForm.slash_action_eqn, ModularFormClass.hasSum_qExpansion, qExpansion_coeff_isBigO_of_norm_isBigO, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, ModularGroup.SL_neg_smul, UpperHalfPlane.continuous_coe, Derivative.serreDerivative_mdifferentiable, UpperHalfPlane.hasStrictFDerivAt_smul, UpperHalfPlane.mdifferentiable_iff, ModularFormClass.exp_decay_sub_atImInfty', UpperHalfPlane.isEmbedding_coe, SlashInvariantForm.vAdd_apply_of_mem_strictPeriods, ModularForm.is_invariant_one, ModularForm.mul_coe, EisensteinSeries.D2_T, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, UpperHalfPlane.instIsFiniteMeasureOnCompactsVolume, UpperHalfPlane.mdifferentiableAt_ofComplex, UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_right, SlashInvariantForm.coe_norm, EisensteinSeries.D2_mul, ModularGroup.exists_eq_T_zpow_of_c_eq_zero, UpperHalfPlane.vadd_im, UpperHalfPlane.measurable_coe, CuspForm.coe_add, CuspForm.toSlashInvariantForm_coe, CuspForm.smul_apply, UpperHalfPlane.instNontrivial, UpperHalfPlane.modular_T_smul, UpperHalfPlane.IsBoundedAtImInfty.slash, SlashInvariantForm.coe_intCast, ModularGroup.isClosed_fd, ModularGroup.smul_eq_lcRow0_add, UpperHalfPlane.vadd_left_injective, ModularForm.constℝ_toFun, ModularForm.SL_smul_slash, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, UpperHalfPlane.mdifferentiable_smul, ModularForm.slash_apply, ModularGroup.isCompact_truncatedFundamentalDomain, EisensteinSeries.G2_T_transform, CuspForm.add_apply, UpperHalfPlane.petersson_slash, ModularGroup.coe_truncatedFundamentalDomain, UpperHalfPlane.continuous_re

---

← Back to Index