Formalizing Choquet-Deny theorem

Stream: new members

[Peter Kosenko]

Hi! After lurking here for a while, I was very recently inspired to grab Mathematics In Lean and work through the basics in order to learn Lean and Mathlib.

I set myself a modest goal to formalize some basic facts about harmonic functions on discrete groups. I have recorded my partial progress to the github.

• My very first attempt is contained in the HarmonicPMF.lean file, it took me a while to realize the awkwardness of working with discrete probability measures. I was only able to formalize the triviality of bounded harmonic functions on finite groups with help from Aristotle, but the proof is rather hard to read and I would like to go and refine it a bit more.
• One of my goals was to actually show that any bounded harmonic function on an abelian group is trivial (wrt to any measure with support generating the group) @Sébastien Gouëzel suggested an alternative and more general formulation for the topological version of the Choquet-Deny theorem, which seems much more suited for Lean formalization. I got good progress but I still have many sorry's due to having to prove integrability of functions used in the proof.
• In the email correspondence @Sébastien Gouëzel suggested to think about the statement a bit more carefully -- I am not sure we require regularity? Seems we only use Fubini-Tonelli in the proof, as we only interchange the integrals for non-negative functions. We need some kind of non-degeneracy though.
• After I am done with Choquet-Deny, I could try formalizing Poisson boundaries using either the universal property or unique realization of bounded harmonic function using the Poisson representation.

Any feedback is appreciated!

[Jakub Nowak]

I think that the problem with proofs generated by Aristotle is that it tends to use lots of super convoluted syntax and arguments. Understanding proofs generated by Aristotle can be daunting task even for people experience with Lean. Basically, I feel like using Aristotle is a one-way ticket. You should never ever try to read proofs that is has generated.

[Peter Kosenko]

Yeah, unfortunately I don't feel like I learned anything from the completed proofs the LLM gave me (it does abuse refine' a lot, which the linter complains about!). I will probably refrain on relying exclusively on Aristotle as I am still learning Lean.

[Sébastien Gouëzel]

What you can do is try to get a proof with many assumptions, and then think harder to see if you can remove them (possibly with a different proof) or if they are really necessary. But the first step is definitely to get some proof (but not over finite groups because there sums over finite sets are too different from the natural general setting). Also, I agree that you will learn a lot more by writing by hand your own proofs than by using LLMs -- also LLMs can point you in some proof strategy directions, and give you the names of useful lemmas.

[Bbbbbbbbba]

Peter Kosenko said:

Yeah, unfortunately I don't feel like I learned anything from the completed proofs the LLM gave me (it does abuse refine' a lot, which the linter complains about!). I will probably refrain on relying exclusively on Aristotle as I am still learning Lean.

The refine' problem, if I understand correctly, is superficial. Just replace them with refine and replace some _ with ?_ as appropriate.

[Bbbbbbbbba]

Jakub Nowak said:

I think that the problem with proofs generated by Aristotle is that it tends to use lots of super convoluted syntax and arguments. Understanding proofs generated by Aristotle can be daunting task even for people experience with Lean. Basically, I feel like using Aristotle is a one-way ticket. You should never ever try to read proofs that is has generated.

That's interesting, because I find Aristotle proofs pretty editable, although maybe it is that my problem was easy enough that it did not give Aristotle enough space to convolute.

[Weiyi Wang]

Sometimes Aristotle can do more than necessary, like it loves simp_all +decide [...] and often a simple `simp [...] works

[Jakub Nowak]

I didn't try Aristotle myself yet, my experience is only from code I've seen people post. My experience is that Aristotle is like an experienced mathematician that learned Lean yesterday but is very determined to finish the proof.
It can come up with good ideas and can brake proof into smaller steps. But it often misses relevant useful lemmas from mathlib and reproves things that are already proven there. It often uses defeq abuse. Instead of rethinking that it should use a different API, it will throw in conversions and defeq abuse everywhere.

[Bbbbbbbbba]

I thought missing relevant useful lemmas is something humans still do after months of using Lean...

[Jakub Nowak]

Yes and no. When I think I need some argument that I think it should be in mathlib and can't find it, then I ask on zulip. And I either get an asnwer or I add the lemma to mathlib.

[Bbbbbbbbba]

Imagine if Aristotle had an account on zulip :joy:

[Peter Kosenko]

I have finished v1 of the proof of the Choquet-Deny theorem, no sorry terms remaining.

theorem ChoquetDeny {G : Type*} [AddCommGroup G] [TopologicalSpace G]
[SecondCountableTopology G] [MeasurableSpace G]
[BorelSpace G] [IsTopologicalAddGroup G]
(μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ]
(f : G → ℝ) (hfmeas : Measurable f)
(hfbnd : ∃ (C : ℝ), ∀ (x : G), |f x| ≤ C)
(hfint : ∀ (x : G), ∫ y, f (x + y) ∂μ = f x) : ∀ (x : G), ∀ᵐ (y : G) ∂μ, f x = f (x + y)

I had to require my group to be second countable due to some issues when I applied the Fubini theorem, but due to the way I stated the conclusion, we don't need regularity of $\mu$ at this step. It should be enough to require that the support of the measure generates the group -- we only need a condition like that to show that $\int |f|^2 d\mu = 0 \iff f = 0 \mu-a.e$.

[Peter Kosenko]

Next step is to refine the proof and document the lemmas and steps more carefully.