independent random variables

Stream: Is there code for X?

[Vincent Beffara]

Do we have somewhere that the expectation of the product of two independent random variables is the product of their expectations?

I am trying to prove this but am running in circles trying to manage putting different sigma-fields and measurable_space structures on the same underlying type (but with the same measure ...). So far I am able to write something that at least type-checks,

def measurable' {α β : Type*} (F : set (set α)) [measurable_space β] (f : α → β) : Prop :=
∀ ⦃t : set β⦄, measurable_set t → f ⁻¹' t ∈ F

lemma indep_fun_of_indep_sets {F1 F2 : set (set Ω)} (hindep : indep_sets F1 F2)
  {X Y : Ω → ℝ} {hX : measurable' F1 X} {hY : measurable' F2 Y} : indep_fun X Y
| _ _ ⟨_,hA,rfl⟩ ⟨_,hB,rfl⟩ := hindep _ _ (hX hA) (hY hB)

lemma integral_mul_of_indep_sets {F1 F2 : set (set Ω)} (hindep : indep_sets F1 F2) {X Y : Ω → ℝ}
  {hXm : measurable' F1 X} {hXi : integrable X}
  {hYm : measurable' F2 Y} {hYi : integrable Y} :
integral volume (X * Y) = integral volume X * integral volume Y := sorry

but it feels like I am doing it wrong. I also tried starting like

lemma integral_indep {X Y : Ω → ℝ} {hX : integrable X} {hY : integrable Y} {hXY : integrable (X * Y)}
    {h : indep_fun X Y} : ∫ ω, (X * Y) ω = (∫ ω, X ω) * (∫ ω, Y ω) :=
begin
  apply integrable.induction (λ X : Ω → ℝ, ∫ ω, (X * Y) ω = (∫ ω, X ω) * (∫ ω, Y ω)); sorry
end

but did not manage to go much further.

[Rémy Degenne]

We have it for the Lebesgue integral: docs#probability_theory.lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun but it is not used by anything right now so there is no guarantee that it is usable. I started proving the same statement for the Bochner integral a month ago but I did not have time to work on Lean recently, so I did not finish that work. I realized that you really want to do induction on functions which are measurable with respect to some sub-sigma-algebras in order to prove this, so I wrote such an induction lemma. I will PR that induction lemma during the week-end.

[Vincent Beffara]

Thanks! I will have a look ...

[Vincent Beffara]

I managed to prove the case of nonnegative variables, using the lintegral version, but it is very sub-optimal (to say the least):

variables {Ω : Type*} [measure_space Ω] [is_probability_measure (volume : measure Ω)]

lemma integral_indep_of_pos {X Y : Ω → ℝ} {hXYind : indep_fun X Y}
  {hXpos : 0 ≤ X} {hXmes : measurable X} {hYpos : 0 ≤ Y} {hYmes : measurable Y}:
  𝔼[X * Y] = 𝔼[X] * 𝔼[Y] :=
begin
  rw integral_eq_lintegral_of_nonneg_ae,
  rw integral_eq_lintegral_of_nonneg_ae,
  rw integral_eq_lintegral_of_nonneg_ae,

  let f : Ω → ennreal := ennreal.of_real ∘ X,
  let g : Ω → ennreal := ennreal.of_real ∘ Y,
  have := @lintegral_mul_eq_lintegral_mul_lintegral_of_indep_fun Ω _ volume f g _ _ _,
  have := congr_arg ennreal.to_real this,
  convert this,
  { funext, simp [f,g], apply ennreal.of_real_mul, apply hXpos },
  { exact ennreal.to_real_mul.symm },
  { exact measurable.ennreal_of_real hXmes },
  { exact measurable.ennreal_of_real hYmes },
  { rintro _ _ ⟨A,hA,rfl⟩ ⟨B,hB,rfl⟩, simp [f,g],
    rw @set.preimage_comp _ _ _ X ennreal.of_real _, set A' := ennreal.of_real ⁻¹' A,
    rw @set.preimage_comp _ _ _ Y ennreal.of_real _, set B' := ennreal.of_real ⁻¹' B,
    apply hXYind,
    { simp,
      apply @measurable_set_preimage _ _ _ _ real.measurable_space,
      { apply measurable.of_comap_le, simp },
      { apply measurable_set_preimage ennreal.measurable_of_real hA } },
    { simp,
      apply @measurable_set_preimage _ _ _ _ real.measurable_space,
      { apply measurable.of_comap_le, simp },
      { apply measurable_set_preimage ennreal.measurable_of_real hB } }, },
  { apply filter.eventually_of_forall, intro ω, apply hYpos },
  { exact hYmes.ae_measurable },
  { apply filter.eventually_of_forall, intro ω, apply hXpos },
  { exact hXmes.ae_measurable },
  { apply filter.eventually_of_forall, intro ω, apply mul_nonneg, apply hXpos, apply hYpos },
  { apply measurable.ae_measurable, exact measurable.mul hXmes hYmes }
end

[Vincent Beffara]

OK so I finally proved E[X*Y] = E[X] * E[Y] by adding some plumbing around the lintegral version, the code is here https://github.com/vbeffara/lean/blob/main/src/probability/indep.lean

@Rémy Degenne I agree that the right way would be to have an induction on functions that are measurable wrt a sub-sigma-algebra, as that will be of more general use, but I needed to scratch that itch :-)

[Rémy Degenne]

That code looks good. You should PR it and add that result to the probability.integration file. If you do, could you generalize your statements to any measure, not only volume? It should change almost nothing to the proofs.

[Vincent Beffara]

Yes, I will see about that. But first I would also like to slightly generalize lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space to work on ae_measurable functions to be able to drop the measurable X assumption (integrable X should be enough).

[Sebastien Gouezel]

I am not sure you have the right statement yet. Instead, it should probably be : if X is a real-valued random variable, Y is vector-valued, and both are integrable and independent, then X • Y is integrable and E (X • Y) = E X • E Y. Or, even better: if B is bilinear continuous and X and Y are independent, then E (B X Y) = B (E X) (E Y)(is that even true? :-)

[Vincent Beffara]

What I want is something like X and Y are independent (with values in arbitrary types) iff for every f and g with values in the reals, E[(f o X) * (g o Y)] = E[f o X] * E[g o Y], from which I believed all the others would follow as needed (but I did not think so much about that). I'm not sure I want to break the symmetry with smul, and I'm not sure either that I want to learn how to use bilinear maps in lean (yet) ;-)

[Vincent Beffara]

But certainly the current version is not at the right level of generality!