Weighted disjoint-pair sums

DefinitionFirst family in the weighted-pair counterexamples#✓fully proved

The family {∅, {0}} on Fin 2, used in the counterexamples of this file.

def rbyCexA : Finset (Finset (Fin 2)) := {∅, {0}}

Used by 1

Used byDown- and up-compressing two families can decrease disjoint pairs

DefinitionSecond family in the weighted-pair counterexamples#✓fully proved

The family {∅} on Fin 2, used in the counterexamples of this file.

def rbyCexB : Finset (Finset (Fin 2)) := {∅}

Used by 1

Used byDown- and up-compressing two families can decrease disjoint pairs

TheoremDown- and up-compressing two families can decrease disjoint pairs#✓fully proved

Down-compressing 𝒜 and up-compressing ℬ at the same coordinate can strictly decrease the number of disjoint pairs.

theorem rby_separate_compression_strictly_decreases :
    ∃ (𝒜 ℬ : Finset (Finset (Fin 2))) (i : Fin 2),
      (boxDoubled (Down.compression i 𝒜)
        (UV.compression ({i} : Finset (Fin 2)) ∅ ℬ)).card
        < (boxDoubled 𝒜 ℬ).card

Uses 5

Statement usesDoubled family of disjoint pairs

Proof usesSize of the doubled disjoint-pair family · Number of disjoint pairs from two families · First family in the weighted-pair counterexamples · Second family in the weighted-pair counterexamples

DefinitionProduct weight of a finset#✓fully proved

The product weight ∏ x, w x (x ∈ S) of the configuration with support S.

noncomputable def fwt (w : α → Bool → ℝ) (S : Finset α) : ℝ :=
  ∏ x, w x (decide (x ∈ S))

Used by 8

Used byWeighted disjoint pairs as a doubled-weight probability · Down-compression does not decrease weighted disjoint pairs · Weighted down-compression monotonicity fails for general weights · Weight of a family of finsets · Expansion of the Reimer deficit over one coordinate · Weighted number of disjoint pairs · Weighted disjoint pairs bounded by the product of family weights · Box-value bound fails for non-symmetric weights

DefinitionProduct weight of a finset off one coordinate#✓fully proved

The product weight of S over all coordinates except i.

noncomputable def fwt' (w : α → Bool → ℝ) (i : α) (S : Finset α) : ℝ :=
  ∏ x ∈ univ.erase i, w x (decide (x ∈ S))

Used by 5

Used byWeight kernel of disjoint pairs off a coordinate · Down-compression does not decrease weighted disjoint pairs · Weight of a family off one coordinate · Expansion of the Reimer deficit over one coordinate · Weighted number of disjoint pairs off one coordinate

DefinitionWeighted number of disjoint pairs#✓fully proved

The weighted number of disjoint pairs: ∑ fwt w S * fwt w T over disjoint (S, T) ∈ 𝒜 × ℬ.

noncomputable def wdpairs (w : α → Bool → ℝ) (𝒜 ℬ : Finset (Finset α)) : ℝ :=
  ∑ p ∈ (𝒜 ×ˢ ℬ).filter (fun p => Disjoint p.1 p.2), fwt w p.1 * fwt w p.2

Uses 1 · Used by 6

Statement usesProduct weight of a finset

Used byWeighted disjoint pairs as a doubled-weight probability · Down-compression does not decrease weighted disjoint pairs · Weighted down-compression monotonicity fails for general weights · Expansion of the Reimer deficit over one coordinate · Weighted disjoint pairs bounded by the product of family weights · Box-value bound fails for non-symmetric weights

DefinitionWeighted number of disjoint pairs off one coordinate#✓fully proved

wdpairs with coordinate i omitted from the weights.

noncomputable def wdpairs' (w : α → Bool → ℝ) (i : α) (𝒜 ℬ : Finset (Finset α)) : ℝ :=
  ∑ p ∈ (𝒜 ×ˢ ℬ).filter (fun p => Disjoint p.1 p.2), fwt' w i p.1 * fwt' w i p.2

Uses 1 · Used by 2

Statement usesProduct weight of a finset off one coordinate

Used byDown-compression does not decrease weighted disjoint pairs · Expansion of the Reimer deficit over one coordinate

DefinitionWeight of a family of finsets#✓fully proved

The weight ∑ S ∈ 𝒜, fwt w S of a family.

noncomputable def fmarg (w : α → Bool → ℝ) (𝒜 : Finset (Finset α)) : ℝ :=
  ∑ S ∈ 𝒜, fwt w S

