Product and mixed intersection collections

Product and mixed intersection collections with the frequency and deficit bounds needed for the mixed-intersection step.

Helper: sum of products = (sum)^ℓ

Two-set deficit intersection inequality

theorem KaltonRoberts.deficit_inter_le {U : Type u_1} [DecidableEq U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (A B : Finset U) : deficit f M (A ∩ B) ≤ deficit f M A + deficit f M B + 2

Deficit of an intersection is at most the sum of deficits plus 2.

Finite intersection deficit bound

noncomputable def KaltonRoberts.finsetInter {U : Type u_1} [DecidableEq U] [Fintype U] {ℓ : ℕ} (A : Fin ℓ → Finset U) : Finset U

The intersection of a family indexed by Fin ℓ.

Equations

• KaltonRoberts.finsetInter A = Finset.univ.inf A

theorem KaltonRoberts.deficit_finsetInter_le {U : Type u_1} [DecidableEq U] [Fintype U] (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) (A : Fin ℓ → Finset U) : deficit f M (finsetInter A) ≤ ∑ k : Fin ℓ, deficit f M (A k) + 2 * (↑ℓ - 1)

Deficit of ℓ-fold intersection is at most sum of deficits + 2*(ℓ-1).

Product intersection collection

noncomputable def KaltonRoberts.WeightedCollection.productInter {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) : WeightedCollection U

The ℓ-fold product intersection collection.

Equations

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

theorem KaltonRoberts.WeightedCollection.productInter_totalWeight {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) : (C.productInter ℓ).totalWeight = C.totalWeight ^ ℓ

Total weight of the product collection equals C.totalWeight^ℓ.

theorem KaltonRoberts.WeightedCollection.productInter_itemFreq {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) (i : U) : (C.productInter ℓ).itemFreq i ≤ C.itemFreq i ^ ℓ

Item frequency of the product collection is at most (itemFreq C i)^ℓ.

theorem KaltonRoberts.WeightedCollection.productInter_avgDeficit {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (D : ℝ) (_hD : 0 ≤ D) (hdeficit : C.avgDeficit f M ≤ D) : (C.productInter ℓ).avgDeficit f M ≤ ↑ℓ * D + 2 * (↑ℓ - 1)

Average deficit of the product collection.

Mixed intersection collection

The key insight for the mixed collection: to make the convex combination work with unnormalized collections, we multiply the ℓ-branch by TW^(ℓ+1) and the (ℓ+1)-branch by TW^ℓ, equalizing the denominators. The total weight becomes TW^(2ℓ+1).

noncomputable def KaltonRoberts.WeightedCollection.mixedInter {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) (τ : ℝ) (hτ : 0 ≤ τ) (hτ1 : τ ≤ 1) : WeightedCollection U

The mixed intersection collection: weighted mixture of ℓ-fold and (ℓ+1)-fold product intersections, with balanced weights so that frequency bounds work correctly for unnormalized collections.

Equations

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

theorem KaltonRoberts.WeightedCollection.mixedInter_totalWeight {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) (τ : ℝ) (hτ : 0 ≤ τ) (hτ1 : τ ≤ 1) : (C.mixedInter ℓ τ hτ hτ1).totalWeight = C.totalWeight ^ (2 * ℓ + 1)

Total weight of the mixed collection.

theorem KaltonRoberts.WeightedCollection.mixedInter_itemFreq_le {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) (τ : ℝ) (hτ : 0 ≤ τ) (hτ1 : τ ≤ 1) (t : ℝ) (_ht : 0 ≤ t) (_ht1 : t ≤ 1) (hfreq : ∀ (i : U), C.itemFreq i ≤ t) (i : U) : (C.mixedInter ℓ τ hτ hτ1).itemFreq i ≤ (1 - τ) * t ^ ℓ + τ * t ^ (ℓ + 1)

theorem KaltonRoberts.WeightedCollection.mixedInter_avgDeficit_le {U : Type u_1} [DecidableEq U] [Fintype U] (C : WeightedCollection U) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) (τ : ℝ) (hτ : 0 ≤ τ) (hτ1 : τ ≤ 1) (f : Finset U → ℝ) (hf : IsApproxAdditive f 1) (M : ℝ) (hM : ∀ (S : Finset U), |f S| ≤ M) (D : ℝ) (hD : 0 ≤ D) (hdeficit : C.avgDeficit f M ≤ D) : (C.mixedInter ℓ τ hτ hτ1).avgDeficit f M ≤ ↑ℓ * D + 2 * (↑ℓ - 1) + τ * (D + 2)