Doubled ground set in Reimer's proof

DefinitionEncoding a pair of finsets in the doubled ground set#✓fully proved

The finset inl '' S ∪ inr '' T of α ⊕ α, encoding the pair (S, T).

noncomputable def dbl (S T : Finset α) : Finset (α ⊕ α) :=
  S.map ⟨Sum.inl, Sum.inl_injective⟩ ∪ T.map ⟨Sum.inr, Sum.inr_injective⟩

Used by 4

Used byDoubled family of disjoint pairs · Size of the doubled disjoint-pair family · Disjoint-union family is no larger than the doubled family · Weighted disjoint pairs as a doubled-weight probability

DefinitionDoubled family of disjoint pairs#✓fully proved

The family of dbl S T over disjoint pairs S ∈ 𝒜, T ∈ ℬ.

noncomputable def boxDoubled (𝒜 ℬ : Finset (Finset α)) : Finset (Finset (α ⊕ α)) :=
  ((𝒜 ×ˢ ℬ).filter (fun p => Disjoint p.1 p.2)).image (fun p => dbl p.1 p.2)

Uses 1 · Used by 6

Statement usesEncoding a pair of finsets in the doubled ground set

Used bySize of the doubled disjoint-pair family · Disjoint-union family is no larger than the doubled family · Weighted disjoint pairs as a doubled-weight probability · 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

TheoremSize of the doubled disjoint-pair family#✓fully proved

The size of boxDoubled 𝒜 ℬ is the number of disjoint pairs in 𝒜 × ℬ.

theorem card_boxDoubled (𝒜 ℬ : Finset (Finset α)) :
    (boxDoubled 𝒜 ℬ).card = ((𝒜 ×ˢ ℬ).filter (fun p => Disjoint p.1 p.2)).card

Uses 2 · Used by 3

Statement usesDoubled family of disjoint pairs

Proof usesEncoding a pair of finsets in the doubled ground set

Used byOne 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

TheoremDisjoint-union family is no larger than the doubled family#✓fully proved

#(𝒜 ○ ℬ) ≤ #(boxDoubled 𝒜 ℬ): distinct disjoint pairs can have the same union.

theorem card_boxFamily_le_boxDoubled (𝒜 ℬ : Finset (Finset α)) :
    (𝒜 ○ ℬ).card ≤ (boxDoubled 𝒜 ℬ).card

Uses 2

Statement usesDoubled family of disjoint pairs

Proof usesEncoding a pair of finsets in the doubled ground set

DefinitionUp-compression at a point of the doubled ground set#✓fully proved

Up-compression of a family on α ⊕ α at the point a (UV.compression {a} ∅).

noncomputable def upComp (a : α ⊕ α) (𝒜 : Finset (Finset (α ⊕ α))) : Finset (Finset (α ⊕ α)) :=
  UV.compression {a} ∅ 𝒜

Used by 2

Used byUp-compression at the right copy of a coordinate · One compression step on the doubled disjoint-pair family

DefinitionDown-compression at the left copy of a coordinate#✓fully proved

Down-compression at the left copy inl i.

noncomputable def downLeft (i : α) (𝒜 : Finset (Finset (α ⊕ α))) : Finset (Finset (α ⊕ α)) :=
  Down.compression (Sum.inl i) 𝒜

Used by 2

Used byDouble compression at a coordinate · One compression step on the doubled disjoint-pair family

DefinitionUp-compression at the right copy of a coordinate#✓fully proved

Up-compression at the right copy inr i.

noncomputable def upRight (i : α) (𝒜 : Finset (Finset (α ⊕ α))) : Finset (Finset (α ⊕ α)) :=
  upComp (Sum.inr i) 𝒜

Uses 1 · Used by 2

Statement usesUp-compression at a point of the doubled ground set

Used byDouble compression at a coordinate · One compression step on the doubled disjoint-pair family

DefinitionDouble compression at a coordinate#✓fully proved

Down-compression at inl i followed by up-compression at inr i.

noncomputable def doubleCompress (i : α) (𝒜 : Finset (Finset (α ⊕ α))) :
    Finset (Finset (α ⊕ α)) :=
  upRight i (downLeft i 𝒜)

Uses 2 · Used by 1

Statement usesDown-compression at the left copy of a coordinate · Up-compression at the right copy of a coordinate

Used byOne compression step on the doubled disjoint-pair family

DefinitionFamily closed under erasing the left copy#✓fully proved

IsDownAtLeft i 𝒜: 𝒜 is closed under erasing inl i.

def IsDownAtLeft (i : α) (𝒜 : Finset (Finset (α ⊕ α))) : Prop :=
  ∀ s ∈ 𝒜, s.erase (Sum.inl i) ∈ 𝒜

