Commit 2023-06-26 09:40 6f0a97ee

View on Github →

feat: port Combinatorics.SimpleGraph.Regularity.Increment (#5476)

Estimated changes

Modified Mathlib.lean

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

modified theorem Finpartition.coe_energy

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

added theorem SzemerediRegularity.card_increment

added theorem SzemerediRegularity.energy_increment

added theorem SzemerediRegularity.increment_isEquipartition

added theorem SzemerediRegularity.offDiag_pairs_le_increment_energy

added theorem SzemerediRegularity.pairContrib_lower_bound

added theorem SzemerediRegularity.uniform_add_nonuniform_eq_offDiag_pairs