SzemerediRegularity.a_add_one_le_four_pow_parts_card
theorem SzemerediRegularity.a_add_one_le_four_pow_parts_card :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ},
Fintype.card α / P.parts.card - Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card +
1 ≤
4 ^ P.parts.card
The theorem `SzemerediRegularity.a_add_one_le_four_pow_parts_card` states that for any type `α` with decidable equality and finite number of elements, and for any given finite partition `P` of the universal set of `α`, the integer division of the card of `α` by the card of `P.parts` minus the quantity of the product of the integer division of the card of `α` by the `stepBound` of P.parts.card and 4 to the power of card of P.parts, increased by 1, is less than or equal to 4 to the power of the card of P.parts. This theorem is an auxiliary result used in the context of Szemeredi's Regularity Lemma.
More concisely: For any finite type `α` with decidable equality and given finite partition `P` of `α`, the quotient of `α`'s cardinality by the number of parts in `P` minus the product of their cardinalities raised to the power of 4 and divided by the step bound of `P.parts.card`, plus one, is bounded by 4 raised to the power of the number of parts in `P`.
|
SzemerediRegularity.stepBound_pos
theorem SzemerediRegularity.stepBound_pos : ∀ {n : ℕ}, 0 < n → 0 < SzemerediRegularity.stepBound n
The theorem `SzemerediRegularity.stepBound_pos` states that for any natural number `n` greater than zero, the function `SzemerediRegularity.stepBound` also returns a value greater than zero. In the context of Szemerédi's regularity lemma, this means that blowing up a partition of size `n` during the induction results in a partition of size at most `stepBound n`, which is also a positive number.
More concisely: For any natural number `n` greater than zero, `SzemerediRegularity.stepBound n` is a positive number.
|