Commit 2023-05-19 16:48 f51de876

View on Github →

feat(combinatorics/simple_graph/regularity/chunk): Partition of a part (#18371) The heart of the calculation of Szemerédi Regularity Lemma. Define the partition of a part of the original partition and show it locally increases the energy. This is all internal to the proof of SRL, so I made most lemmas private

Estimated changes

Created src/combinatorics/simple_graph/regularity/chunk.lean

added theorem szemeredi_regularity.bUnion_star_subset_nonuniform_witness

added theorem szemeredi_regularity.card_bUnion_star_le_m_add_one_card_star_mul

added theorem szemeredi_regularity.card_chunk

added theorem szemeredi_regularity.card_eq_of_mem_parts_chunk

added theorem szemeredi_regularity.card_le_m_add_one_of_mem_chunk_parts

added theorem szemeredi_regularity.edge_density_chunk_not_uniform

added theorem szemeredi_regularity.edge_density_chunk_uniform

added theorem szemeredi_regularity.m_le_card_of_mem_chunk_parts

added theorem szemeredi_regularity.star_subset_chunk

Modified src/combinatorics/simple_graph/regularity/uniform.lean

added theorem simple_graph.le_card_nonuniform_witness

deleted theorem simple_graph.nonuniform_witness_card_le