[Merged by Bors] - feat(Topology/Instances/AddCircle): add Ioc analogues of lift and equiv lemmas by pitmonticone · Pull Request #37570 · leanprover-community/mathlib4

pitmonticone · 2026-04-02T19:34:46Z

Add AddCircle lemmas:

liftIoc_eq_liftIco_of_ne: the Ioc and Ico lifts agree away from the basepoint
coe_eq_coe_iff_of_mem_Ioc: Ioc analogue of coe_eq_coe_iff_of_mem_Ico
eq_coe_Ioc: Ioc analogue of eq_coe_Ico
coe_equivIoc: Ioc analogue of coe_equivIco
equivIoc_coe_of_mem: if y ∈ Ioc a (a + p), then equivIoc p a y = y

Upstreamed from the Carleson project.

Co-authored-by: James Sundstrom [email protected]
Co-authored-by: Leo Diedering [email protected]

…iv lemmas Add Ioc analogues of existing AddCircle Ico lemmas: - `liftIoc_eq_liftIco_of_ne` - `coe_eq_coe_iff_of_mem_Ioc` - `eq_coe_Ioc` - `coe_equivIoc` - `equivIoc_coe_of_mem` Upstreamed from the [Carleson](https://github.com/fpvandoorn/carleson) project. Co-authored-by: James Sundstrom <[email protected]> Co-authored-by: Leo Diedering <[email protected]>

github-actions · 2026-04-02T19:35:48Z

PR summary 91f509a196

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ coe_eq_coe_iff_of_mem_Ioc
+ coe_equivIco
+ coe_equivIoc
+ eq_coe_Ioc
+ equivIco_coe_of_mem
+ equivIoc_coe_of_mem
+ liftIoc_eq_liftIco_of_ne

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.

No changes to technical debt.

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

loefflerd · 2026-04-04T16:31:47Z

Add Ioc analogues of existing AddCircle Ico lemmas:
liftIoc_eq_liftIco_of_ne
coe_eq_coe_iff_of_mem_Ioc
eq_coe_Ioc
coe_equivIoc
equivIoc_coe_of_mem

I'm a little puzzled by the PR description since of these five lemmas, only three of them seem to have existing Ico counterparts: we have AddCircle.coe_eq_coe_iff_of_mem_Ico, AddCircle.eq_coe_Ico, and AddCircle.coe_equivIco, so it makes perfect sense to add the Ioc counterparts; but the others don't seem to match anything in the library, there is no equivIco_coe_of_mem. (There is a similar lemma docs#AddCircle.equivIco_coe_eq but that has an Ioc analogue already.)

pitmonticone · 2026-04-04T21:59:36Z

Good point, thanks! Updated the PR description. Only coe_eq_coe_iff_of_mem_Ioc, eq_coe_Ioc, and coe_equivIoc are direct Ioc analogues. The other two (liftIoc_eq_liftIco_of_ne and equivIoc_coe_of_mem) are new standalone lemmas.

loefflerd · 2026-04-06T12:09:55Z

+    (equivIoc p a y : AddCircle p) = y :=
+  (equivIoc p a).left_inv y
+
+lemma equivIoc_coe_of_mem {y : 𝕜} (hy : y ∈ Set.Ioc a (a + p)) :


Same for this one: we should have both Ioc and Ico versions (but this one shouldn't get a simp flag).

loefflerd · 2026-04-06T12:18:33Z

+  have x_eq_b : x = ↑b :=
+    (QuotientAddGroup.equivIcoMod hp.out a).apply_eq_iff_eq_symm_apply.mp rfl
+  rw [x_eq_b, liftIco_coe_apply b.coe_prop]
+  exact liftIoc_coe_apply ⟨lt_of_le_of_ne b.coe_prop.1 (x_ne_a <| · ▸ x_eq_b), b.coe_prop.2.le⟩


Suggested change

exact liftIoc_coe_apply ⟨lt_of_le_of_ne b.coe_prop.1 (x_ne_a <| · ▸ x_eq_b), b.coe_prop.2.le⟩

exact liftIoc_coe_apply (by grind)

loefflerd · 2026-04-06T12:23:06Z

+  have x_eq_b : x = ↑b :=
+    (QuotientAddGroup.equivIcoMod hp.out a).apply_eq_iff_eq_symm_apply.mp rfl


If you add missing Ico lemma above this becomes just

Suggested change

have x_eq_b : x = ↑b :=

(QuotientAddGroup.equivIcoMod hp.out a).apply_eq_iff_eq_symm_apply.mp rfl

have x_eq_b : x = ↑b := coe_equivIco.symm

loefflerd · 2026-04-06T12:23:52Z

    (QuotientAddGroup.equivIcoMod hp.out 0).symm_apply_apply a⟩

+/-- Ioc version of `eq_coe_Ico`. -/
+lemma eq_coe_Ioc (a : AddCircle p) : ∃ b ∈ Set.Ioc 0 p, ↑b = a := by


Suggested change

lemma eq_coe_Ioc (a : AddCircle p) : ∃ b ∈ Set.Ioc 0 p, ↑b = a := by

lemma eq_coe_Ioc (a : AddCircle p) : ∃ b ∈ Ioc 0 p, ↑b = a := by

loefflerd · 2026-04-06T12:25:16Z

+theorem liftIoc_eq_liftIco_of_ne (f : 𝕜 → B) {x : AddCircle p}
+    (x_ne_a : x ≠ a) : liftIoc p a f x = liftIco p a f x := by


f can be implicit (inferrable from either side of the equality)

Suggested change

theorem liftIoc_eq_liftIco_of_ne (f : 𝕜 → B) {x : AddCircle p}

(x_ne_a : x ≠ a) : liftIoc p a f x = liftIco p a f x := by

theorem liftIoc_eq_liftIco_of_ne {f : 𝕜 → B} {x : AddCircle p} (x_ne_a : x ≠ a) :

liftIoc p a f x = liftIco p a f x := by

loefflerd · 2026-04-06T12:26:03Z

+    (equivIoc p a y : AddCircle p) = y :=
+  (equivIoc p a).left_inv y
+
+lemma equivIoc_coe_of_mem {y : 𝕜} (hy : y ∈ Set.Ioc a (a + p)) :


Suggested change

lemma equivIoc_coe_of_mem {y : 𝕜} (hy : y ∈ Set.Ioc a (a + p)) :

lemma equivIoc_coe_of_mem {y : 𝕜} (hy : y ∈ Ioc a (a + p)) :

(and elsewhere)

…lifts

…[simp], fix Set. prefix

…icone/mathlib4 into carleson/AddCircle-lifts

pitmonticone · 2026-04-07T10:05:51Z

Thank you @loefflerd. I should have addressed all your review comments.

…icone/mathlib4 into carleson/AddCircle-lifts

Update the upstreaming status comments for files that have been PRed to mathlib: - `Analysis/MeanInequalitiesPow` leanprover-community/mathlib4#37547 - `Order/LiminfLimsup` leanprover-community/mathlib4#37549 (merged) - `Topology/Order/Basic` leanprover-community/mathlib4#37550 (moved to DenselyOrdered) - `MeasureTheory/Integral/Average` leanprover-community/mathlib4#37551 - `MeasureTheory/Measure/ENNReal` leanprover-community/mathlib4#37552 (generalized to `measurable_iSup_of_lowerSemicontinuous`) - `MeasureTheory/Integral/Lebesgue` leanprover-community/mathlib4#37558 (merged) - `MeasureTheory/Function/LpSpace/Indicator` leanprover-community/mathlib4#37559 - `MeasureTheory/Function/LpSpace/ContinuousFunctions` leanprover-community/mathlib4#37560 - `Data/ENNReal` leanprover-community/mathlib4#37565 (partial) - `MeasureTheory/Integral/Bochner/ContinuousLinearMap` leanprover-community/mathlib4#37568 (partial) - `Topology/Instances/AddCircle/Defs` leanprover-community/mathlib4#37570 (partial) - `Discrete/SumEstimates` leanprover-community/mathlib4#37597 Also notes that `IntegrableAtFilter.congr` and `integrableOn_of_integrableOn_inter_support` already exist in mathlib.

loefflerd

LGTM – just a tiny formatting nit to finish

maintainer delegate

github-actions · 2026-04-09T17:17:13Z

🚀 Pull request has been placed on the maintainer queue by loefflerd.

Co-authored-by: David Loeffler <[email protected]>

faenuccio

Thanks, I left a couple of stylistic comments, but then you can go.

faenuccio · 2026-04-10T17:49:52Z

bors d+

mathlib-bors · 2026-04-10T17:49:55Z

✌️ pitmonticone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Filippo A. E. Nuccio <[email protected]>

pitmonticone · 2026-04-10T19:08:19Z

bora r+

loefflerd · 2026-04-10T19:09:59Z

@pitmonticone I think you may have a typo

pitmonticone · 2026-04-10T19:10:46Z

Ops, thanks!

pitmonticone · 2026-04-10T19:11:02Z

bors r+

…iv lemmas (#37570) Add AddCircle lemmas: - `liftIoc_eq_liftIco_of_ne`: the Ioc and Ico lifts agree away from the basepoint - `coe_eq_coe_iff_of_mem_Ioc`: Ioc analogue of `coe_eq_coe_iff_of_mem_Ico` - `eq_coe_Ioc`: Ioc analogue of `eq_coe_Ico` - `coe_equivIoc`: Ioc analogue of `coe_equivIco` - `equivIoc_coe_of_mem`: if `y ∈ Ioc a (a + p)`, then `equivIoc p a y = y` Upstreamed from the [Carleson](https://github.com/fpvandoorn/carleson) project. Co-authored-by: James Sundstrom <[email protected]> Co-authored-by: Leo Diedering <[email protected]> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-04-10T20:22:48Z

Pull request successfully merged into master.

Build succeeded:

pitmonticone added carleson part of the ongoing formalization of Carleson's theorem easy < 20s of review time. See the lifecycle page for guidelines. labels Apr 2, 2026

github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Apr 2, 2026

pitmonticone mentioned this pull request Apr 2, 2026

chore(ToMathlib): note upstreaming status for 8 files fpvandoorn/carleson#548

Merged

mathlib-triage bot assigned loefflerd Apr 3, 2026

loefflerd added awaiting-author A reviewer has asked the author a question or requested changes. and removed easy < 20s of review time. See the lifecycle page for guidelines. labels Apr 4, 2026

Merge branch 'master' into carleson/AddCircle-lifts

991f265

pitmonticone removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 4, 2026

loefflerd reviewed Apr 6, 2026

View reviewed changes

loefflerd added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 6, 2026

pitmonticone added 3 commits April 7, 2026 10:59

Merge remote-tracking branch 'origin/master' into carleson/AddCircle-…

c3ac04b

…lifts

address review: add Ico versions, make f implicit, golf proofs, add @…

564d775

…[simp], fix Set. prefix

Merge branch 'carleson/AddCircle-lifts' of https://github.com/pitmont…

9c59c91

…icone/mathlib4 into carleson/AddCircle-lifts

pitmonticone added 3 commits April 7, 2026 11:07

Merge branch 'master' into carleson/AddCircle-lifts

1a51f87

chore: match eq_coe_Ico binder style to eq_coe_Ioc

7d2ebfa

Merge branch 'carleson/AddCircle-lifts' of https://github.com/pitmont…

d76e82f

…icone/mathlib4 into carleson/AddCircle-lifts

pitmonticone removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 7, 2026

loefflerd reviewed Apr 9, 2026

View reviewed changes

Comment thread Mathlib/Topology/Instances/AddCircle/Defs.lean Outdated

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 9, 2026

pitmonticone and others added 2 commits April 9, 2026 20:39

Update Mathlib/Topology/Instances/AddCircle/Defs.lean

72f34ec

Co-authored-by: David Loeffler <[email protected]>

[pre-commit.ci lite] apply automatic fixes

cc9bf0f

faenuccio reviewed Apr 10, 2026

View reviewed changes

Comment thread Mathlib/Topology/Instances/AddCircle/Defs.lean Outdated

mathlib-triage bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 10, 2026

Update Defs.lean

b1ba0f4

Co-authored-by: Filippo A. E. Nuccio <[email protected]>

mathlib-bors bot changed the title ~~feat(Topology/Instances/AddCircle): add Ioc analogues of lift and equiv lemmas~~ [Merged by Bors] - feat(Topology/Instances/AddCircle): add Ioc analogues of lift and equiv lemmas Apr 10, 2026

mathlib-bors bot closed this Apr 10, 2026

	exact liftIoc_coe_apply ⟨lt_of_le_of_ne b.coe_prop.1 (x_ne_a <\| · ▸ x_eq_b), b.coe_prop.2.le⟩
	exact liftIoc_coe_apply (by grind)

		have x_eq_b : x = ↑b :=
		(QuotientAddGroup.equivIcoMod hp.out a).apply_eq_iff_eq_symm_apply.mp rfl

	have x_eq_b : x = ↑b :=
	(QuotientAddGroup.equivIcoMod hp.out a).apply_eq_iff_eq_symm_apply.mp rfl
	have x_eq_b : x = ↑b := coe_equivIco.symm

	lemma eq_coe_Ioc (a : AddCircle p) : ∃ b ∈ Set.Ioc 0 p, ↑b = a := by
	lemma eq_coe_Ioc (a : AddCircle p) : ∃ b ∈ Ioc 0 p, ↑b = a := by

		theorem liftIoc_eq_liftIco_of_ne (f : 𝕜 → B) {x : AddCircle p}
		(x_ne_a : x ≠ a) : liftIoc p a f x = liftIco p a f x := by

	lemma equivIoc_coe_of_mem {y : 𝕜} (hy : y ∈ Set.Ioc a (a + p)) :
	lemma equivIoc_coe_of_mem {y : 𝕜} (hy : y ∈ Ioc a (a + p)) :

Conversation

pitmonticone commented Apr 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 91f509a196

Import changes for modified files

Declarations diff

Uh oh!

loefflerd commented Apr 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pitmonticone commented Apr 4, 2026

Uh oh!

Uh oh!

loefflerd Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

loefflerd Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

loefflerd Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

loefflerd Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

loefflerd Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

loefflerd Apr 6, 2026

Choose a reason for hiding this comment

Uh oh!

pitmonticone commented Apr 7, 2026

Uh oh!

loefflerd left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Apr 9, 2026

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

faenuccio commented Apr 10, 2026

Uh oh!

mathlib-bors bot commented Apr 10, 2026

Uh oh!

pitmonticone commented Apr 10, 2026

Uh oh!

loefflerd commented Apr 10, 2026

Uh oh!

pitmonticone commented Apr 10, 2026

Uh oh!

pitmonticone commented Apr 10, 2026

Uh oh!

mathlib-bors bot commented Apr 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

pitmonticone commented Apr 2, 2026 •

edited

Loading

github-actions bot commented Apr 2, 2026 •

edited

Loading

loefflerd commented Apr 4, 2026 •

edited

Loading