Commit 2024-04-29 09:44 a9cdcd23

View on Github →

feat: Triangle counting (#8896) Prove the triangle counting lemma. Definitions that are internal to the proof are made private.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Density.lean

added theorem Rel.interedges_eq_biUnion

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

added theorem Finpartition.IsEquipartition.card_biUnion_offDiag_le'

added theorem Finpartition.IsEquipartition.card_biUnion_offDiag_le

added theorem Finpartition.IsEquipartition.card_interedges_sparsePairs_le'

added theorem Finpartition.IsEquipartition.card_interedges_sparsePairs_le

added theorem Finpartition.IsEquipartition.sum_nonUniforms_lt'

added theorem Finpartition.IsEquipartition.sum_nonUniforms_lt

deleted theorem Finpartition.botIsUniform

added theorem Finpartition.bot_isUniform

deleted theorem Finpartition.isUniformOne

added theorem Finpartition.isUniform_one

added theorem Finpartition.mk_mem_nonUniforms

deleted theorem Finpartition.mk_mem_nonUniforms_iff

added theorem Finpartition.mk_mem_sparsePairs

added def Finpartition.nonUniforms

added def Finpartition.sparsePairs

added theorem Finpartition.sparsePairs_mono

added theorem SimpleGraph.IsUniform.pos

modified theorem SimpleGraph.isUniform_one

modified theorem SimpleGraph.isUniform_singleton

added def SimpleGraph.regularityReduced

added theorem SimpleGraph.regularityReduced_anti

added theorem SimpleGraph.regularityReduced_le

added theorem SimpleGraph.regularityReduced_mono

added theorem SimpleGraph.unreduced_edges_subset

Created Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

added theorem SimpleGraph.triangle_counting'

added theorem SimpleGraph.triangle_counting

Modified Mathlib/Order/Partition/Equipartition.lean

deleted theorem Finpartition.Set.Subsingleton.isEquipartition

added theorem Set.Subsingleton.isEquipartition