Commit 2023-12-26 20:26 fae20230

View on Github →

chore: Make Szeméredi regularity calculation more readable (#9284) by using calc, gcongr and positivity. This should be much more maintainable now. Nicely enough, this reduces the total number of lines.

Estimated changes

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

added theorem SzemerediRegularity.coe_stepBound

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

modified theorem SzemerediRegularity.energy_increment

added theorem SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq

deleted theorem SzemerediRegularity.offDiag_pairs_le_increment_energy

deleted theorem SzemerediRegularity.pairContrib_lower_bound

deleted theorem SzemerediRegularity.uniform_add_nonuniform_eq_offDiag_pairs

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