UniformConvergence

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

Statistics

Metric	Count
Definitions	0
Theorems eisensteinSeries_tendstoLocallyUniformly, eisensteinSeries_tendstoLocallyUniformlyOn	2
Total	2

EisensteinSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eisensteinSeries_tendstoLocallyUniformly 📖	mathematical	—	TendstoLocallyUniformly UpperHalfPlane Complex Finset Set.Elem gammaSet UpperHalfPlane.instTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup eisSummand Set Set.instMembership eisensteinSeries Filter.atTop PartialOrder.toPreorder Finset.partialOrder	—	Nat.instAtLeastTwoHAddOfNat Int.cast_ofNat IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.one Real.instNontrivial Real.rpow_intCast Summable.subtype instIsUniformAddGroupReal Real.instCompleteSpace summable_one_div_norm_rpow UpperHalfPlane.instLocallyCompactSpace UpperHalfPlane.subset_verticalStrip_of_isCompact TendstoUniformlyOn.mono tendstoUniformlyOn_tsum Complex.instCompleteSpace Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal norm_zpow Int.cast_neg summand_bound_of_mem_verticalStrip le_of_lt Int.cast_pos IsOrderedRing.toIsOrderedAddMonoid Real.instIsOrderedRing IsOrderedRing.toZeroLEOneClass lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
eisensteinSeries_tendstoLocallyUniformlyOn 📖	mathematical	—	TendstoLocallyUniformlyOn Complex Finset Set.Elem gammaSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField UpperHalfPlane Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup eisSummand Set Set.instMembership OpenPartialHomeomorph.toFun' UpperHalfPlane.instTopologicalSpace UpperHalfPlane.ofComplex DFunLike.coe SlashInvariantForm Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing CongruenceSubgroup.Gamma SlashInvariantForm.funLike eisensteinSeriesSIF Filter.atTop PartialOrder.toPreorder Finset.partialOrder setOf Real.instLT Real.instZero Complex.im	—	UpperHalfPlane.upperHalfPlaneSet.eq_1 UpperHalfPlane.range_coe Set.image_univ TendstoLocallyUniformlyOn.comp UpperHalfPlane.isOpenEmbedding_coe eisensteinSeries_tendstoLocallyUniformly Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target OpenPartialHomeomorph.continuousOn_symm

---

← Back to Index