[Merged by Bors] - feat(Combinatorics/SimpleGraph): part of Tutte's theorem by pimotte · Pull Request #22119 · leanprover-community/mathlib4

pimotte · 2025-02-20T11:02:16Z

Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's:

necessity of the Tutte condition (not_isTutteViolator)
the fact that the empty set violates the Tutte condition if the number of vertices is odd (IsTutteViolator.empty)
the construction of a perfect matching in a graph that decomposes into cliques (Subgraph.IsPerfectMatching.exists_of_isClique_supp)

Definitions added: IsTutteViolator.

depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph): define odd components #22125

Zulip thread on Tutte's

github-actions · 2025-02-20T11:03:22Z

PR summary 8628440bf1

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Matching	936	949	+13 (+1.39%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents	749	759	+10 (+1.34%)
Mathlib.Combinatorics.SimpleGraph.UniversalVerts	941	951	+10 (+1.06%)

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents` `Mathlib.Combinatorics.SimpleGraph.UniversalVerts`	10
`Mathlib.Combinatorics.SimpleGraph.Matching`	13
`Mathlib.Combinatorics.SimpleGraph.Tutte` (new file)	952

Declarations diff

+ ConnectedComponent.even_ncard_supp_sdiff_rep
+ IsClique.even_iff_exists_isMatching
+ IsMatching.eq_of_adj_left
+ IsMatching.eq_of_adj_right
+ IsTutteViolator
+ IsTutteViolator.empty
+ Subgraph.IsPerfectMatching.exists_of_isClique_supp
+ disjoint_image_val_universalVerts
+ even_ncard_compl_iff
+ even_ncard_image_val_supp_sdiff_image_val_rep_union
+ ncard_eq
+ not_isTutteViolator_of_isPerfectMatching
+ odd_ncard_compl_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 script/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).

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib4-dependent-issues-bot · 2025-03-20T17:21:54Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Combinatorics/SimpleGraph): define odd components #22125~~
By Dependent Issues (🤖). Happy coding!

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies

Just pushed a small golf and suggested another one. Rest looks good to me, thanks!

maintainer delegate

github-actions · 2025-04-02T11:15:48Z

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

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

b-mehta

This is broadly in good shape, I've left a couple of comments for now. I'll take another look after you've addressed them!

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

…b4 into PO_tutte_pt1

b-mehta · 2025-04-30T10:52:37Z

Looks good, thank you!

bors merge

Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's: - necessity of the Tutte condition (`not_isTutteViolator`) - the fact that the empty set violates the Tutte condition if the number of vertices is odd (`IsTutteViolator.empty`) - the construction of a perfect matching in a graph that decomposes into cliques (`Subgraph.IsPerfectMatching.exists_of_isClique_supp`) Definitions added: `IsTutteViolator`. Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2025-04-30T12:12:00Z

Build failed (retrying...):

Build

Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's: - necessity of the Tutte condition (`not_isTutteViolator`) - the fact that the empty set violates the Tutte condition if the number of vertices is odd (`IsTutteViolator.empty`) - the construction of a perfect matching in a graph that decomposes into cliques (`Subgraph.IsPerfectMatching.exists_of_isClique_supp`) Definitions added: `IsTutteViolator`. Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2025-04-30T12:59:31Z

Pull request successfully merged into master.

Build succeeded:

Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's: - necessity of the Tutte condition (`not_isTutteViolator`) - the fact that the empty set violates the Tutte condition if the number of vertices is odd (`IsTutteViolator.empty`) - the construction of a perfect matching in a graph that decomposes into cliques (`Subgraph.IsPerfectMatching.exists_of_isClique_supp`) Definitions added: `IsTutteViolator`. Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

pimotte added 10 commits February 19, 2025 16:53

Work in progress

8622346

Prepping PR

e6d8b3e

Refactoring

4adc803

Merge remote-tracking branch 'origin/master' into PO_tutte_pt1

d80f82a

Move off inlined lemma

6552a11

Refactoring

7aeb75d

Polishing

d020260

Fixes

730107a

Import order

0097b68

Namespacing

fe630fb

pimotte added the t-combinatorics Combinatorics label Feb 20, 2025

pimotte requested a review from YaelDillies February 20, 2025 11:02

Documentation

7416cbf

pimotte changed the title ~~feat(SimpleGraph): part of Tutte's theorem~~ feat(Combinatorics/SimpleGraph): part of Tutte's theorem Feb 20, 2025

YaelDillies reviewed Feb 20, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 20, 2025

pimotte and others added 2 commits February 20, 2025 14:49

Apply suggestions from code review

47b698b

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Post-review patches

fe83cf9

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 20, 2025

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 20, 2025

pimotte mentioned this pull request Mar 14, 2025

[Merged by Bors] - feat(Combinatorics/SimpleGraph): Tutte's theorem #22915

Closed

2 tasks

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 20, 2025

YaelDillies reviewed Mar 20, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2025

pimotte and others added 3 commits March 22, 2025 11:23

Apply suggestions from code review

83c6162

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Merge remote-tracking branch 'origin/master' into PO_tutte_pt1

44b9735

Patches

58676c7

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 22, 2025

pimotte and others added 4 commits March 31, 2025 14:16

Apply suggestions from code review

dc17aaa

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Combinatorics/SimpleGraph/Tutte.lean

18fc7d2

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Ugly thing

782fbc9

Unsqueezed simp and other small tweaks

4c5ce7e

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2025

golf

a5b612e

YaelDillies approved these changes Apr 2, 2025

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean Outdated

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 2, 2025

pimotte and others added 2 commits April 3, 2025 13:34

Update Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

68f755b

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Lint fix

0e73fb1

b-mehta reviewed Apr 17, 2025

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Tutte.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Tutte.lean Outdated

Comment thread Mathlib/Combinatorics/SimpleGraph/Tutte.lean Outdated

Comment thread Mathlib/Data/Set/Card.lean Outdated

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 17, 2025

pimotte and others added 2 commits April 18, 2025 09:07

Update Mathlib/Combinatorics/SimpleGraph/Tutte.lean

d992a7b

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Combinatorics/SimpleGraph/Tutte.lean

b30b3a4

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 18, 2025

YaelDillies and others added 3 commits April 18, 2025 21:49

golf using choose

9e03067

Fix types

dea4153

Merge branch 'PO_tutte_pt1' of github.com:leanprover-community/mathli…

8628440

…b4 into PO_tutte_pt1

YaelDillies removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 30, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Apr 30, 2025

mathlib-bors bot changed the title ~~feat(Combinatorics/SimpleGraph): part of Tutte's theorem~~ [Merged by Bors] - feat(Combinatorics/SimpleGraph): part of Tutte's theorem Apr 30, 2025

mathlib-bors bot closed this Apr 30, 2025

mathlib-bors bot deleted the PO_tutte_pt1 branch April 30, 2025 12:59

Conversation

pimotte commented Feb 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8628440bf1

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Mar 20, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Apr 2, 2025

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

b-mehta commented Apr 30, 2025

Uh oh!

mathlib-bors bot commented Apr 30, 2025

Uh oh!

mathlib-bors bot commented Apr 30, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

pimotte commented Feb 20, 2025 •

edited

Loading

github-actions bot commented Feb 20, 2025 •

edited

Loading