Discrete correlation inequalities

Stream: maths

[Yaël Dillies]

Two weeks and a half ago, we were looking for probability projects to give to LFTCM participants. @Kalle Kytölä suggested the four functions theorem, aka Ahlswede-Daykin inequality, and I claimed to have formalised it already.

[Yaël Dillies]

This was a lie. I got confused with the Ahlswede-Zhang identity, which is indeed proved and on its way to mathlib (!3#18612).

[Yaël Dillies]

To make up for the calumny, I set to actually prove the Ahlswede-Daykin inequality. After two solid weeks of effort, this is now done, along with a handful of corollaries.

[Yaël Dillies]

Here are the results I have, all available in LeanCamCombi:

• The four functions theorem, in (possibly infinite!) distributive lattices

theorem four_functions_theorem {α β : Type*} [DistribLattice α] [DecidableEq α]
  [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f₁ f₂ f₃ f₄ : α → β)
  (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
  (h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) (s t : Finset α) :
    (∑ a in s, f₁ a) * ∑ a in t, f₂ a ≤
      (∑ a in pointwiseInfs s t, f₃ a) * ∑ a in pointwiseSups s t, f₄ a

All references I could find only talk about finite distributive lattices, but in fact we can restrict the statement to the lattice generated by the finite sets s and t, and this lattice is always finite. This gives us extra generality for free.

• Daykin's inequality

theorem Finset.le_card_infs_mul_card_sups {α : Type*} [DistribLattice α] [DecidableEq α]
  (s t : Finset α) :
    s.card * t.card ≤ (pointwiseInfs s t).card * (pointwiseSups s t).card

• Holley's inequality

theorem holley {α β : Type*} [DistribLattice α] [DecidableEq α] [Fintype α]
  [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f g μ : α → β)
  (hμ₀ : 0 ≤ μ) (hf : 0 ≤ f) (hg : 0 ≤ g) (hμ : Monotone μ)
  (hfg : ∑ a, f a = ∑ a, g a) (h : ∀ a b, f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) :
    ∑ a, μ a * f a ≤ ∑ a, μ a * g a

• The Fortuin-Kastelyn-Ginibre inequality

theorem fkg {α β : Type*} [DistribLattice α] [DecidableEq α] [Fintype α]
  [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f g μ : α → β)
  (hμ₀ : 0 ≤ μ) (hf₀ : 0 ≤ f) (hg₀ : 0 ≤ g) (hf : Monotone f) (hg : Monotone g)
  (hμ : ∀ a b, μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) :
    (∑ a, μ a * f a) * ∑ a, μ a * g a ≤ (∑ a, μ a) * ∑ a, μ a * (f a * g a)

• The Marica-Schönheim inequality, in generalised Boolean algebras. This is usually stated for finite Boolean algebras, but doesn't refer to compl, so we can go onto the Boolean algebra generated by our generalised Boolean algebra, prove the statement there, then pull back.

lemma Finset.le_card_diffs_mul_card_diffs {α : Type*} [DecidableEq α]
  [GeneralizedBooleanAlgebra α] (s t : Finset α),
    card s * card t ≤ card (pointwiseDiffs s t) * card (pointwiseDiffs t s)

theorem Finset.card_le_card_diffs {α : Type*} [DecidableEq α]
  [GeneralizedBooleanAlgebra α] (s : Finset α),
    card s  ≤ card (pointwiseDiffs s s)

• The Marica-Schönheim special case of Graham's conjecture. This uses the Marica-Schönheim inequality in an infinite generalized Boolean algebra without complements (namely Finset ℕ), so both our generalisations of Ahlswede-Daykin to infinite distributive lattices and of Marica-Schönheim to generalised Boolean algebras were necessary.

theorem marica_schoenheim {n : ℕ} (f : ℕ → ℕ) (hn : n ≠ 0) (hf : StrictMonoOn f (Set.Iio n))
    (hf' : ∀ k < n, Squarefree (f k)) : ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i

[Yaël Dillies]

Of course, a formalisation wouldn't be fun without its boatload of unforeseen prerequisites. So here are some highlights from the past two weeks:

• Birkhoff's representation theorem: Any finite distributive lattice can be embedded into a finite powerset

lemma exists_birkhoff_representation.{u} (α : Type u) [Finite α] [DistribLattice α] :
    ∃ (β : Type u) (_ : DecidableEq β) (_ : Fintype β) (f : LatticeHom α (Finset β)),
      Injective f

• The Boolean algebra generated by a generalised Boolean algebra

/-- Boolean algebra containing a given generalised Boolean algebra `α` as a sublattice. -/
def Booleanisation (α : Type*) := α ⊕ α

instance instBooleanAlgebra : BooleanAlgebra (Booleanisation α)

/-- The embedding from a generalised Boolean algebra to its generated Boolean algebra. -/
def inlLatticeHom : LatticeHom α (Booleanisation α)

lemma inlLatticeHom_injective : Injective (inlLatticeHom (α := α))

• Pointwise set difference of finite families and the API that goes with it

def diffs {α : Type*} [GeneralizedBooleanAlgebra α] :
    Finset α → Finset α → Finset α := image₂ (· \ ·)

• Sublattices

structure Sublattice (α : Type*) [Lattice α] where
  carrier : Set α
  supClosed' : SupClosed carrier
  infClosed' : InfClosed carrier

• Sublattice generated by a set, and the fact that it is finite if the generating set is
• Fancy new highly functional ClosureOperator API. After years of complaining about my own API, I've finally found a way to improve it.

[Yaël Dillies]

There are a few more low-hanging fruits from here:

• Golf the mathlib proof of the Harris-Kleitman inequality (docs#IsLowerSet.le_card_inter_finset), which I did a year ago without knowing that it was a corollary of Ahlswede-Daykin.
• The XYZ inequality, aka Fishburn-Shepp

[Yaël Dillies]

In terms of size, this is about 2000 lines of material spread across 25 files. I am hoping to PR all that to mathlib shortly with the maintainers' collaboration, but my term is starting next week.

[Kalle Kytölä]

Brilliant!

Does this work more generally? Yaël, have you by any chance proven the lost fur mat theorem or the ferment lust theorem or anything like that? (If you have, then the follow-up is obvious: we just need to trick you into reading a subsequent message carelessly and then wait for LeanCamCombi to catch up...) :grinning_face_with_smiling_eyes:

Ok, but this is seriously nice! I hope especially Holley and FKG are PRd to Mathlib in not too distant future. They would pretty instantly enable some interesting percolation results, and I certainly have also other applications in mind in a slightly longer term. (I suspect @Vincent Beffara would have even more...).

[Yaël Dillies]

I actually looked up what the lost fur mat theorem was. :smiling_face_with_tear:

[Kevin Buzzard]

Please feel free into being tricked into working for me for two solid weeks :-)

[Yaël Dillies]

@Kalle Kytölä, since you're so excited about the result, I spent a few hours this morning opening prerequisite PRs. I've collated them in a Github project. Review as it suits you :wink: : https://github.com/orgs/leanprover-community/projects/12/views/1

[Kalle Kytölä]

The link to the Github project doesn't work for me... (Organizing the PRs like that sounds quite helpful in principle, though.)

I'd be happy to try to review if there are sufficiently simple pieces for someone who isn't yet well-versed in Mathlib's tricks and design. (Also the earliest I can try is the weekend and I can't even promise to have time then.)

And yes, I'm indeed very happy about this. Thanks a lot for getting confused!

[Yaël Dillies]

Hmm, would a @maintainers mind changing the visibility of the project from private to something else?

[Yaël Dillies]

Update: I've just PRed the second big result, namely Birkhoff's representation theorem, in #7417. It depends on #7374, #7375, #7416 which are all ready for review (and pretty easy).

[Sebastien Gouezel]

λ is forbidden in mathlib, can you use fun instead in these PRs?

[Yaël Dillies]

Done

[Yaël Dillies]

Update: I've opened the last big prerequisite: sublattices (#7549). Four functions itself is now living at #7551. I highly encourage people to have a look at the Github project and review the three prerequisite PRs remaining.

[Eric Wieser]

There are still lots of lambdas there

[Yaël Dillies]

Update: Birkhoff's representation theorem (#7417) is up for grab!

[Yaël Dillies]

Now three PRs away!

• #7417: Birkhoff's representation theorem
• #7549: Sublattices
• #7551: Four functions theorem

[Yaël Dillies]

... and now the main PR is ready to be reviewed: #7551

[Yaël Dillies]

It's in! :tada: