prob and stats e.g. in Lean4 - linearity of expectation

Stream: new members

[Becker A.]

I'm trying to learn how to express probability and stats concepts in Lean4, using guides like this one.

For a conceptually easy example on paper, I'm trying to express the linearity of expectation for a finite array of independent random variables. Specifically:

$$E\left[\sum_{i = 1}^n X_i\right] = \sum_{i = 1}^n E[X_i]$$

where the X_i are independent.

so far I have this:

import Mathlib
open MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal

noncomputable def moment_of_sum
  {R : Type u_1} [NormedAddCommGroup R] [NormedSpace ℝ R] [CommSemiring R] -- [MeasurableSpace R]
  {Ω : Type u_2} [MeasurableSpace Ω]
  (P : Measure Ω)
  {n : ℕ}
  (X : (Fin n) → Ω → R)
  -- (hX : (i : Fin n) → Measurable (X i))
  (k : ℕ)
  : R := P[fun (ω : Ω) => (∑ i : Fin n, X i ω) ^ k]


example
  {Ω : Type u_1} [m : MeasurableSpace Ω]
  {P : Measure Ω} [IsProbabilityMeasure P]
  {P2 : Measure ℝ}
  {μ : ℝ}
  {σ : ℝ≥0}
  {X : Fin 3 → Ω → ℝ}
  (hX : (i : Fin 3) → Measurable (X i))
  (h_indep : iIndep X P) -- this doesn't compile
  : (moment_of_sum P X 1 = ∑ i : Fin 3, moment (X i) 1 P)
  := by
  sorry

...but I'm struggling to express the iIndep expression (atm it doesn't compile). I also don't know if this is the conventional method for formalizing this kind of proof.

general questions:

• how do I use iIndep?
• am I on the right track?
• I looked for an existing theorem and saw MeasureTheory.condExpL1_add but didn't see how it would apply here (without maybe a dummy conditional parameter). is there an existing mathlib proof for this specifically?
• any tips I might not know about that would help me approach stuff like this moving forwards?

[Snir Broshi]

Becker A. said:

I'm trying to learn how to express probability and stats concepts in Lean4, using guides like this one.

IIUC the blog you referenced states you should use docs#ProbabilityTheory.iIndepFun, not docs#ProbabilityTheory.iIndep:

For a family X : ι → Ω → ℝ of independent random variables, use iIndepFun. To express independence of sets, use IndepSet (two sets) and iIndepSet (family of sets). For sigma-algebras, Indep and iIndep.

[Snir Broshi]

I don't understand where you're going with this, but here's the cleaned up code:

import Mathlib
open MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal

