feat(NumberTheory/ModularForms): arithmetic subgroups act properly discontinuously

[loefflerd]

Arithmetic subgroups (subgroups of GL(2, R) commensurable with SL(2, Z)) act properly discontinuously on the upper half-plane.

---

• depends on: feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n) #37601

[github-actions]

PR summary fb17c7c573

Import changes exceeding 2%

%	File
+22.84%	Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups	1922	2361	+439 (+22.84%)

Import changes for all files

Files	Import difference
8 files Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion	99
Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs	100
Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace	102
5 files Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.QExpansion	103
Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable	104
Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence	191
Mathlib.NumberTheory.ModularForms.BoundedAtCusp	241
Mathlib.NumberTheory.ModularForms.Identities	327
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.SlashInvariantForms	332
Mathlib.NumberTheory.ModularForms.Cusps	343
Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups Mathlib.NumberTheory.ModularForms.CongruenceSubgroups	439
Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (new file)	978

---

Declarations diff

+ ProperlyDiscontinuousSMul.ofFiniteRelIndex
+ Subgroup.Commensurable.properlyDiscontinuousSMul_iff
+ Subgroup.IsArithmetic.properlyDiscontinuous
+ Subgroup.properlyDiscontinuousSMul_iff
+ Subgroup.properlyDiscontinuousSMul_iff_of_isFiniteRelIndex
+ Subgroup.properlyDiscontinuousSMul_of_le
+ Topology.IsClosedEmbedding.prodMap
+ _root_.Continuous.generalLinearGroup_map
+ _root_.Continuous.specialLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.generalLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.specialLinearGroup_map
+ _root_.Topology.IsClosedEmbedding.units_map
+ _root_.Topology.IsEmbedding.generalLinearGroup_map
+ _root_.Topology.IsEmbedding.specialLinearGroup_map
+ _root_.Topology.IsEmbedding.units_map
+ _root_.Topology.IsInducing.generalLinearGroup_map
+ _root_.Topology.IsInducing.specialLinearGroup_map
+ _root_.Topology.IsInducing.units_map
+ closedEmbedding_intCast
+ continuous_mapGL
+ discreteSpecialLinearGroupIntRangeSL
+ instProperlyDiscontinuousSL2RSubgroup
+ instT1Space
+ instance [SMul Γ α] [ProperlyDiscontinuousSMul Γ α] (G : Subgroup Γ) :
+ isClosedEmbedding_mapGL
+ isClosed_range_intCast
+ isOpen_compl_range_intCast
+ isometry_intCast
+ properlyDiscontinuousSL2ZRange

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
6899	-2	backward.isDefEq.respectTransparency

Current commit ca010600a2
Reference commit fb17c7c573

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n) #37601
  By Dependent Issues (🤖). Happy coding!