Independence of A, B, C implies independence of A, B+C

Stream: Polynomial Freiman-Ruzsa conjecture

[Jonas Bayer]

For proving pfr#sum_dist_diff_le I need to show that I can deduce

iIndepFun (fun x ↦ hG) ![X₁, X₂, X₁' + X₂']

from iIndepFun (fun x ↦ hG) ![X₁, X₂, X₁', X₂']. Is there already a lemma which can do this? I've not found one so I started trying to state the result, but I find it hard to come up with an idiomatic way to do this.

[Rémy Degenne]

docs#ProbabilityTheory.IndepFun.comp should be what you are looking for.

[Rémy Degenne]

Oh sorry no, you ask about iIndepFun

[Floris van Doorn]

https://teorth.github.io/pfr/docs/PFR/ForMathlib/Independence.html#ProbabilityTheory.iIndepFun.comp and https://teorth.github.io/pfr/docs/PFR/ForMathlib/Independence.html#ProbabilityTheory.iIndepFun.reindex are very close, but won't get you quite there, I think. The proofs should transfer though.

[Floris van Doorn]

You probably want to prove a iIndepFun.prod that pairs up two variables, and then you can use comp to add them.

[Terence Tao]

Hmm. Is it essential that you need joint independence of all three variables? Pairwise independence can be obtained from existing tools such as docs#ProbabilityTheory.iIndepFun.indepFun_prod or pfr#ProbabilityTheory.iIndepFun.indepFun_prod_prod , but right now there aren't so many tools to establish joint independence. Ideally, we should have a variant of docs#ProbabilityTheory.iIndepFun.indepFun_finset that allows for more than two disjoint sets (and then one can use pfr#ProbabilityTheory.iIndepFun.comp to conclude). If joint independence is really what you need, one option is to write up such a variant and add it back to the task list, and establish what you need from that variant; it could be a useful addition to the independence portion of MathLib.

[Jonas Bayer]

I'm not sure how to best do this without getting type theory problems. I started by writing a function that changes the value of f i to (f i, f j), but of course, that also changes the type of f. So I wrote a function that calculates what the new type should be as follows:

/-- Change α' such that α' i becomes α' i × α' j  -/
def pairIndicesOfSpaces [DecidableEq ι] (α' : ι → Type u) (i j : ι) : ι → Type u :=
  fun k => if k ≠ i then α' k else (α' i × α' j)

/-- Change f such that f i becomes (f i × f j) -/
def pairIndices [DecidableEq ι] (f : (i : ι) → Ω → α i) (i j : ι) :
  (k : ι) → Ω → (pairIndicesOfSpaces α i j) k :=
  fun k => if k ≠ i then f k else (f i, f j)

But this doesn't type check and I'm not convinced it can be made to work. What would be the right setup for defining iIndepFun.prod as @Floris van Doorn proposes?

The correct function would of course also have to delete the index j but I think this should be the easier part.

[Jonas Bayer]

Joint independence is necessary for using pfr#condDist_diff_ofsum_le @Terence Tao. Unless one can change the hypotheses of that lemma to pairwise independence I don't see a way around the issue.

[Jonas Bayer]

And yes, having docs#ProbabilityTheory.iIndepFun.indepFun_finset for multiple disjoint sets would help. I'll try to state this now.

[Terence Tao]

Jonas Bayer said:

And yes, having docs#ProbabilityTheory.iIndepFun.indepFun_finset for multiple disjoint sets would help. I'll try to state this now.

By the way, there is a hacky alternate way to proceed, which is to establish a lemma that if (A, B) is independent of C and A is independent of B, then A, B, C are jointly independent; this is not too difficult from pfr#ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map' and pfr#ProbabilityTheory.iIndepFun_iff_map_prod_eq_prod_map_map and would allow one to leverage the pairwise independence lemmas to get back to joint independence. But I think having a ProbabilityTheory.iIndepFun.iIndepFun_finset lemma for Mathlib is the better long-term solution, even if it would be a bit more work (hopefully someone will volunteer to fill it in though).

[Jonas Bayer]

That's a good point. I'll remember the hack but try to do it in the more general way for now.

[Jonas Bayer]

When stating iIndepFun.iIndepFun_finset one gets the same problem that I had above. Initially, one has a function f such that the f i are jointly independent and the values of f i are in α i for $i \in I$. One then chooses disjoint sets T_j where $j \in J$ and wants to consider $f' (j) := \prod_{i \in T_j} f(T_j)$ where the product is to be understood as forming a tuple. However, it is not clear to me how the type of f' could be written in Lean.

A solution would be to consider the case where all the α i are the same type β. Then the type of f' j could simply be List β. This would be sufficient for the lemma that I need to prove, but still wouldn't solve the problem in general.

[Floris van Doorn]

One way to write the general lemma is this:

variable {S : ι' → Finset ι} (hS : Pairwise (Disjoint on S)) in
lemma iIndepFun.prod' (h : iIndepFun n f μ) :
    let β := fun k ↦ Π i : S k, α i
    iIndepFun (β := β) (fun k ↦ MeasurableSpace.pi)
      (fun (k : ι') (x : Ω) (i : S k) ↦ f i x) μ := by
  sorry

(this compiles in the Independence file)

[Floris van Doorn]

It will still take a bit of work to instantiate this general version to your application.

[Jonas Bayer]

Thanks a lot for writing this lemma! I tried to instantiate it but it is already difficult to satisfy the MeasurableSpace condition. The way you wrote the lemma it becomes necessary to proveMeasurableSpace ((a : { x // x ∈ S k }) → α ↑a) for any k : ι'. But I only have that the α i are measurable spaces, can one even prove the necessary hypothesis from this? What is the right way to think about the type (a : { x // x ∈ S k }) → α ↑a?

[Johan Commelin]

Seems like the product of the measurable spaces $\alpha_i$ over all $i$ in the finite set $S_k$.

[Johan Commelin]

And I certainly think that we should have much better notation for that. Because I agree that in its current form it is quite hard to parse.

[Jonas Bayer]

Thanks, this is very helpful!