example {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {n : ℕ} {X : Fin n → Ω → ℝ} (h_indep : iIndepFun X P) :
    moment (fun ω ↦ ∑ i, X i ω) 1 P = ∑ i, moment (X i) 1 P := by
  sorry

[Becker A.]

...so it was just a typo T-T
thanks!

[Becker A.]

okay I'm still looking to construct a lean4 proof for the below equation:

$$E\left[\sum_{i = 1}^n X_i\right] = \sum_{i = 1}^n E[X_i]$$

and I now have this:

import Mathlib

-- https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/
open MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal


-- https://leanprover-community.githb.io/blog/posts/basic-probability-in-mathlib/#:~:text=Measure%20%CE%A9.-,Identically%20distributed,-IdentDistrib%20X%20Y
-- https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/#:~:text=of%20the%20indicator).-,Independence,-Mathlib%20has%20several

noncomputable def sum_random_vars
  {R : Type u_1} [NormedAddCommGroup R] [NormedSpace ℝ R] [CommSemiring R] -- [MeasurableSpace R]
  {Ω : Type u_2} [MeasurableSpace Ω]
  {n : ℕ}
  (X : (Fin n) → Ω → R)
  -- (hX : (i : Fin n) → Measurable (X i))
  : (Ω → R) := fun (ω : Ω) => (∑' i : Fin n, X i ω)

example
  {Ω : Type u_1} [m : MeasurableSpace Ω]
  {P : Measure Ω} [IsProbabilityMeasure P]
  {n : ℕ}
  {X : Fin n → Ω → ℝ}
  (hX : (i : Fin n) → Measurable (X i))
  : (moment (sum_random_vars X) 1 P = ∑' i : Fin n, moment (X i) 1 P)
  := by
  unfold sum_random_vars
  unfold moment
  simp only [pow_one, Pi.pow_apply]
  rw [integral_tsum_of_summable_integral_norm]
  -- rw [integral_tsum]

  sorry

with tactic state:

2 goals
case hF_int
Ω : Type u_1
m : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
n : ℕ
X : Fin n → Ω → ℝ
hX : ∀ (i : Fin n), Measurable (X i)
⊢ ∀ (i : Fin n), Integrable (X i) P
case hF_sum
Ω : Type u_1
m : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
n : ℕ
X : Fin n → Ω → ℝ
hX : ∀ (i : Fin n), Measurable (X i)
⊢ Summable fun i ↦ ∫ (a : Ω), ‖X i a‖ ∂P

• am I on the right track?
• any tips for closing this? e.g.:

1. are there ways to show Summable or Integrable? or would convention just have me include those as function parameters?
2. any notable difference between integral_tsum and integral_tsum_of_summable_integral_norm in this context?

[David Ledvinka]

Firstly, instead of using tsum (topological sum) you can just use regular sum (∑ instead of ∑'). This allows you to use the lemma integral_finset_sum. Secondly you need to assume the functions are integrable, otherwise it won't necessarily be true.

[Becker A.]

yeah I used ∑' so that I could apply integral_tsum_of_summable_integral_norm, which operates on ∑' specifically, not ∑. is there another function that's equivalent to integral_tsum_... but for ∑?

[David Ledvinka]

Sorry I edited my message to include it right after I posted. Its integral_finset_sum. Note tsum is for possibly infinite sum, this is why you get the extra Summabilitygoal that requires you to show the sum converges.

[Rémy Degenne]

Note that you don't need independence for linearity of the expectation.

[Becker A.]

David Ledvinka said:

tsum is for possibly infinite sum, this is why you get the extra Summabilitygoal that requires you to show the sum converges.

okay. so in other words, tsum is specifically for sums that are finite (basing this also on docs), which is why I need to provide a proof that this sum is finite. do I have that right?

[Becker A.]

Rémy Degenne said:

Note that you don't need independence for linearity of the expectation.

thanks, yeah I removed that from my second code chunk. but also I'm trying to eventually do something more complicated that does require independence, which is why I got confused and added that in by mistake. so that original question/answer will not go to waste!

[David Ledvinka]

No, tsum is for possibly infinite sums that unconditionally converge. They can converge to infinity if they are for example in the type ENNReal (the extended non-negative Reals which is [0,∞])

[Becker A.]

okay. so would I edit my first statement to instead be this?:

tsum is specifically for sums that converge, which is why I need to provide a proof that this sum converges.

[Becker A.]

ohhhhhh so it's to exclude things like the alternating series [1, -1, 1, -1, ...]

[David Ledvinka]

Essentially, but there is some subtlety here that is a bit hard to explain. For reasons that are explained in other zulip threads and textbooks (I think somewhere in Mathematics in Lean?) it is mostly convenient when formalising in type theory to assign junk values to functions/operations when they dont make sense and have theorems make up for this by requiring the necessary assumptions rather than having the operations not be defined for those bad cases. So tsum works on any sequence but will assign a value of 0 when the sum doesn't converge.

[Becker A.]

David Ledvinka said:

Essentially, but there is some subtlety here that is a bit hard to explain. ...

yep! I've seen that for e.g. for differentiability.

so then basically for that particular theorem: even though it's also defined for non-converging summations via the junk 0 value, it's still only logically correct when they do converge in summation (hence why it requires the convergence proof)?

or like, the version w/o the junk value assumes convergence in summation inherently (which this statement needs), but the junk value one needs the extra proof because adding the junk value relaxed the statement conditions s.t. it removed that necessary proof?

[Becker A.]

anyway I think this answers my question, thanks all! feel free to mark this topic as resolved