Weighted finite collections and certificate mass decomposition

Weighted collections and the positive/negative mass decomposition of a dual certificate for the low-frequency construction and recombination pipeline.

Weighted finite collections

structure KaltonRoberts.WeightedCollection (U : Type v) [DecidableEq U] : Type (v + 1)

A weighted finite collection of subsets of U. The weights are nonneg reals with positive total weight, so the collection represents a (possibly unnormalized) distribution over finsets.

This avoids the need for literal multisets (which would require rational certificates and denominator clearing).

• J : Type v

  Finite index type.

• finJ : Fintype self.J

  Fintype instance for J.

• decJ : DecidableEq self.J

  DecidableEq instance for J.

• sets : self.J → Finset U

  The indexed family of sets.

• weight : self.J → ℝ

  Weight of each index.

• weight_nonneg (j : self.J) : 0 ≤ self.weight j

  Weights are nonnegative.

• total_pos : 0 < ∑ j : self.J, self.weight j

  Weights sum to a positive value (total mass).

noncomputable def KaltonRoberts.WeightedCollection.totalWeight {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) : ℝ

Total weight of a weighted collection.

Equations

• C.totalWeight = ∑ j : C.J, C.weight j

theorem KaltonRoberts.WeightedCollection.totalWeight_pos {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) : 0 < C.totalWeight

