Commit 2023-06-26 04:42 9cb18fde

View on Github →

feat: port Combinatorics.SimpleGraph.Regularity.Bound (#4409)

Estimated changes

Modified Mathlib.lean

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

added theorem SzemerediRegularity.a_add_one_le_four_pow_parts_card

added theorem SzemerediRegularity.add_div_le_sum_sq_div_card

added theorem SzemerediRegularity.bound_pos

added theorem SzemerediRegularity.card_aux₁

added theorem SzemerediRegularity.card_aux₂

added theorem SzemerediRegularity.coe_m_add_one_pos

added theorem SzemerediRegularity.eps_pos

added theorem SzemerediRegularity.eps_pow_five_pos

added theorem SzemerediRegularity.hundred_div_ε_pow_five_le_m

added theorem SzemerediRegularity.hundred_le_m

added theorem SzemerediRegularity.hundred_lt_pow_initialBound_mul

added theorem SzemerediRegularity.initialBound_le_bound

added theorem SzemerediRegularity.initialBound_pos

added theorem SzemerediRegularity.le_bound

added theorem SzemerediRegularity.le_initialBound

added theorem SzemerediRegularity.le_stepBound

added theorem SzemerediRegularity.m_pos

added theorem SzemerediRegularity.mul_sq_le_sum_sq

added theorem SzemerediRegularity.one_le_m_coe

added theorem SzemerediRegularity.pow_mul_m_le_card_part

added theorem SzemerediRegularity.seven_le_initialBound

added def SzemerediRegularity.stepBound

added theorem SzemerediRegularity.stepBound_mono

added theorem SzemerediRegularity.stepBound_pos_iff

added def Tactic.evalBound

added def Tactic.evalInitialBound