Uses 1 · Used by 3

Statement usesProduct weight of a finset

Used byWeighted disjoint pairs as a doubled-weight probability · Expansion of the Reimer deficit over one coordinate · Weighted disjoint pairs bounded by the product of family weights

DefinitionWeight of a family off one coordinate#✓fully proved

fmarg with coordinate i omitted from the weights.

noncomputable def fmarg' (w : α → Bool → ℝ) (i : α) (𝒜 : Finset (Finset α)) : ℝ :=
  ∑ S ∈ 𝒜, fwt' w i S

Uses 1 · Used by 1

Statement usesProduct weight of a finset off one coordinate

Used byExpansion of the Reimer deficit over one coordinate

TheoremWeighted disjoint pairs bounded by the product of family weights#✓fully proved

For nonnegative weights, wdpairs w 𝒜 ℬ ≤ fmarg w 𝒜 * fmarg w ℬ (drop the disjointness constraint).

theorem wdpairs_le_mul {w : α → Bool → ℝ} (hw : ∀ x b, 0 ≤ w x b) (𝒜 ℬ : Finset (Finset α)) :
    wdpairs w 𝒜 ℬ ≤ fmarg w 𝒜 * fmarg w ℬ

Uses 3

Statement usesWeight of a family of finsets · Weighted number of disjoint pairs

Proof usesProduct weight of a finset

TheoremExpansion of the Reimer deficit over one coordinate#✓fully proved

The deficit fmarg w 𝒜 * fmarg w ℬ - wdpairs w 𝒜 ℬ expanded over coordinate i.

theorem wbutterfly_deficit_identity (w : α → Bool → ℝ) (𝒜 ℬ : Finset (Finset α)) (i : α) :
    fmarg w 𝒜 * fmarg w ℬ - wdpairs w 𝒜 ℬ
      = w i true * w i true
          * (fmarg' w i (𝒜.memberSubfamily i) * fmarg' w i (ℬ.memberSubfamily i))
      + w i true * w i false
          * (fmarg' w i (𝒜.memberSubfamily i) * fmarg' w i (ℬ.nonMemberSubfamily i)
              - wdpairs' w i (𝒜.memberSubfamily i) (ℬ.nonMemberSubfamily i))
      + w i false * w i true
          * (fmarg' w i (𝒜.nonMemberSubfamily i) * fmarg' w i (ℬ.memberSubfamily i)
              - wdpairs' w i (𝒜.nonMemberSubfamily i) (ℬ.memberSubfamily i))
      + w i false * w i false
          * (fmarg' w i (𝒜.nonMemberSubfamily i) * fmarg' w i (ℬ.nonMemberSubfamily i)
              - wdpairs' w i (𝒜.nonMemberSubfamily i) (ℬ.nonMemberSubfamily i))

Uses 6

Statement usesWeight of a family of finsets · Weight of a family off one coordinate · Weighted number of disjoint pairs · Weighted number of disjoint pairs off one coordinate

Proof usesProduct weight of a finset · Product weight of a finset off one coordinate

DefinitionBox value of a doubled family under a symmetric weight#✓fully proved

(∏ x, w x true)^2 * #𝒰: for a symmetric weight, the weight of a doubled family.

noncomputable def wboxValue (w : α → Bool → ℝ) (𝒰 : Finset (Finset (α ⊕ α))) : ℝ :=
  (∏ x, w x true) ^ 2 * (𝒰.card : ℝ)

Used by 1

Used byBox-value bound fails for non-symmetric weights

TheoremBox-value bound fails for non-symmetric weights#✓fully proved

For a non-symmetric weight, wdpairs w 𝒜 ℬ ≤ wboxValue w (boxDoubled 𝒜 ℬ) can fail.

theorem wdpairs_not_le_wboxValue_general :
    ∃ (w : Fin 1 → Bool → ℝ),
      (∀ x b, 0 ≤ w x b) ∧
      ¬ (wdpairs w ({∅} : Finset (Finset (Fin 1))) {∅}
          ≤ wboxValue w (boxDoubled ({∅} : Finset (Finset (Fin 1))) {∅}))

Uses 6

Statement usesDoubled family of disjoint pairs · Box value of a doubled family under a symmetric weight · Weighted number of disjoint pairs

Proof usesSize of the doubled disjoint-pair family · Number of disjoint pairs from two families · Product weight of a finset

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.