noncomputable def KaltonRoberts.WeightedCollection.itemFreq {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (i : U) : ℝ

Item frequency: the weighted fraction of sets containing item i.

Equations

• C.itemFreq i = (∑ j : C.J, C.weight j * if i ∈ C.sets j then 1 else 0) / C.totalWeight

noncomputable def KaltonRoberts.WeightedCollection.avgDeficit {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (f : Finset U → ℝ) (M : ℝ) : ℝ

Weighted average deficit.

Equations

• C.avgDeficit f M = (∑ j : C.J, C.weight j * KaltonRoberts.deficit f M (C.sets j)) / C.totalWeight

noncomputable def KaltonRoberts.WeightedCollection.avgSurplus {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (f : Finset U → ℝ) (M : ℝ) : ℝ

Weighted average surplus.

Equations

• C.avgSurplus f M = (∑ j : C.J, C.weight j * KaltonRoberts.surplus f M (C.sets j)) / C.totalWeight

theorem KaltonRoberts.WeightedCollection.itemFreq_nonneg {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (i : U) : 0 ≤ C.itemFreq i

Item frequency is nonneg.

theorem KaltonRoberts.WeightedCollection.itemFreq_le_one {U : Type u_1} [DecidableEq U] (C : WeightedCollection U) (i : U) : C.itemFreq i ≤ 1

Item frequency is at most 1.

Certificate mass decomposition

noncomputable def KaltonRoberts.DualCertificate.posMass {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : ℝ

Positive mass of a dual certificate: p = ∑_S max(λ(S), 0).

Equations

• cert.posMass = ∑ S : Finset U, max (cert.lam S) 0

noncomputable def KaltonRoberts.DualCertificate.negMass {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : ℝ

Negative mass of a dual certificate: q = ∑_S max(−λ(S), 0).

Equations

• cert.negMass = ∑ S : Finset U, max (-cert.lam S) 0

theorem KaltonRoberts.DualCertificate.posMass_nonneg {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : 0 ≤ cert.posMass

Positive mass is nonneg.

theorem KaltonRoberts.DualCertificate.negMass_nonneg {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : 0 ≤ cert.negMass

Negative mass is nonneg.

theorem KaltonRoberts.DualCertificate.posMass_add_negMass {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.posMass + cert.negMass = 1

theorem KaltonRoberts.DualCertificate.posMass_le_one {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.posMass ≤ 1

p ≤ 1

theorem KaltonRoberts.DualCertificate.negMass_le_one {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.negMass ≤ 1

q ≤ 1

theorem KaltonRoberts.DualCertificate.posMass_pos {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (h : ∃ (S : Finset U), 0 < cert.lam S) : 0 < cert.posMass

Positive mass is positive when there is a positively-weighted set.

theorem KaltonRoberts.DualCertificate.negMass_pos {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (h : ∃ (S : Finset U), cert.lam S < 0) : 0 < cert.negMass

Negative mass is positive when there is a negatively-weighted set.

Zero-marginal frequency identity

theorem KaltonRoberts.DualCertificate.marginal_pos_eq_neg {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (i : U) : ∑ S : Finset U with i ∈ S, max (cert.lam S) 0 = ∑ S : Finset U with i ∈ S, max (-cert.lam S) 0

theorem KaltonRoberts.DualCertificate.pos_item_sum_le_negMass {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (i : U) : ∑ S : Finset U with i ∈ S, max (cert.lam S) 0 ≤ cert.negMass

Item frequency bound: for each item i, the sum of positive weights over sets containing i is at most the negative mass q.

theorem KaltonRoberts.DualCertificate.neg_item_sum_le_posMass {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (i : U) : ∑ S : Finset U with i ∈ S, max (-cert.lam S) 0 ≤ cert.posMass

Symmetric bound: for each item i, the sum of negative weights over sets containing i is at most the positive mass p.

Positive and negative weighted collections from a certificate

noncomputable def KaltonRoberts.DualCertificate.posCollection {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hp : 0 < cert.posMass) : WeightedCollection U

The positive weighted collection from a dual certificate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KaltonRoberts.DualCertificate.negCollection {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hq : 0 < cert.negMass) : WeightedCollection U

The negative weighted collection from a dual certificate.

Equations

• One or more equations did not get rendered due to their size.

theorem KaltonRoberts.DualCertificate.posCollection_totalWeight {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hp : 0 < cert.posMass) : (cert.posCollection hp).totalWeight = cert.posMass

The total weight of the positive collection is p.

theorem KaltonRoberts.DualCertificate.negCollection_totalWeight {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hq : 0 < cert.negMass) : (cert.negCollection hq).totalWeight = cert.negMass

The total weight of the negative collection is q.

Frequency and deficit bounds for certificate collections

theorem KaltonRoberts.DualCertificate.posCollection_itemFreq_le {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hp : 0 < cert.posMass) (i : U) : (cert.posCollection hp).itemFreq i ≤ cert.negMass / cert.posMass

theorem KaltonRoberts.DualCertificate.posCollection_avgDeficit_eq_zero {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hp : 0 < cert.posMass) : (cert.posCollection hp).avgDeficit f M = 0

theorem KaltonRoberts.DualCertificate.negCollection_avgSurplus_eq_zero {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hq : 0 < cert.negMass) : (cert.negCollection hq).avgSurplus f M = 0

theorem KaltonRoberts.DualCertificate.negCollection_itemFreq_le {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hq : 0 < cert.negMass) (i : U) : (cert.negCollection hq).itemFreq i ≤ cert.posMass / cert.negMass

Swapping lemma: ensure q ≤ 1/2

theorem KaltonRoberts.DualCertificate.can_swap_to_small_q {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.negMass ≤ 1 / 2 ∨ cert.posMass ≤ 1 / 2

By possibly replacing f by −f, we may arrange q ≤ 1/2 ≤ p.

Augmented collections (Lemma 2.3 of the paper)

The augmented positive collection A consists of:

• Positive active sets P (with weight λ⁺(P))
• Complements Nᶜ of negative active sets N (with weight λ⁻(N))

Total weight = p + q = 1. Every item has frequency exactly q (by the zero-marginal property). Average deficit ≤ q(1 − u).

Symmetrically for the augmented negative collection B.

noncomputable def KaltonRoberts.DualCertificate.augPosCollection {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : WeightedCollection U

The augmented positive collection from a dual certificate (Lemma 2.3). Includes positive active sets and complements of negative active sets.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def KaltonRoberts.DualCertificate.augNegCollection {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : WeightedCollection U

The augmented negative collection from a dual certificate (Lemma 2.3). Includes negative active sets and complements of positive active sets.

Equations

• One or more equations did not get rendered due to their size.

theorem KaltonRoberts.DualCertificate.augPosCollection_totalWeight {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.augPosCollection.totalWeight = 1

Total weight of the augmented positive collection is 1.

theorem KaltonRoberts.DualCertificate.augNegCollection_totalWeight {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) : cert.augNegCollection.totalWeight = 1

Total weight of the augmented negative collection is 1.

theorem KaltonRoberts.DualCertificate.augPosCollection_itemFreq {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (i : U) : cert.augPosCollection.itemFreq i = cert.negMass

theorem KaltonRoberts.DualCertificate.augNegCollection_itemFreq {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (i : U) : cert.augNegCollection.itemFreq i = cert.posMass

theorem KaltonRoberts.DualCertificate.augPosCollection_avgDeficit_le {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hf : IsApproxAdditive f 1) (_hM : ∀ (S : Finset U), |f S| ≤ M) : cert.augPosCollection.avgDeficit f M ≤ cert.negMass * (1 - f Finset.univ)

theorem KaltonRoberts.DualCertificate.augNegCollection_avgSurplus_le {U : Type u_1} [DecidableEq U] [Fintype U] {f : Finset U → ℝ} {M : ℝ} (cert : DualCertificate f M) (hf : IsApproxAdditive f 1) (_hM : ∀ (S : Finset U), |f S| ≤ M) : cert.augNegCollection.avgSurplus f M ≤ cert.posMass * (1 + f Finset.univ)

Uniform weighted collection from a finite family

noncomputable def KaltonRoberts.WeightedCollection.uniformOfFamily {U' : Type u} [DecidableEq U'] {J : Type u} [Fintype J] [DecidableEq J] (sets : J → Finset U') (hJ : 0 < Fintype.card J) : WeightedCollection U'

Build a WeightedCollection with uniform weight 1 from a finite family of subsets indexed by a type J with positive cardinality.

Equations

• KaltonRoberts.WeightedCollection.uniformOfFamily sets hJ = { J := J, finJ := inst✝¹, decJ := inst✝, sets := sets, weight := fun (x : J) => 1, weight_nonneg := ⋯, total_pos := ⋯ }

theorem KaltonRoberts.WeightedCollection.uniformOfFamily_totalWeight {U' : Type u} [DecidableEq U'] {J : Type u} [Fintype J] [DecidableEq J] (sets : J → Finset U') (hJ : 0 < Fintype.card J) : (uniformOfFamily sets hJ).totalWeight = ↑(Fintype.card J)

Total weight of a uniform collection equals the cardinality.

theorem KaltonRoberts.WeightedCollection.uniformOfFamily_itemFreq {U' : Type u} [DecidableEq U'] {J : Type u} [Fintype J] [DecidableEq J] (sets : J → Finset U') (hJ : 0 < Fintype.card J) (i : U') : (uniformOfFamily sets hJ).itemFreq i = ↑{j : J | i ∈ sets j}.card / ↑(Fintype.card J)

Item frequency in a uniform collection equals card {j | i ∈ sets j} / card J.

theorem KaltonRoberts.WeightedCollection.uniformOfFamily_avgDeficit {U' : Type u} [DecidableEq U'] {J : Type u} [Fintype J] [DecidableEq J] (sets : J → Finset U') (hJ : 0 < Fintype.card J) (f : Finset U' → ℝ) (M : ℝ) : (uniformOfFamily sets hJ).avgDeficit f M = (∑ j : J, deficit f M (sets j)) / ↑(Fintype.card J)

Average deficit of a uniform collection equals (∑ j, deficit f M (sets j)) / card J.

theorem KaltonRoberts.WeightedCollection.uniformOfFamily_avgSurplus {U' : Type u} [DecidableEq U'] {J : Type u} [Fintype J] [DecidableEq J] (sets : J → Finset U') (hJ : 0 < Fintype.card J) (f : Finset U' → ℝ) (M : ℝ) : (uniformOfFamily sets hJ).avgSurplus f M = (∑ j : J, surplus f M (sets j)) / ↑(Fintype.card J)

Average surplus of a uniform collection equals (∑ j, surplus f M (sets j)) / card J.