complete proof of iIndepFun.pi #131
Conversation
| lemma iIndepFun.prod (h : iIndepFun n f μ) : | ||
| let β := fun k ↦ Π i : ST k, α i | ||
| iIndepFun (β := β) (fun k ↦ MeasurableSpace.pi) | ||
| (fun (k : ι') (x : Ω) (i : ST k) ↦ f i x) μ := by |
There was a problem hiding this comment.
How do you feel about this lemma now that you've proved the "correct" one? Do you think this one should go in mathlib, or should we ditch it?
There was a problem hiding this comment.
In practical situations I think this one can be pretty useful. It's not clear to me if the application in endgame would be nicer with iIndepFun.prod or iIndepFun.pi.
There was a problem hiding this comment.
My proof of iIndepFun.prod is quite hacky (in particular I have this weird lemma exists_indexfn that really shouldn't take up so much space). If it can be deduced as a corollary of iIndepFun.pi then I'd be more than happy to replace my proof with that one. I don't see the harm in having both of them in Mathlib.
There was a problem hiding this comment.
I've played a little bit to see if iIndepFun.pi could be used instead of iIndepFun.prod in the proof of the independence lemma of X_1, X_2, X'_1 + X'_2 in endgame.lean, and indeed the proof is smoother because you don't have to fight against the system. I've made the change in the PR, but I can revert it if you prefer. In light of this, I'd say that iIndepFun.pi is more suitable for mathlib than iIndepFun.prod.
There was a problem hiding this comment.
Looks good and I have merged. I like how your approach has the "kappa" function built in while I had to work somewhat tediously to obtain the counterpart of that function in my own approach. Another example, by the way, of how Lean favors a conceptual architecture for mathematics that differs in some subtle ways from what human mathematicians intuitively work with. But perhaps I would still advocate for putting iIndepFun.prod in Mathlib but with a docstring warning that iIndepFun.pi is recommended instead? Mostly because I think that mathematicians new to Lean might go looking for such a method and not understand why it isn't there.
On a related note: how feasible do you think it would be to incorporate iIndepFun.pi and various other independence lemmas into an `independence' tactic that can try to deduce either pairwise or joint independence of various combinations of functions (and I guess also eventually sets and sigma algebras, if we want to really make this tactic useful) from such existing hypotheses ? Dealing with independence was a surprisingly time consuming portion of the entire project.
There was a problem hiding this comment.
I'm not sure there is something deep to be gained here with the use of the kappa function to build a sigma type: it's more about the inner workings of Lean related to dependent type theory which makes some proofs smooth, and some proofs less smooth -- in general, one should avoid subtypes whenever possible, because the system is not very efficient with them. By the way, using a sigma type like I did is not my idea, it's @YaelDillies who translated the not very idiomatic iIndepFun.prod to the more idiomatic iIndepFun.pi. Even though he did not check whether it would apply cleanly, it's one of those things where you learn by practice the designs that work best.
For your question about an independence tactic, that's a very good question. I have never done any serious metaprogramming myself, so I can't answer this one. In general anything is possible, but the first thing is to have a good model of what we want to do. After a few projects using serious probability theory, maybe some pattern will emerge where we will see what we really need. But for now it's probably a little early for that, we need more data points.
There was a problem hiding this comment.
Independence is one of the things paper mathematicians have the most intuition about. Eg in the Ajtai-Komlos-Szemerédi bound on Ramsey numbers, there is this depth-first search in a binomial random graph. The proof notices that the sequence of edges visited is itself a Bernoulli sequence because, well, every edge we visited was an independent coin toss. But you're tossing different coins depending on the previous tosses! I have no idea how to even start proving this kind of statements.
No description provided.