stuck on proof for iIndepFun on subset of indices

Stream: new members

[Becker A.]

any help here? existing proof steps is just as far as I've gotten, feel free to rewrite.

the problem - I want to prove that if you have a family of independent random variables iIndepFun X P, then the subset of random variables with the last one excluded is also itself a family of independent random variables iIndepFun (fun i : Fin n => X i.castSucc) P

things I've tried - I've demo'd it below. basically I tried to unfold the definition of iIndepFun in both the input parameter iIndepFun X P and the goal iIndepFun (fun i : Fin n => X i.castSucc) P, and am trying to map the goal to the input via apply.

see code below:

import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.Probability.Independence.Basic

open Finset MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal

lemma iIndepFun_succ
    {Ω : Type u_1} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P]
    {n : ℕ}
    {X : Fin (n + 1) → Ω → ℝ}
    (hXIndep : iIndepFun X P)
    : iIndepFun (fun i : Fin n => X i.castSucc) P
  := by
  unfold iIndepFun Kernel.iIndepFun Kernel.iIndep Kernel.iIndepSets Kernel.const
  unfold iIndepFun Kernel.iIndepFun Kernel.iIndep Kernel.iIndepSets Kernel.const at hXIndep
  simp_all only [Set.mem_setOf_eq, Kernel.coe_mk, ae_dirac_eq, Filter.eventually_pure]
  intro s f hsf

  have hf : ∃ (f' : Fin (n + 1) → Set Ω), ∀ (j : Fin n), f j = f' j.castSucc := by
    exists (
        fun i => if h : i ≠ Fin.last n then f (Fin.castPred i (by rewrite [ne_eq]; exact h))
        else ⊥
      )
    simp only [ne_eq, Fin.castSucc_ne_last, not_false_eq_true, ↓reduceDIte, Fin.castPred_castSucc,
      implies_true]

  have hs1 : ∀ i ∈ s, i.castSucc ∈ (Finset.map Fin.castSuccEmb s) := by
    simp only [mem_map, Fin.coe_castSuccEmb, Fin.castSucc_inj, exists_eq_right, imp_self,
      implies_true]
  have hs2 : ∀ i ∈ (Finset.map Fin.castSuccEmb s), ∃ j ∈ s, j.castSucc = i := by
    simp only [mem_map, Fin.coe_castSuccEmb, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro i hi
    exists i

  -- apply hXIndep
  sorry

why it doesn't work - w/ the apply I get this error:

_:38:2
Tactic `apply` failed: could not unify the conclusion of `hXIndep`
  P (Set.iInter fun (i : Fin (n + 1)) ↦ ⋂ (_ : i ∈ ?s), ?f i) = ∏ x ∈ ?s, P (?f x)
with the goal
  P (Set.iInter fun (i : Fin n) ↦ ⋂ (_ : i ∈ s), f i) = ∏ x ∈ s, P (f x)

Note: The full type of `hXIndep` is
  ∀ (s : Finset (Fin (n + 1))) {f : Fin (n + 1) → Set Ω},
    (∀ i ∈ s, MeasurableSet (f i)) → P (⋂ i ∈ s, f i) = ∏ x ∈ s, P (f x)

-> seems like the input uses Fin (n + 1) whereas the goal uses Fin n.

Not sure how to fix / rewrite from scratch. Please advise, thanks!

[Vlad Tsyrklevich]

1. This does not compile, make it an #mwe
2. Use your words. What is the problem? What have you tried? Why doesn't it work?

[Becker A.]

1. forgot the imports, my bad. just edited to include them

[Becker A.]

2a. please be kind.
2b. just wrote out more details, lmk if you need any other information

[David Ledvinka]

It seems like you just tried to unravel the (very complicated) definition. Rarely in paper math or lean do you prove random variables are independent "by definition". You should think about how you would prove it on paper first. I gave a solution in spoilers but I encourage you to try it yourself before looking.

import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.Probability.Independence.Basic

open Finset MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal

#check iIndepFun.precomp

lemma iIndepFun_succ
    {Ω : Type u_1} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P]
    {n : ℕ}
    {X : Fin (n + 1) → Ω → ℝ}
    (hXIndep : iIndepFun X P)
    : iIndepFun (fun i : Fin n => X i.castSucc) P := by
  exact iIndepFun.precomp (f := X) (Fin.castSucc_injective n) hXIndep

[Becker A.]

yeahhhh I kind of thought that through the definition I could just do some Fin.castSucc's and convert one to the other

[Becker A.]

what I really wanted was an existing theorem that said something like ∀ i ≠ j, IndepFun (X i) (X j) P P ↔ iIndepFun X P. because then I could use IndepFun on every pair to directly show that for every pair on the subset, and then convert that result back to iIndepFun for the subset

[Etienne Marion]

This is not true.

[Becker A.]

oh? I thought iIndepFun was a way to express a bunch of random variables Xi, where all Xi/Xj are independent for i ≠ j.

[Becker A.]

can you describe to me what/how I'm misunderstanding?

[David Ledvinka]

A classic counter example is:

Let X,Y be independent ℤ mod 2 random variables with probability 1/2 being 0 or 1. Define Z = X + Y. Then any pair of random variables in {X,Y,Z} are independent but they are not mutually independent since if I know any two then I know the third.

[Becker A.]

ohhhhh so it's more that you have that any individual Xi is independent of the whole collection of the others?

[Becker A.]

(kinda sounds like ProbabilityTheory.iIndepFun.indepFun_sub_right)

[Becker A.]

(or maybe that any partition of RV's are mutually independent?)

[David Ledvinka]

What sounds like that, are you saying for your originally problem?

[Becker A.]

David Ledvinka said:

A classic counter example is:

Let X,Y be independent ℤ mod 2 random variables with probability 1/2 being 0 or 1. Define Z = X + Y. Then any pair of random variables in {X,Y,Z} are independent but they are not mutually independent since if I know any two then I know the third.

^this

Becker A. said:

(kinda sounds like ProbabilityTheory.iIndepFun.indepFun_sub_right)

sounds like it requires something more powerful like ^this

[Becker A.]

sorry if that wasn't clear

[David Ledvinka]

Well those random variables are not iIndepFun, they are only pairwise independent.

[Becker A.]

understood. I think I'm not articulating my thought process well anymore so I might just drop this particular thought thread. but that's an interesting counter-example that I didn't consider, thanks for sharing!

[Becker A.]

also I wouldn't have considered using precomp because tbh I don't really understand what it's asserting. I would love a short description if you have the energy for it, if not then at least thanks for providing it!

[David Ledvinka]

This is how I came to the solution. Your problem amounts to something like saying if $X_1, ... X_{n+1}$ are mutually independent then $X_1, ..., X_{n}$ are mutually independent. But in lean we represent these as functions from Fin n to the random variables Ω → ℝ . All you are doing is restricting/reindexing. You should think if I drop random variables that shouldn't change independence and if I "rename" the random variables that shouldn't change independence.

What is reindexing formally? (Pre)composing with a bijection on the domain, and restricting would be precomposing with an injection. I actually looked for comp first, thinking it might be called that, saw that was something else, and then looked for the lemma I actually wanted.

[Becker A.]

firstly, thank you! I love a good journey through somebody’s thought-process :sparkling_heart:

Second, I think I understand most if this but not everything; specifically:

• random variables as functions from Fin n to Omega to R - yep, knew this
• just dropping one RV, and the property still holds - yep
• injection - need to re-look up the definition every time to not confuse with surjection, but yep
• precomposing - i.e. applying a function to the indices then applying f after - sure got it
• restricting would be precomposing with an injection - not sure I understand this fully

[Snir Broshi]

Becker A. said:

• restricting would be precomposing with an injection - not sure I understand this fully

Your original code contains fun i : Fin n => X i.castSucc, which is equal to X ∘ Fin.castSucc, aka precomposing X with Fin.castSucc, and Fin.castSucc is injective (docs#Fin.castSucc_injective)

[Becker A.]

...hm. okay. for some reason I was thinking it'd have to go the other way, where you start with i : Fin (n + 1) and somehow find an injection of the form Fin (n + 1) -> Fin n, which shouldn't be possible, hence confusion. that makes more sense. thanks!