Used by 1

Used byOne compression step on the doubled disjoint-pair family

DefinitionFamily closed under inserting the right copy#✓fully proved

IsUpAtRight i 𝒜: 𝒜 is closed under inserting inr i.

def IsUpAtRight (i : α) (𝒜 : Finset (Finset (α ⊕ α))) : Prop :=
  ∀ s ∈ 𝒜, insert (Sum.inr i) s ∈ 𝒜

Used by 1

Used byOne compression step on the doubled disjoint-pair family

DefinitionLeft copy in the doubled ground set#✓fully proved

The left copy {inl a} of α in α ⊕ α.

def leftBlock : Set (α ⊕ α) := {x | x.isLeft}

Used by 1

Used byReimer equality for a left event and a right event

DefinitionRight copy in the doubled ground set#✓fully proved

The right copy {inr a} of α in α ⊕ α.

def rightBlock : Set (α ⊕ α) := {x | x.isRight}

Used by 1

Used byReimer equality for a left event and a right event

DefinitionRestriction of a doubled configuration to the left copy#✓fully proved

The restriction of a configuration on α ⊕ α to the left copy.

def leftCfg (ω : ConfigSpace (α ⊕ α)) : ConfigSpace α := fun a => ω (Sum.inl a)

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byEvent on the left copy of the doubled ground set · Reimer equality for a left event and a right event

DefinitionRestriction of a doubled configuration to the right copy#✓fully proved

The restriction of a configuration on α ⊕ α to the right copy.

def rightCfg (ω : ConfigSpace (α ⊕ α)) : ConfigSpace α := fun a => ω (Sum.inr a)

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byReimer equality for a left event and a right event · Event on the right copy of the doubled ground set

DefinitionEvent on the left copy of the doubled ground set#✓fully proved

The event on α ⊕ α that the left restriction lies in A.

def leftEvent (A : Set (ConfigSpace α)) : Set (ConfigSpace (α ⊕ α)) := {ω | leftCfg ω ∈ A}

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a doubled configuration to the left copy

Used byReimer equality for a left event and a right event

DefinitionEvent on the right copy of the doubled ground set#✓fully proved

The event on α ⊕ α that the right restriction lies in B.

def rightEvent (B : Set (ConfigSpace α)) : Set (ConfigSpace (α ⊕ α)) := {ω | rightCfg ω ∈ B}

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a doubled configuration to the right copy

Used byReimer equality for a left event and a right event

DefinitionDoubled coordinate weight#✓fully proved

The coordinate weight w on both copies of α.

def doubleWeight (w : α → Bool → ℝ) : (α ⊕ α) → Bool → ℝ := Sum.elim w w

Used by 1

Used byWeighted disjoint pairs as a doubled-weight probability

TheoremReimer equality for a left event and a right event#✓fully proved

Reimer's inequality, with equality, for a left event and a right event.

theorem reimer_wprob_doubled_split (φ : (α ⊕ α) → Bool → ℝ)
    (hφ1 : ∀ x, φ x false + φ x true = 1) (A B : Set (ConfigSpace α)) :
    wprob φ (disjointOccurrence (leftEvent A) (rightEvent B))
      = wprob φ (leftEvent A) * wprob φ (rightEvent B)

Uses 12

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events · Event on the left copy of the doubled ground set · Event on the right copy of the doubled ground set · Weighted probability of an event

Proof usesEvent depending only on a set of coordinates · Agreement of configurations on a set · Left copy in the doubled ground set · Restriction of a doubled configuration to the left copy · Reimer's inequality for events on disjoint coordinate sets · Right copy in the doubled ground set · Restriction of a doubled configuration to the right copy

TheoremWeighted disjoint pairs as a doubled-weight probability#✓fully proved

wdpairs w 𝒜 ℬ is the doubled-weight probability of familyEvent (boxDoubled 𝒜 ℬ).

theorem wprob_familyEvent_boxDoubled_eq_wdpairs (w : α → Bool → ℝ) (𝒜 ℬ : Finset (Finset α)) :
    wprob (doubleWeight w) (familyEvent (boxDoubled 𝒜 ℬ)) = wdpairs w 𝒜 ℬ

Uses 13

Statement usesDoubled family of disjoint pairs · Doubled coordinate weight · Event of a family of finsets · Weighted number of disjoint pairs · Weighted probability of an event

Proof usesConfiguration space of a statistical-mechanics model · Configurations on a finite set as finsets · Support of a configuration as a finset · Encoding a pair of finsets in the doubled ground set · Weight of a family of finsets · Product weight of a finset · Product weight of a configuration · Configuration with a given support

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.