Skip to content

feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem#28685

Open
mitchell-horner wants to merge 63 commits intoleanprover-community:masterfrom
mitchell-horner:erdos-stone-1
Open

feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem#28685
mitchell-horner wants to merge 63 commits intoleanprover-community:masterfrom
mitchell-horner:erdos-stone-1

Conversation

@mitchell-horner
Copy link
Copy Markdown
Collaborator

@mitchell-horner mitchell-horner commented Aug 20, 2025 •
edited
Loading

Proves the minimal degree-version of the Erdős-Stone theorem:

If G has a minimal degree of at least (1 - 1 / r + o(1)) * card V, then G contains a copy of a completeEquipartiteGraph in r + 1 parts each of size t.

The double-counting construction from the proof is available in namespace ErdosStone.

This is the first of several pull requests towards the full Erdős-Stone(-Simonovits) theorem, hence the name of the file.

Open in Gitpod

@mitchell-horner
Add Bipartite section
4d5d9a7
@mitchell-horner
Impl between_le
907f2d1
@mitchell-horner
Merge branch 'master' into mitchell-horner/between
87b84ac
@mitchell-horner
Merge branch 'master' into mitchell-horner/between
9dcdcc7
@mitchell-horner
Impl between_isBipartite
8045aa6
@mitchell-horner
Merge branch 'master' into mitchell-horner/between
68a1882
@mitchell-horner
Merge branch 'master' into mitchell-horner/between
b857f8e
@mitchell-horner
Impl DecidablePred
78753cc
@mitchell-horner
Impl completeEquipartiteGraph
79b84cb
@mitchell-horner
Remove Fintype assumption
d134f91
@mitchell-horner
Remove simp tag
8714dba
@mitchell-horner
Impl completeEquipartiteSubgraph
2cbca72
@mitchell-horner
Update docstrings
09f6580
@mitchell-horner
Impl DecidablePred
5747774
@mitchell-horner
Impl completeEquipartiteGraph
35466cb
@mitchell-horner
Remove Fintype assumption
486a7fd
@mitchell-horner
Remove simp tag
03be3a6
@mitchell-horner
Fix formatting
aadb934
@mitchell-horner
Fix completeEquipartiteGraph.completeMultipartiteGraph
9bc64b5
@mitchell-horner
Refactor isContained_completeEquipartiteGraph_of_colorable
0fd73f1
@mitchell-horner
Impl completeEquipartiteGraph.turanGraph
62da8f6
@mitchell-horner
Update docstrings
a016728
@mitchell-horner
Fix formatting
59ed36a
@mitchell-horner
Move section Coloring
34c80ba
@mitchell-horner
Merge branch 'master' into complete-equipartite
421951a
@mitchell-horner
Impl filter_disjiUnion
95fd722
@mitchell-horner
Impl one_sub_one_div_cast_* theorems
afca995
@mitchell-horner
Move card_edgeFinset_eq
6541651
@mitchell-horner
Impl Colorable.map
7ddc8e0
@mitchell-horner
Impl chromaticNumber_eq_iff_colorable_not_colorable
44eee46
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 20, 2025
@mitchell-horner mitchell-horner added the WIP Work in progress label Aug 20, 2025
@mitchell-horner mitchell-horner mentioned this pull request Aug 20, 2025
Open
1 task
@mathlib4-dependent-issues-bot 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 Aug 20, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 20, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 20, 2025 •
edited
Loading

PR summary 02398f3984

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits (new file) 1380

Declarations diff

+ between_verts_isBipartiteWith
+ card_edgeFinset_between_verts_le
+ degree_between_verts_lt_of_mem_sdiff
+ eventually_completeEquipartiteGraph_isContained_of_minDegree
+ filter
+ filter.pi
+ filter.pi.exists_le_card_fiber
+ filter.pi.mem_val
+ filter_subset_compl_verts
+ le_card_edgeFinset_between_verts
+ mul_le_card_filter_mul

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

@mitchell-horner mitchell-horner added the t-combinatorics Combinatorics label Aug 25, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 28, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Aug 28, 2025

This pull request has conflicts, please merge master and resolve them.

@mitchell-horner mitchell-horner mentioned this pull request Sep 3, 2025
Closed
2 tasks
@mathlib-dependent-issues mathlib-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 1, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 1, 2026

This PR/issue depends on:

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 2, 2026
@mitchell-horner mitchell-horner removed the WIP Work in progress label Mar 2, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@YaelDillies YaelDillies

Labels

t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mitchell-horner @mathlib4-merge-conflict-bot @YaelDillies @mathlib4-dependent-issues-bot