Almost-refinement of finite partitions

A finite partition P of s almost refines a partition P₀ of s up to δ when every part A of P₀ is covered, except for at most δ * #A of its elements, by parts of P contained in A. Divisibility usually prevents an equipartition with a prescribed number of parts from refining a given partition exactly, but Finpartition.equitabilise always produces one that almost refines it. Almost-refinement is preserved by passing to an exact refinement, so iterated refinement procedures, such as the energy increment in Szemerédi's regularity lemma, keep it.

Main declarations

• Finpartition.AlmostRefines P P₀ δ: P almost refines P₀ up to δ.
• Finpartition.almostRefines_iff: the canonical cover is by all parts of P contained in A.
• Finpartition.almostRefines_of_le: an exact refinement almost refines up to any δ ≥ 0.
• Finpartition.AlmostRefines.mono_left: almost-refinement passes to exact refinements.
• Finpartition.IsEquipartition.exists_equipartition_card_eq_almostRefines: an equipartition with k parts is almost refined, up to δ, by an equipartition with any number n ≥ 2k / δ of parts, provided n is at most the size of the ground set.

def Finpartition.AlmostRefines {α : Type u_1} [DecidableEq α] {s : Finset α} (P P₀ : Finpartition s) (δ : ℝ) : Prop

P almost refines P₀ up to δ: each part A of P₀ contains a family of parts of P whose union misses at most δ * #A elements of A.

theorem Finpartition.almostRefines_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {P P₀ : Finpartition s} {δ : ℝ} : P.AlmostRefines P₀ δ ↔ ∀ A ∈ P₀.parts, ↑(A \ {B ∈ P.parts | B ⊆ A}.biUnion id).card ≤ δ * ↑A.card

Almost-refinement only has to be checked on the largest admissible cover: the parts of P contained in a given part of P₀.

theorem Finpartition.AlmostRefines.mono {α : Type u_1} [DecidableEq α] {s : Finset α} {P P₀ : Finpartition s} {δ δ' : ℝ} (h : P.AlmostRefines P₀ δ) (hδ : δ ≤ δ') : P.AlmostRefines P₀ δ'

Almost-refinement is monotone in the tolerance.

theorem Finpartition.almostRefines_of_le {α : Type u_1} [DecidableEq α] {s : Finset α} {P P₀ : Finpartition s} {δ : ℝ} (h : P ≤ P₀) (hδ : 0 ≤ δ) : P.AlmostRefines P₀ δ

An exact refinement almost refines up to any nonnegative tolerance.

theorem Finpartition.AlmostRefines.mono_left {α : Type u_1} [DecidableEq α] {s : Finset α} {P P₀ Q : Finpartition s} {δ : ℝ} (hQP : Q ≤ P) (h : P.AlmostRefines P₀ δ) : Q.AlmostRefines P₀ δ

An exact refinement of a partition almost refining P₀ almost refines P₀ with the same tolerance.

theorem Finpartition.IsEquipartition.exists_equipartition_card_eq_almostRefines {α : Type u_1} [DecidableEq α] {s : Finset α} {P : Finpartition s} {δ : ℝ} (hP : P.IsEquipartition) {n : ℕ} (hn : n ≠ 0) (hns : n ≤ s.card) (hδ : 2 * ↑P.parts.card ≤ δ * ↑n) : ∃ (Q : Finpartition s), Q.IsEquipartition ∧ Q.parts.card = n ∧ Q.AlmostRefines P δ

If P is an equipartition of s into k parts and 0 < n ≤ #s with 2k ≤ δn, then some equipartition of s into exactly n parts almost refines P up to δ. It is obtained from Finpartition.equitabilise, which leaves at most #s / n elements of each part of P uncovered.