Harris inequality

TheoremHarris inequality#✓fully proved

The Harris inequality (Harris 1960): under the product Bernoulli(p) measure on a finite configuration space, increasing events are positively correlated, P_p(A) * P_p(B) ≤ P_p(A ∩ B). No measurability hypothesis is needed since E is finite. See also IsUpperSet.le_card_inter_finset (Harris–Kleitman, counting form).

theorem harris_inequality [Fintype E] [DecidableEq E] {p : ℝ≥0} (hp : p ≤ 1)
    {A B : Set (ConfigSpace E)} (hA : IsIncreasing A) (hB : IsIncreasing B) :
    (bernoulliProductMeasure (E := E) p hp).real A
        * (bernoulliProductMeasure (E := E) p hp).real B
      ≤ (bernoulliProductMeasure (E := E) p hp).real (A ∩ B)

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Bernoulli product measure on configuration space

Proof usesFKG lattice condition · Log-modular weights satisfy the FKG lattice condition · Probability of an event as a sum of configuration masses · Log-modularity of Bernoulli product weights · Nonnegativity of configuration masses · Configuration masses sum to one · FKG inequality for increasing events

Used byHarris inequality for finitely dependent increasing events

TheoremAn event depends on the coordinates its indicator depends on#✓fully proved

If the indicator of A depends only on the coordinates in S (Mathlib's DependsOn), so does the event A (StatMech.DependsOn).

theorem ih_event_dependsOn_of_indicator {A : Set (ConfigSpace E)} {S : Set E}
    (h : _root_.DependsOn (A.indicator (fun _ => (1 : ℝ))) S) :
    StatMech.DependsOn A S

Uses 3

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

Proof usesAgreement of configurations on a set

TheoremIndicator of an event depends on the coordinates the event depends on#✓fully proved

If the event A depends only on S, so does its indicator function.

theorem ih_indicator_dependsOn_of_event {A : Set (ConfigSpace E)} {S : Set E}
    (h : StatMech.DependsOn A S) :
    _root_.DependsOn (A.indicator (fun _ => (1 : ℝ))) S

Uses 2 · Used by 1

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

Used byIncreasing-event probabilities are monotone in the parameter

TheoremEvents depending on a coordinate set are closed under intersection#✓fully proved

Events depending only on S are closed under intersection.

theorem ih_dependsOn_inter {A B : Set (ConfigSpace E)} {S : Set E}
    (hA : StatMech.DependsOn A S) (hB : StatMech.DependsOn B S) :
    StatMech.DependsOn (A ∩ B) S

Uses 3

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

Proof usesAgreement of configurations on a set

TheoremEvents depending on a coordinate set are closed under unions#✓fully proved

Events depending only on S are closed under arbitrary unions.

theorem ih_dependsOn_iUnion {ι : Sort*} {S : Set E} {A : ι → Set (ConfigSpace E)}
    (hA : ∀ i, StatMech.DependsOn (A i) S) :
    StatMech.DependsOn (⋃ i, A i) S

Uses 3

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

Proof usesAgreement of configurations on a set

DefinitionFilling a finite configuration with closed coordinates#✓fully proved

The configuration on E equal to η on the finite set F and closed (false) off F.

def ih_fill (F : Finset E) (eta : ConfigSpace F) : ConfigSpace E :=
  fun e => if h : e ∈ F then eta ⟨e, h⟩ else false

Uses 1 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model

Used byFinitely dependent event is a cylinder over its section · Monotonicity of the closed filling map · Section of an event on a finite coordinate set · Section of an increasing event is increasing · Section of a disjoint occurrence · Aizenman–Barsky inequality on infinite vertex-transitive graphs

TheoremMonotonicity of the closed filling map#✓fully proved

ih_fill F is monotone.

theorem ih_fill_mono (F : Finset E) : Monotone (ih_fill F)

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Filling a finite configuration with closed coordinates

Used bySection of an increasing event is increasing

DefinitionSection of an event on a finite coordinate set#✓fully proved

The section of an event A on F: the configurations η on F with ih_fill F η ∈ A.

def ih_section (A : Set (ConfigSpace E)) (F : Finset E) : Set (ConfigSpace F) :=
  {eta | ih_fill F eta ∈ A}

Uses 2 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Filling a finite configuration with closed coordinates

Used byFinitely dependent event is a cylinder over its section · Harris inequality for finitely dependent increasing events · Section of an increasing event is increasing · BK inequality on countable configuration spaces · Section of a disjoint occurrence · BK inequality for inhomogeneous measures on a countable set · Aizenman–Barsky inequality on infinite vertex-transitive graphs

TheoremSection of an increasing event is increasing#✓fully proved

The section of an increasing event is increasing.

theorem ih_section_isIncreasing {A : Set (ConfigSpace E)} (hA : IsIncreasing A)
    (F : Finset E) : IsIncreasing (ih_section A F)

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Section of an event on a finite coordinate set

Proof usesFilling a finite configuration with closed coordinates · Monotonicity of the closed filling map

Used byHarris inequality for finitely dependent increasing events · BK inequality on countable configuration spaces · BK inequality for inhomogeneous measures on a countable set

TheoremFinitely dependent event is a cylinder over its section#✓fully proved

An event depending only on the coordinates in F is the cylinder over its section on F.

theorem ih_eq_cylinder_of_dependsOn {A : Set (ConfigSpace E)} (F : Finset E)
    (hA : DependsOn A (F : Set E)) :
    A = MeasureTheory.cylinder F (ih_section A F)

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Section of an event on a finite coordinate set

Proof usesFilling a finite configuration with closed coordinates

Used byHarris inequality for finitely dependent increasing events · BK inequality on countable configuration spaces · BK inequality for inhomogeneous measures on a countable set · Aizenman–Barsky inequality on infinite vertex-transitive graphs

TheoremHarris inequality for finitely dependent increasing events#✓fully proved

The Harris inequality on a countable configuration space for increasing events that depend on finitely many coordinates: P_p(A) * P_p(B) ≤ P_p(A ∩ B).

theorem ih_harris_of_finite_dependsOn {p : ℝ≥0} (hp : p ≤ 1)
    {A B : Set (ConfigSpace E)} (F : Finset E)
    (hAdep : DependsOn A (F : Set E)) (hBdep : DependsOn B (F : Set E))
    (hAinc : IsIncreasing A) (hBinc : IsIncreasing B) :
    (bernoulliProductMeasure (E := E) p hp).real A *
        (bernoulliProductMeasure (E := E) p hp).real B ≤
      (bernoulliProductMeasure (E := E) p hp).real (A ∩ B)

Uses 9

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Increasing event · Bernoulli product measure on configuration space

Proof usesHarris inequality · Finitely dependent event is a cylinder over its section · Section of an event on a finite coordinate set · Section of an increasing event is increasing · Bernoulli product measure of a cylinder event, real-valued form

TheoremPositive correlation passes to decreasing intersections#✓fully proved

Positive correlation passes to limits of decreasing sequences of measurable events: if μ(A n) μ(B n) ≤ μ(A n ∩ B n) for all n, the same holds for ⋂ n, A n and ⋂ n, B n.

theorem ih_harris_iInter_of_antitone
    (mu : Measure (ConfigSpace E)) [IsProbabilityMeasure mu]
    (A B : ℕ → Set (ConfigSpace E))
    (hAanti : Antitone A) (hBanti : Antitone B)
    (hAmeas : ∀ n, MeasurableSet (A n)) (hBmeas : ∀ n, MeasurableSet (B n))
    (hstage : ∀ n, mu.real (A n) * mu.real (B n) ≤ mu.real (A n ∩ B n)) :
    mu.real (⋂ n, A n) * mu.real (⋂ n, B n) ≤
      mu.real ((⋂ n, A n) ∩ (⋂ n, B n))

Uses 1

Statement usesConfiguration space of a statistical-mechanics model

TheoremContinuity from above of a finite measure, real-valued form#✓fully proved

Continuity from above of a finite measure, real-valued form: μ.real (A n) tends to μ.real (⋂ n, A n) for a decreasing sequence of measurable sets.

theorem ih_tendsto_measureReal_iInter {Ω : Type*} [MeasurableSpace Ω]
    (mu : Measure Ω) [IsFiniteMeasure mu]
    (A : ℕ → Set Ω) (hanti : Antitone A)
    (hmeas : ∀ n, MeasurableSet (A n)) :
    Tendsto (fun n => mu.real (A n)) atTop (nhds (mu.real (⋂ n, A n)))

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.