Commit 2024-05-02 15:03 3e76e0d0

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Dart.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

added theorem SimpleGraph.two_mul_card_edgeFinset

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

added theorem SimpleGraph.FarFromTriangleFree.lt_half

added theorem SimpleGraph.FarFromTriangleFree.lt_one

modified def SimpleGraph.FarFromTriangleFree

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

added def Mathlib.Meta.Positivity.evalTriangleRemovalBound

added theorem SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset

added theorem SimpleGraph.regularityReduced_edges_card_aux

added theorem SimpleGraph.triangleRemovalBound_mul_cube_lt

added theorem SimpleGraph.triangleRemovalBound_nonpos

added theorem SimpleGraph.triangleRemovalBound_pos

added theorem SimpleGraph.triangle_removal

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.filter_and_not

Modified scripts/noshake.json