Down-compression and disjoint pairs

DefinitionSupport of a configuration as a finset#✓fully proved

The support {i | ω i = true} of a configuration, as a finset.

def cfgSupport [Fintype E] [DecidableEq E] (ω : ConfigSpace E) : Finset E :=
  Finset.univ.filter (fun i => ω i = true)

Uses 1 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model

Used byWeighted disjoint pairs as a doubled-weight probability · Configurations on a finite set as finsets · Down-compression of a family of configurations · Event of a family of finsets · Reimer's inequality for two lower families · Reimer's inequality for two upper families

DefinitionConfiguration with a given support#✓fully proved

The configuration whose open coordinates are exactly the elements of s.

def supportCfg [DecidableEq E] (s : Finset E) : ConfigSpace E := fun i => decide (i ∈ s)

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byWeighted disjoint pairs as a doubled-weight probability · Configurations on a finite set as finsets · Down-compression of a family of configurations

DefinitionConfigurations on a finite set as finsets#✓fully proved

Configurations on a finite set are the same as finsets (their supports).

def cfgEquivFinset [Fintype E] [DecidableEq E] : ConfigSpace E ≃ Finset E where
  toFun := cfgSupport
  invFun := supportCfg
  left_inv := supportCfg_cfgSupport
  right_inv := cfgSupport_supportCfg

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Support of a configuration as a finset · Configuration with a given support

Used byWeighted disjoint pairs as a doubled-weight probability

DefinitionDown-compression of a family of configurations#✓fully proved

Down-compression at i of a family of configurations, through cfgEquivFinset.

noncomputable def downCompress [Fintype E] [DecidableEq E] (i : E)
    (𝒜 : Finset (ConfigSpace E)) : Finset (ConfigSpace E) :=
  (Down.compression i (𝒜.image cfgSupport)).image supportCfg

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Support of a configuration as a finset · Configuration with a given support

TheoremReimer's inequality on one coordinate#✓fully proved

Reimer's inequality on one coordinate, for all events.

theorem reimer_wprob_one (φ : Fin 1 → Bool → ℝ)
    (hφ0 : ∀ i b, 0 ≤ φ i b) (hφ1 : ∀ i, φ i false + φ i true = 1)
    (A B : Set (ConfigSpace (Fin 1))) :
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events · Weighted probability of an event

Proof usesOccurrence of an event on a coordinate set · An event occurring on a set contains the configuration · Agreement of configurations on a set · Membership in a disjoint occurrence · Product weight of a configuration

DefinitionEvent depending only on a set of coordinates#✓fully proved

DependsOn A S: whether a configuration lies in A depends only on its values on S. This is Mathlib's DependsOn for the membership predicate of A.

