feat(NumberTheory/Modular): interior and closure of fundamental domain by loefflerd · Pull Request #35946 · leanprover-community/mathlib4

loefflerd · 2026-03-01T23:53:25Z

Show that the open and closed fundamental domains for the modular group are related by the interior / closure operations.

github-actions · 2026-03-01T23:54:37Z

PR summary 693459cd7a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Modular	2097	2098	+1 (+0.05%)

Import changes for all files

Files	Import difference
`Mathlib.NumberTheory.Modular`	1

Declarations diff

+ coe_fd
+ coe_fdo
+ fd_eq_closure_fdo
+ fdo_eq_interior_fd
+ fdo_subset_fd
+ isClosed_coe_fd
+ isClosed_fd
+ isOpenMap_norm
+ isOpenMap_re
+ isOpen_fdo
+ mem_closure_of_arc
+ mem_closure_of_one_lt_norm
+ one_le_normSq_iff
+ one_lt_normSq_iff

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/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).

CBirkbeck

This all looks good, I only have these minor golfs.

CBirkbeck · 2026-03-03T13:28:35Z

Mathlib/NumberTheory/Modular.lean

+      have : ContinuousAt (fun a : ℝ ↦ (UpperHalfPlane.ofComplex (a * x : ℂ) : ℂ)) 1 := by
+        apply ContinuousAt.comp
+        · fun_prop
+        · apply ContinuousAt.comp
+          · apply OpenPartialHomeomorph.continuousAt
+            simpa [UpperHalfPlane.ofComplex] using x.coe_im_pos
+          · fun_prop


Suggested change

have : ContinuousAt (fun a : ℝ ↦ (UpperHalfPlane.ofComplex (a * x : ℂ) : ℂ)) 1 := by

apply ContinuousAt.comp

· fun_prop

· apply ContinuousAt.comp

· apply OpenPartialHomeomorph.continuousAt

simpa [UpperHalfPlane.ofComplex] using x.coe_im_pos

· fun_prop

have : ContinuousAt (fun a : ℝ ↦ (UpperHalfPlane.ofComplex (a * x : ℂ) : ℂ)) 1 := by

apply ContinuousAt.comp (by fun_prop)

apply ContinuousAt.comp _ (by fun_prop)

apply OpenPartialHomeomorph.continuousAt

simpa [UpperHalfPlane.ofComplex] using x.coe_im_pos

CBirkbeck · 2026-03-03T13:41:50Z

Mathlib/NumberTheory/Modular.lean

+    simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2
+
+end Topology
+


Suggested change

CBirkbeck · 2026-03-03T13:46:30Z

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

+    obtain ⟨w, -, hw⟩ := hεs this
+    exact w.ne_zero hw


Suggested change

obtain ⟨w, -, hw⟩ := hεs this

exact w.ne_zero hw

simpa [UpperHalfPlane.ne_zero] using hεs this

CBirkbeck · 2026-03-03T13:48:55Z

Mathlib/NumberTheory/Modular.lean

+      simp [← normSq_eq_norm_sq, normSq_apply]
+      ring
+    rw [hxnorm, one_pow, add_assoc, lt_add_iff_pos_right]
+    rw [← NNReal.coe_pos] at ha


Suggested change

rw [← NNReal.coe_pos] at ha

CBirkbeck · 2026-03-03T13:49:46Z

Mathlib/NumberTheory/Modular.lean

+    rw [UpperHalfPlane.isOpenEmbedding_coe.tendsto_nhds_iff, Function.comp_def]
+    dsimp only
+    rw [show 𝓝 (x : ℂ) = 𝓝 (x + (((0 : ℝ≥0) : ℝ) : ℂ) * Complex.I) by simp]
+    apply Continuous.tendsto
+    fun_prop


Suggested change

rw [UpperHalfPlane.isOpenEmbedding_coe.tendsto_nhds_iff, Function.comp_def]

dsimp only

rw [show 𝓝 (x : ℂ) = 𝓝 (x + (((0 : ℝ≥0) : ℝ) : ℂ) * Complex.I) by simp]

apply Continuous.tendsto

fun_prop

rw [UpperHalfPlane.isOpenEmbedding_coe.tendsto_nhds_iff, Function.comp_def,

show 𝓝 (x : ℂ) = 𝓝 (x + (((0 : ℝ≥0) : ℝ) : ℂ) * Complex.I) by simp]

apply Continuous.tendsto

fun_prop

CBirkbeck · 2026-03-03T13:51:46Z

Mathlib/NumberTheory/Modular.lean

+      have := this.tendsto
+      rw [UpperHalfPlane.ofComplex_apply_of_im_pos (by simpa using x.coe_im_pos)] at this
+      simpa


Suggested change

have := this.tendsto

rw [UpperHalfPlane.ofComplex_apply_of_im_pos (by simpa using x.coe_im_pos)] at this

simpa

simpa [UpperHalfPlane.ofComplex_apply_of_im_pos (by simpa using x.coe_im_pos)] using

this.tendsto

CBirkbeck · 2026-03-03T13:54:15Z

Mathlib/NumberTheory/Modular.lean

