Commit 2022-03-31 02:41 8a213165

View on Github →

feat(combinatorics/simple_graph/regularity/bound): Numerical bounds for Szemerédi's regularity lemma (#12962) Define the constants appearing in Szemerédi's regularity lemma and prove a bunch of numerical facts about them.

Estimated changes

Modified src/algebra/order/field.lean

added theorem le_div_self

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

added theorem szemeredi_regularity.a_add_one_le_four_pow_parts_card

added theorem szemeredi_regularity.bound_pos

added theorem szemeredi_regularity.card_aux₁

added theorem szemeredi_regularity.card_aux₂

added theorem szemeredi_regularity.coe_m_add_one_pos

added theorem szemeredi_regularity.eps_pos

added theorem szemeredi_regularity.eps_pow_five_pos

added theorem szemeredi_regularity.four_pow_pos

added theorem szemeredi_regularity.hundred_div_ε_pow_five_le_m

added theorem szemeredi_regularity.hundred_le_m

added theorem szemeredi_regularity.hundred_lt_pow_initial_bound_mul

added theorem szemeredi_regularity.initial_bound_le_bound

added theorem szemeredi_regularity.initial_bound_pos

added theorem szemeredi_regularity.le_bound

added theorem szemeredi_regularity.le_initial_bound

added theorem szemeredi_regularity.le_step_bound

added theorem szemeredi_regularity.m_coe_pos

added theorem szemeredi_regularity.m_pos

added theorem szemeredi_regularity.one_le_m_coe

added theorem szemeredi_regularity.pow_mul_m_le_card_part

added theorem szemeredi_regularity.seven_le_initial_bound

added def szemeredi_regularity.step_bound

added theorem szemeredi_regularity.step_bound_mono

added theorem szemeredi_regularity.step_bound_pos_iff

Modified src/order/partition/equipartition.lean

added theorem finpartition.is_equipartition.card_parts_eq_average