def DependsOn (A : Set (ConfigSpace E)) (S : Set E) : Prop :=
  ∀ ω ω', agreeOn S ω ω' → (ω ∈ A ↔ ω' ∈ A)

Uses 2 · Used by 21

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations on a set

Used byEvents depending on a coordinate set are closed under unions · Events depending on a coordinate set are closed under intersection · Finitely dependent event is a cylinder over its section · An event depends on the coordinates its indicator depends on · Harris inequality for finitely dependent increasing events · Indicator of an event depends on the coordinates the event depends on · Union bound from the three-event BK inequality · Disjoint occurrence preserves finite dependence · BK inequality on countable configuration spaces · Increasing-event probabilities are monotone in the parameter · Occurrence of a finitely dependent event within its window · BK inequality for three increasing events · BK inequality for inhomogeneous measures on a countable set · Reimer equality for a left event and a right event · Disjoint occurrence equals intersection for disjoint dependence sets · Reimer's inequality for events on disjoint coordinate sets · Independence of events on complementary coordinate sets · Determined-by and depends-on are the same predicate · Independence of events determined by disjoint coordinate sets · Monotonicity in \(p\) of the Bernoulli percolation probability · Aizenman–Barsky inequality on infinite vertex-transitive graphs

TheoremDisjoint occurrence equals intersection for disjoint dependence sets#✓fully proved

If A depends only on S, B only on T, and S, T are disjoint, then A □ B = A ∩ B.

theorem disjointOccurrence_eq_inter_of_dependsOn {A B : Set (ConfigSpace E)} {S T : Set E}
    (hA : DependsOn A S) (hB : DependsOn B T) (hST : Disjoint S T) :
    disjointOccurrence A B = A ∩ B

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · An event occurring on a set contains the configuration · Agreement of configurations on a set · Disjoint occurrence lies in the intersection

Used byReimer's inequality for events on disjoint coordinate sets

TheoremIndependence of events on complementary coordinate sets#✓fully proved

Events depending on complementary coordinate sets are independent under a product probability weight.

theorem wprob_inter_mul_of_split [Fintype E] [DecidableEq E] (P : E → Prop)
    (φ : E → Bool → ℝ) (hφ1 : ∀ x, φ x false + φ x true = 1)
    {A B : Set (ConfigSpace E)} (hA : DependsOn A {x | P x}) (hB : DependsOn B {x | ¬ P x}) :
    wprob φ (A ∩ B) = wprob φ A * wprob φ B

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Weighted probability of an event

Proof usesAgreement of configurations on a set · Product weight of a configuration · Product probability weight has total mass one

Used byReimer's inequality for events on disjoint coordinate sets · Independence of events determined by disjoint coordinate sets

TheoremReimer's inequality for events on disjoint coordinate sets#✓fully proved

Reimer's inequality, with equality, for events depending on disjoint coordinate sets.

theorem reimer_wprob_of_disjoint_support [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (hφ1 : ∀ x, φ x false + φ x true = 1)
    {A B : Set (ConfigSpace E)} {S T : Set E}
    (hA : DependsOn A S) (hB : DependsOn B T) (hST : Disjoint S T) :
    wprob φ (disjointOccurrence A B) = wprob φ A * wprob φ B

Uses 8 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Disjoint occurrence of events · Weighted probability of an event

Proof usesAgreement of configurations on a set · Agreement on a set restricts to subsets · Disjoint occurrence equals intersection for disjoint dependence sets · Independence of events on complementary coordinate sets

Used byReimer equality for a left event and a right event · Reimer equality for events determined by disjoint coordinates

DefinitionNumber of disjoint pairs from two families#✓fully proved

The number of disjoint pairs (S, T) ∈ 𝒜 × ℬ.

def dpairsCount (𝒜 ℬ : Finset (Finset α)) : ℕ :=
  ((𝒜 ×ˢ ℬ).filter (fun p => Disjoint p.1 p.2)).card

Used by 5

Used byDown-compression does not decrease the disjoint-pair count · Recursion for disjoint pairs by membership of a coordinate · One compression step on the doubled disjoint-pair family · Down- and up-compressing two families can decrease disjoint pairs · Box-value bound fails for non-symmetric weights

TheoremRecursion for disjoint pairs by membership of a coordinate#✓fully proved

Splitting disjoint pairs by membership of i: pairs where neither, only the first, or only the second set contains i.

theorem dpairsCount_fiber_recursion (𝒜 ℬ : Finset (Finset α)) (i : α) :
    dpairsCount 𝒜 ℬ
      = dpairsCount (𝒜.nonMemberSubfamily i) (ℬ.nonMemberSubfamily i)
      + dpairsCount (𝒜.memberSubfamily i) (ℬ.nonMemberSubfamily i)
      + dpairsCount (𝒜.nonMemberSubfamily i) (ℬ.memberSubfamily i)

Uses 1 · Used by 2

Statement usesNumber of disjoint pairs from two families

Used byDown-compression does not decrease the disjoint-pair count · One compression step on the doubled disjoint-pair family

TheoremOne compression step on the doubled disjoint-pair family#✓fully proved

Bookkeeping for one compression step at coordinate i on boxDoubled 𝒜 ℬ: doubleCompress i preserves its size and makes it down-closed at inl i and up-closed at inr i, and sizes split over memberSubfamily i and nonMemberSubfamily i.

theorem reimer_butterfly_compress_step (𝒜 ℬ : Finset (Finset α)) (i : α) :
    (doubleCompress i (boxDoubled 𝒜 ℬ)).card = (boxDoubled 𝒜 ℬ).card
    ∧ IsDownAtLeft i (doubleCompress i (boxDoubled 𝒜 ℬ))
    ∧ IsUpAtRight i (doubleCompress i (boxDoubled 𝒜 ℬ))
    ∧ (boxDoubled 𝒜 ℬ).card
        = (boxDoubled (𝒜.nonMemberSubfamily i) (ℬ.nonMemberSubfamily i)).card
        + (boxDoubled (𝒜.memberSubfamily i) (ℬ.nonMemberSubfamily i)).card
        + (boxDoubled (𝒜.nonMemberSubfamily i) (ℬ.memberSubfamily i)).card
    ∧ (𝒜.memberSubfamily i).card + (𝒜.nonMemberSubfamily i).card = 𝒜.card
    ∧ (ℬ.memberSubfamily i).card + (ℬ.nonMemberSubfamily i).card = ℬ.card

Uses 10

Statement usesFamily closed under erasing the left copy · Family closed under inserting the right copy · Doubled family of disjoint pairs · Double compression at a coordinate

Proof usesSize of the doubled disjoint-pair family · Down-compression at the left copy of a coordinate · Number of disjoint pairs from two families · Recursion for disjoint pairs by membership of a coordinate · Up-compression at a point of the doubled ground set · Up-compression at the right copy of a coordinate

TheoremDown-compression does not decrease the disjoint-pair count#✓fully proved

Down-compressing both families at i does not decrease the number of disjoint pairs.

theorem dpairsCount_downDown_mono (𝒜 ℬ : Finset (Finset α)) (i : α) :
    dpairsCount 𝒜 ℬ ≤ dpairsCount (Down.compression i 𝒜) (Down.compression i ℬ)

Uses 2

Statement usesNumber of disjoint pairs from two families

Proof usesRecursion for disjoint pairs by membership of a coordinate

DefinitionWeight kernel of disjoint pairs off a coordinate#✓fully proved

fwt' w i S * fwt' w i T for disjoint S, T, and 0 otherwise.

noncomputable def pairKernel' (w : α → Bool → ℝ) (i : α) (S T : Finset α) : ℝ :=
  if Disjoint S T then fwt' w i S * fwt' w i T else 0

Uses 1 · Used by 1

Statement usesProduct weight of a finset off one coordinate

Used byDown-compression does not decrease weighted disjoint pairs

TheoremDown-compression does not decrease weighted disjoint pairs#✓fully proved

Down-compressing both families at i does not decrease the weighted number of disjoint pairs when w i true ≤ w i false.

theorem wdpairs_downDown_mono {w : α → Bool → ℝ} (hw : ∀ x b, 0 ≤ w x b) (i : α)
    (hdom : w i true ≤ w i false) (𝒜 ℬ : Finset (Finset α)) :
    wdpairs w 𝒜 ℬ ≤ wdpairs w (Down.compression i 𝒜) (Down.compression i ℬ)

Uses 5

Statement usesWeighted number of disjoint pairs

Proof usesProduct weight of a finset · Product weight of a finset off one coordinate · Weight kernel of disjoint pairs off a coordinate · Weighted number of disjoint pairs off one coordinate

TheoremWeighted down-compression monotonicity fails for general weights#✓fully proved

Without w i true ≤ w i false, wdpairs_downDown_mono can fail.

theorem wdpairs_downDown_not_mono_general :
    ∃ (w : Fin 1 → Bool → ℝ) (𝒜 ℬ : Finset (Finset (Fin 1))) (i : Fin 1),
      (∀ x b, 0 ≤ w x b) ∧
      ¬ (wdpairs w 𝒜 ℬ ≤ wdpairs w (Down.compression i 𝒜) (Down.compression i ℬ))

Uses 2

Statement usesWeighted number of disjoint pairs

Proof usesProduct weight of a finset

DefinitionIterated down-compression along a list of coordinates#✓fully proved

Down-compression at each coordinate of cs in turn (the head of cs is applied last).

def iterDownComp (cs : List α) (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
  cs.foldr Down.compression 𝒜

Used by 1

Used byIterated down-compression reaches a lower set

DefinitionDown-compression map on a single finset#✓fully proved

The compression map: erase i from s when s contains i and s.erase i ∉ 𝒜.

noncomputable def cmap (i : α) (𝒜 : Finset (Finset α)) (s : Finset α) : Finset α :=
  if i ∈ s ∧ s.erase i ∉ 𝒜 then s.erase i else s

Used by 1

Used byIterated down-compression reaches a lower set

DefinitionTotal size of a family of finsets#✓fully proved

The total size ∑ S ∈ 𝒜, #S of a family.

noncomputable def totalSize (𝒜 : Finset (Finset α)) : ℕ := ∑ S ∈ 𝒜, S.card

Used by 1

Used byIterated down-compression reaches a lower set

TheoremIterated down-compression reaches a lower set#✓fully proved

Some iterated down-compression of 𝒜 is a lower set.

theorem exists_iterDownComp_isLowerSet (𝒜 : Finset (Finset α)) :
    ∃ cs : List α, IsLowerSet ((iterDownComp cs 𝒜) : Set (Finset α))

Uses 3

Statement usesIterated down-compression along a list of coordinates

Proof usesDown-compression map on a single finset · Total size of a family of finsets

TheoremMembers of a disjoint-union family avoiding a coordinate#✓fully proved

The members of 𝒜 ○ ℬ avoiding i are exactly the disjoint unions of members of 𝒜 and ℬ avoiding i.

theorem boxFamily_filter_notMem_coord (i : α) (𝒜 ℬ : Finset (Finset α)) :
    (𝒜 ○ ℬ).filter (fun U => i ∉ U)
      = (𝒜.filter (fun S => i ∉ S)) ○ (ℬ.filter (fun T => i ∉ T))

DefinitionFamily closed under erasing a coordinate#✓fully proved

IsDownAtCoord i 𝒜: the family 𝒜 is closed under erasing i.

def IsDownAtCoord (i : α) (𝒜 : Finset (Finset α)) : Prop := ∀ s ∈ 𝒜, s.erase i ∈ 𝒜

Used by 1

Used byLower sets are families closed under erasing an element

DefinitionFirst family in the box-compression counterexample#✓fully proved

The family {∅, {1}} on Fin 2, the first family of the counterexample StatMech.reimerStep_box_compression_false.

def reimerStepCexA : Finset (Finset (Fin 2)) := {∅, {1}}

Used by 1

Used byDown-compression can shrink the disjoint-union family

DefinitionSecond family in the box-compression counterexample#✓fully proved

The family {∅, {0, 1}} on Fin 2, the second family of the counterexample StatMech.reimerStep_box_compression_false.

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

Used by 1

Used byDown-compression can shrink the disjoint-union family

TheoremDown-compression can shrink the disjoint-union family#✓fully proved

Down-compressing both families at the same coordinate can strictly decrease the size of 𝒜 ○ ℬ.

theorem reimerStep_box_compression_false :
    ∃ (𝒜 ℬ : Finset (Finset (Fin 2))) (i : Fin 2),
      (Down.compression i 𝒜 ○ Down.compression i ℬ).card < (𝒜 ○ ℬ).card

Uses 2

Proof usesFirst family in the box-compression counterexample · Second family in the box-compression counterexample

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.