Commit 2025-09-17 01:02 38084fae

View on Github →

refactor(SimpleGraph): make triangleRemovalBound positive more often (#29540) It wasn't positive when ε > 4, but that is a junk value anyway, so we change the junk value to a positive one. See #29496 for more context.

Estimated changes

Modified Mathlib/Combinatorics/Additive/Corner/Roth.lean

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

added theorem SimpleGraph.DeleteFar.le_card_edgeFinset

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

modified theorem SimpleGraph.FarFromTriangleFree.lt_half

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

added def Mathlib.Meta.Positivity.evalTriangleRemovalBound

added theorem SimpleGraph.triangleRemovalBound_le

modified theorem SimpleGraph.triangleRemovalBound_pos

Modified Mathlib/Data/Nat/Choose/Bounds.lean

added theorem Nat.choose_lt_descFactorial

added theorem Nat.choose_lt_pow

added theorem Nat.choose_lt_pow_div

Modified Mathlib/Data/Nat/Factorial/Basic.lean

modified theorem Nat.descFactorial_lt_pow

added theorem Nat.descFactorial_pos