A finite weighted incidence bound

If all but a bounded number of sets containing a finite configuration have uniformly positive mass outside its closure, and adjoining such an outside point increases a bounded rank, the number of sets containing a point is uniformly bounded. This is the counting induction used for large faces.

noncomputable def EGZ.WeightedIncidence.mass {α : Type u_1} [Fintype α] (w : α → ℝ) (S : Set α) : ℝ

Mass of a set for a finite real-valued weight.

Equations

• EGZ.WeightedIncidence.mass w S = ∑ a : α, if a ∈ S then w a else 0

@[simp]

theorem EGZ.WeightedIncidence.mass_natCast {α : Type u_1} [Fintype α] (w : α → ℕ) (S : Set α) : mass (fun (a : α) => ↑(w a)) S = ↑(natMassOn w S)

theorem EGZ.WeightedIncidence.mass_nonneg {α : Type u_1} [Fintype α] (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (S : Set α) : 0 ≤ mass w S

theorem EGZ.WeightedIncidence.mass_mono {α : Type u_1} [Fintype α] (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) {S T : Set α} (hST : S ⊆ T) : mass w S ≤ mass w T

theorem EGZ.WeightedIncidence.mass_le_total {α : Type u_1} [Fintype α] (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (S : Set α) : mass w S ≤ ∑ a : α, w a

theorem EGZ.WeightedIncidence.mass_diff_add_inter {α : Type u_1} [Fintype α] (w : α → ℝ) (S T : Set α) : mass w (S \ T) + mass w (S ∩ T) = mass w S

theorem EGZ.WeightedIncidence.mass_restrict_eq_of_subset {α : Type u_1} [Fintype α] (w : α → ℝ) (S T : Set α) (hTS : T ⊆ S) : mass (fun (a : α) => if a ∈ S then w a else 0) T = mass w T

Restricting the common weight does not alter masses inside the retained set.

noncomputable def EGZ.WeightedIncidence.containing {α : Type u_1} {I : Type u_2} [Fintype α] [Fintype I] (F : I → Set α) (S : Finset α) : Finset I

The members of a family that contain every point of a finite set.

Equations

• EGZ.WeightedIncidence.containing F S = {i : I | ∀ a ∈ S, a ∈ F i}

@[simp]

theorem EGZ.WeightedIncidence.mem_containing {α : Type u_1} {I : Type u_2} [Fintype α] [Fintype I] (F : I → Set α) (S : Finset α) (i : I) : i ∈ containing F S ↔ ∀ a ∈ S, a ∈ F i

noncomputable def EGZ.WeightedIncidence.bound (c b : ℝ) : ℕ → ℝ

The recurrence has one bounded exceptional contribution at each rank.

Equations

• EGZ.WeightedIncidence.bound c b 0 = c
• EGZ.WeightedIncidence.bound c b r.succ = c + EGZ.WeightedIncidence.bound c b r / b

theorem EGZ.WeightedIncidence.bound_nonneg {c b : ℝ} (hc : 0 ≤ c) (hb : 0 ≤ b) (r : ℕ) : 0 ≤ bound c b r

theorem EGZ.WeightedIncidence.bound_le_pow {c b : ℝ} (hc : 0 ≤ c) (hb : 0 < b) (r : ℕ) : bound c b r ≤ (c + 1 + b⁻¹) ^ (r + 1)

A convenient closed-form majorant for the recursive bound.

theorem EGZ.WeightedIncidence.sum_mass_eq {α : Type u_1} {I : Type u_2} [Fintype α] (w : α → ℝ) (F : I → Set α) (G : Finset I) (U : Set α) : ∑ i ∈ G, mass w (F i ∩ U) = ∑ a : α, if a ∈ U then ↑{i ∈ G | a ∈ F i}.card * w a else 0

Exchange the two finite sums and count incidences at each atom.

theorem EGZ.WeightedIncidence.card_containing_le {α : Type u_1} {I : Type u_2} [Fintype α] [Fintype I] (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (hM : 0 < ∑ a : α, w a) (F : I → Set α) (rank : Finset α → ℕ) (closure : Finset α → Set α) (exceptional : Finset α → Finset I) (c d : ℕ) (b : ℝ) (hb : 0 < b) (hrank : ∀ (S : Finset α), rank S ≤ d) (hinsert : ∀ (S : Finset α), S.Nonempty → ∀ a ∉ closure S, rank S < rank (insert a S)) (hexceptional : ∀ (S : Finset α), S.Nonempty → (exceptional S).card ≤ c) (hescape : ∀ (S : Finset α), S.Nonempty → ∀ i ∈ containing F S, i ∉ exceptional S → b * ∑ a : α, w a ≤ mass w (F i \ closure S)) (r : ℕ) (S : Finset α) : S.Nonempty → d ≤ rank S + r → ↑(containing F S).card ≤ bound (↑c) b r

Abstract closure-and-rank induction. Exceptional sets need not be members of the containing family; only their cardinality is used.

theorem EGZ.WeightedIncidence.card_family_le {α : Type u_1} {I : Type u_2} [Fintype α] [Fintype I] (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (hM : 0 < ∑ a : α, w a) (F : I → Set α) (rank : Finset α → ℕ) (closure : Finset α → Set α) (exceptional : Finset α → Finset I) (c d : ℕ) (b e : ℝ) (hb : 0 < b) (he : 0 < e) (hrank : ∀ (S : Finset α), rank S ≤ d) (hinsert : ∀ (S : Finset α), S.Nonempty → ∀ a ∉ closure S, rank S < rank (insert a S)) (hexceptional : ∀ (S : Finset α), S.Nonempty → (exceptional S).card ≤ c) (hescape : ∀ (S : Finset α), S.Nonempty → ∀ i ∈ containing F S, i ∉ exceptional S → b * ∑ a : α, w a ≤ mass w (F i \ closure S)) (hlarge : ∀ (i : I), e * ∑ a : α, w a ≤ mass w (F i)) : ↑(Fintype.card I) ≤ bound (↑c) b d / e

If each member also has positive relative mass, the entire family has a uniform cardinality bound.