+lemma fdo_eq_interior_fd : 𝒟ᵒ = interior 𝒟 := by
+  refine subset_antisymm (isOpen_fdo.subset_interior_iff.mpr fdo_subset_fd) ?_
+  have ho1 := UpperHalfPlane.isOpenMap_re.image_interior_subset 𝒟
+  have ho2 := UpperHalfPlane.isOpenMap_norm.image_interior_subset 𝒟
+  intro x hx
+  constructor
+  · rw [Set.image_subset_iff] at ho2
+    have := ho2 hx
+    rw [Set.mem_preimage] at this
+    rw [one_lt_normSq_iff, ← Set.mem_Ioi, ← interior_Ici]
+    apply Set.mem_of_mem_of_subset this (interior_mono ?_)
+    rw [Set.image_subset_iff]
+    intro ξ hξ
+    simpa [Set.mem_preimage, Set.mem_Ici, one_le_normSq_iff] using hξ.1
+  · rw [Set.image_subset_iff] at ho1
+    have := ho1 hx
+    rw [Set.mem_preimage] at this
+    rw [abs_lt, ← Set.mem_Ioo, ← interior_Icc]
+    apply Set.mem_of_mem_of_subset this (interior_mono ?_)
+    rw [Set.image_subset_iff]
+    intro ξ hξ
+    simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2


Suggested change

lemma fdo_eq_interior_fd : 𝒟ᵒ = interior 𝒟 := by

refine subset_antisymm (isOpen_fdo.subset_interior_iff.mpr fdo_subset_fd) ?_

have ho1 := UpperHalfPlane.isOpenMap_re.image_interior_subset 𝒟

have ho2 := UpperHalfPlane.isOpenMap_norm.image_interior_subset 𝒟

intro x hx

constructor

· rw [Set.image_subset_iff] at ho2

have := ho2 hx

rw [Set.mem_preimage] at this

rw [one_lt_normSq_iff, ← Set.mem_Ioi, ← interior_Ici]

apply Set.mem_of_mem_of_subset this (interior_mono ?_)

rw [Set.image_subset_iff]

intro ξ hξ

simpa [Set.mem_preimage, Set.mem_Ici, one_le_normSq_iff] using hξ.1

· rw [Set.image_subset_iff] at ho1

have := ho1 hx

rw [Set.mem_preimage] at this

rw [abs_lt, ← Set.mem_Ioo, ← interior_Icc]

apply Set.mem_of_mem_of_subset this (interior_mono ?_)

rw [Set.image_subset_iff]

intro ξ hξ

simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2

lemma fdo_eq_interior_fd : 𝒟ᵒ = interior 𝒟 := by

refine subset_antisymm (isOpen_fdo.subset_interior_iff.mpr fdo_subset_fd) ?_

have ho1 := UpperHalfPlane.isOpenMap_re.image_interior_subset 𝒟

have ho2 := UpperHalfPlane.isOpenMap_norm.image_interior_subset 𝒟

intro x hx

rw [Set.image_subset_iff] at *

constructor

· rw [one_lt_normSq_iff, ← Set.mem_Ioi, ← interior_Ici]

apply Set.mem_of_mem_of_subset (Set.mem_preimage.mp (ho2 hx)) (interior_mono ?_)

rw [Set.image_subset_iff]

intro ξ hξ

simpa [Set.mem_preimage, Set.mem_Ici, one_le_normSq_iff] using hξ.1

· rw [abs_lt, ← Set.mem_Ioo, ← interior_Icc]

apply Set.mem_of_mem_of_subset ((Set.mem_preimage.mp (ho1 hx))) (interior_mono ?_)

rw [Set.image_subset_iff]

intro ξ hξ

simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2

feat(NumberTheory/Modular): interior and closure of fundamental domain

3463a71

loefflerd added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Mar 3, 2026

loefflerd requested a review from CBirkbeck March 3, 2026 11:46

CBirkbeck reviewed Mar 3, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(NumberTheory/Modular): interior and closure of fundamental domain#35946

feat(NumberTheory/Modular): interior and closure of fundamental domain#35946
loefflerd wants to merge 1 commit intoleanprover-community:masterfrom
loefflerd:DL_funDomain_closure

loefflerd commented Mar 1, 2026

Uh oh!

github-actions bot commented Mar 1, 2026

Import changes for modified files

Declarations diff

Uh oh!

CBirkbeck left a comment

Uh oh!

CBirkbeck Mar 3, 2026

Uh oh!

CBirkbeck Mar 3, 2026

Uh oh!

CBirkbeck Mar 3, 2026 •

edited

Loading

Uh oh!

CBirkbeck Mar 3, 2026

Uh oh!

CBirkbeck Mar 3, 2026

Uh oh!

CBirkbeck Mar 3, 2026

Uh oh!

CBirkbeck Mar 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2

		end Topology

	obtain ⟨w, -, hw⟩ := hεs this
	exact w.ne_zero hw
	simpa [UpperHalfPlane.ne_zero] using hεs this

Conversation

loefflerd commented Mar 1, 2026

Uh oh!

github-actions bot commented Mar 1, 2026

PR summary 693459cd7a

Import changes for modified files

Declarations diff

Uh oh!

CBirkbeck left a comment

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

CBirkbeck Mar 3, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

CBirkbeck Mar 3, 2026 •

edited

Loading