stuck on a proof on probability expectations

Stream: new members

[Becker A.]

Hi all! I've spent ~a week or two trying to write a proof using expectations and I've hit my patience limit, so I'd appreciate some help.

I have a proof (see code at the end) that if you write a sum of real numbers as the sum of all but the last one plus the last one, then taking that sum to some power can be expanded using the binomial theorem:

$$\left(\sum_{i = 1}^{n} X_{i}\right)^{k} = \left(X_{n} + \sum_{i = 1}^{n - 1} X_{i}\right)^{k} = \sum_{l = 0}^{k} {k \choose l} X_{n}^{k - l} \left(\sum_{i = 1}^{n - 1} X_{i}\right)^{l}$$

now I want to assume the Xi are independent random variables and apply an expectation to that:

$$E \left[\left(\sum_{i = 1}^{n} X_{i}\right)^{k}\right] = \sum_{l = 0}^{k} {k \choose l} E \left[X_{n}^{k - l}\right] \cdot E \left[\left(\sum_{i = 1}^{n - 1} X_{i}\right)^{l}\right]$$

I've gotten as far as expanding the first set of equations out within the expectation, but I'm getting hung up on applying mutual independence to the remaining expression in order to split the expression into multiple expectations.

My code so far:

-- import Mathlib

import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Defs
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.Probability.Independence.Basic
import Mathlib.Probability.Moments.Basic
import Mathlib.MeasureTheory.Function.L1Space.Integrable

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Fin

open Finset BigOperators
open MeasureTheory ProbabilityTheory NNReal
open scoped ENNReal


-- working proof of the first set of equations w/o expectations
theorem pow_sum_castSucc_eq_sum_add_pow
  {R : Type u_1} [CommSemiring R]
  {n : ℕ}
  {f : Fin (n.succ) → R}
  {k : ℕ}
  : (∑ i : Fin n.succ, f i) ^ k
    = ∑ j : Fin k.succ, (∑ i : Fin n, f i.castSucc) ^ j.toNat
    * (f (Fin.last n)) ^ (k - j) * k.choose j
  := by
  rw [Fin.sum_univ_castSucc, add_pow, Finset.sum_range, Nat.succ_eq_add_one]
  rfl

def ifun_drop_last
  {R : Type u_1}
  {n : ℕ}
  (f : (Fin n.succ) → R)
  : (Fin n) → R
  := by
  intro j
  apply f
  apply Fin.castLT j
  apply lt_trans (Fin.is_lt j) (n |> Fin.last |> Fin.is_lt)


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


-- working proof of expanding the first equations in the expectation
theorem k_moment_sum_expand
  {Ω : Type u_1} [m : MeasurableSpace Ω]
  {μ : Measure Ω} [IsProbabilityMeasure μ]
  {n : ℕ}
  (X : Fin n.succ → Ω → ℝ)
  (k : ℕ)
  : moment (isum_rv X) k μ
   = μ[∑ ki : Fin k.succ, (X |> ifun_drop_last |> isum_rv) ^ ki.toNat
    * (n |> Fin.last |> X) ^ (k - ki) * k.choose ki]
  := by
    unfold moment ifun_drop_last isum_rv
    simp only [Nat.succ_eq_add_one, Pi.pow_apply, Fin.toNat_eq_val,
      Finset.sum_apply, Pi.mul_apply, Pi.natCast_apply]
    rewrite [<- MeasureTheory.setIntegral_univ]
    nth_rewrite 2 [<- MeasureTheory.setIntegral_univ]
    apply setIntegral_congr_fun
    · exact MeasurableSet.univ
    rw [Set.eqOn_univ, funext_iff]
    intro ω
    rw [pow_sum_castSucc_eq_sum_add_pow]
    rfl


-- unfinished proof of the desired final expression
theorem k_moment_sum_recursive
  {Ω : Type u_1} [m : MeasurableSpace Ω]
  {μ : Measure Ω} [IsProbabilityMeasure μ]
  {n : ℕ}
  (X : Fin n.succ → Ω → ℝ)
  (k : ℕ)
  -- do I need v-this?
  -- (hXIntegrable : Integrable ((isum_rv X) ^ k) μ)
  (hXIndep : iIndepFun X μ)
  : moment (isum_rv X) k μ
    = ∑ ki : Fin k.succ, moment (X |> ifun_drop_last |> isum_rv) ki.toNat μ
      * moment (n |> Fin.last |> X) (k - ki) μ * (k.choose ki).cast
  := by
    rw [k_moment_sum_expand]
    simp only [Nat.succ_eq_add_one, Fin.toNat_eq_val, Finset.sum_apply,
      Pi.mul_apply, Pi.pow_apply, Pi.natCast_apply]
    rw [integral_finset_sum]
    case hf =>
      intro i _
      rw [integrable_mul_const_iff]
      case hc =>
        rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero, <- ne_eq]
        apply Nat.choose_ne_zero
        rw [@Nat.le_iff_lt_add_one]
        exact i.is_lt
      sorry
    sorry

Any help is appreciated, thanks!

[Etienne Marion]

Here is my version (needs some polishing):

import Mathlib

open Finset MeasureTheory ProbabilityTheory


variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P]
    {n k : ℕ} {X : Fin (n + 1) → Ω → ℝ}

theorem MemLp.integrable_pow {f : Ω → ℝ} (h : MemLp f k P) : Integrable (fun x => f x ^ k) P := by
  obtain rfl | hk := eq_or_ne k 0
  · simp
  rw [← integrable_norm_iff]
  · simpa [← memLp_one_iff_integrable] using h.norm_rpow (by norm_cast) (by simp)
  exact h.aestronglyMeasurable.pow k

example (hX : ∀ i, MemLp (X i) k P) (h : iIndepFun X P) :
    ∫ ω, (∑ i, X i ω) ^ k ∂P =
    ∑ l ∈ range (k + 1), (k.choose l) * (∫ ω, (X (Fin.last n) ω) ^ (k - l) ∂P) * (∫ ω, (∑ i : Fin n, X i.castSucc ω) ^ l ∂P) := by
  have key (l : ℕ) : (fun ω => X (Fin.last n) ω ^ (k - l)) ⟂ᵢ[P] fun ω => (∑ i : Fin n, X i.castSucc ω) ^ l := by
    apply IndepFun.comp
    · symm
      have : (fun ω ↦ ∑ i : Fin n, X i.castSucc ω) = ∑ i ∈ Iio (Fin.last n), X i := by ext; simp
      rw [this]
      apply h.indepFun_finset_sum_of_notMem₀
      · exact fun i ↦ (hX i).aemeasurable
      · simp
    · exact measurable_id.pow_const (k - l)
    · exact measurable_id.pow_const l
  simp_rw [Fin.sum_univ_castSucc, add_pow]
  rw [integral_finset_sum]
  · congr with l
    rw [mul_assoc, ← IndepFun.integral_mul_eq_mul_integral, ← integral_const_mul]
    · congr with ω
      simp only [Pi.mul_apply]
      ring
    · exact key l
    · exact (hX _).aestronglyMeasurable.pow (k - l)
    · convert (aestronglyMeasurable_sum (Finset.univ) (fun (i : Fin n) _ ↦ (hX i.castSucc).aestronglyMeasurable)).pow l
      simp
  · intro l hl
    apply Integrable.mul_const
    apply IndepFun.integrable_mul
    · exact (key l).symm
    · apply MemLp.integrable_pow
      apply memLp_finset_sum
      intro i _
      apply (hX i.castSucc).mono_exponent
      simp_all only [mem_range, mem_univ, Nat.cast_le]
      omega
    · apply MemLp.integrable_pow
      apply (hX _).mono_exponent
      simp_all

[Becker A.]

cool thanks! idk how long that actually took you to write but it was definitely under 2 hours. How do I learn to do proofs that fast? T-T

[Ruben Van de Velde]

Mostly by doing :)

[Becker A.]

how much doing, I've probably put in a couple months at this point and it's all still pretty slow and painful. any suggestions for making the doing easier?

[Artie Khovanov]

When I would run across something that was annoying to prove, I would try to do something to make it less annoying to prove in the future, such as abstracting an argument out into a lemma, adding automation, changing definitions, etc.

I don't know if this works for you, but focusing on making code "clean" really helped me ask the right questions to myself and others.

[Artie Khovanov]

But yeah formalising, as with any skill, takes many hours of work to learn.

[Matt Diamond]

@Becker A. It might help to be specific about aspects of the completed proof that eluded you. Was there a lemma that you looked for but didn't know how to find? Or was the problem that you weren't even sure what to look for?

[Etienne Marion]

Indeed the biggest part comes from practice, with some help from the documentation and #loogle. I don't know how much time you spent over those two months, but the learning curve is known to be quite steep unfortunately. Apart from practice, the other thing that helped me a lot was getting code reviews from more experienced members. I think this is important to really get more efficient (the other way would be to skim through the existing code), you learn a lot about tactics, some shortcuts, conventions about how lemmas are stated etc.

[Becker A.]

probably a mix of things:

• I don't know all the tactics yet, so I have fewer things to work with - e.g., I'm pretty comfortable with rw, exact, simp, aesop and apply, but that's mostly it. on brief inspection the proof above uses congr, symm, and omega, none of which I've heard of.
• here I was struggling with showing Integrable for the quantities in question. this I think might have been more a limit of my mathematical understanding of Integrable for generic types (I've taken an undergraduate Real Analysis course, but not sure what exactly Integrable asserts in relation to that). So I think that made it hard for me to know how to prove that.
• having studied probability in an applied math setting I've never had to represent probabilities as mappings from a "measurable" set. I'm guessing it just means that you're kind of defining random variables as their inverse c.d.f., i.e. the mapping from the interval (0, 1) (which is the "measurable" set?) to the real number line. except that the "measurable set" is generalized to be anything, as long as it satisfies the same intuitive properties that (0, 1) does (whatever those are). so I'm also a little lost in that representation.
• a lot of my time is spent searching https://leansearch.net for something I need, eventually finding the perfect thing, trying to apply it with rw or apply, and then having the compiler tell me "rw is trying to apply something of form X, but can't find anything that matches in X". ...as in it says it can't find X in the expression X, like visually the thing it's trying to match looks exactly like my expression and I don't understand why they're different. I don't have exact examples but this happens often.

[Becker A.]

Etienne Marion said:

the other thing that helped me a lot was getting code reviews from more experienced members. I think this is important to really get more efficient (the other way would be to skim through the existing code), you learn a lot about tactics, some shortcuts, conventions about how lemmas are stated etc.

thanks for the suggestion! how do you get those code reviews? do you just post code in new-members and ask for feedback?

[Etienne Marion]

Yes!

[Artie Khovanov]

Yeah unfortunately everybody is very busy and it can be difficult to get eyes on your code. If you are at university, there may be a Lean club around, or at least other students or faculty who know Lean?

[Becker A.]

faculty (in the applied math department), afaict, don't use lean / interactive theorem provers because it's too much effort and not worth it. I haven't talked to other departments though; maybe comp sci or pure math do?

[Yan Yablonovskiy 🇺🇦]

Becker A. said:

faculty (in the applied math department), afaict, don't use lean / interactive theorem provers because it's too much effort and not worth it. I haven't talked to other departments though; maybe comp sci or pure math do?

Depends how big your math school is and where it is , my uni also has no one. The bigger / higher rank math unis are more likely to , but it’s new.

You can try share lean and inspire some people to join you on your journey maybe, that’s what I am trying to do

[Vlad Tsyrklevich]

Becker A. said:

• a lot of my time is spent searching https://leansearch.net for something I need

Natural text search is useful when you know the English name of a theorem or definition but don't know how it might be stated in Lean. If you are in the middle of a proof and know the lean types of what are you dealing with, e.g. I have a MeasurableSpace and I'm looking for an instance of X or a theorem that connects it to Y, I'd recommend using loogle instead (search MeasureableSpace, X or MeasureableSpace,Yin this case but the syntax allows more interesting queries than that as well.) loogle searches by lean types and given that everything is expressed as a type this is much more direct and powerful. When I am proving, I always have loogle in front of me. It is almost as important to me as the infoview.

[Vlad Tsyrklevich]

As for the rest of the statement about the rw/apply not matching: probably the exact types don't match. The next time it happens and you are confused by it, ask on Zulip. I suspect what is happening is that the types appear to be the same but are not in some mild way, e.g. a Nat is an Int or there is some small difference in the types that you can often correct yourself by applying a coercion first or stating a theorem/hypothesis using a slightly different type. Hovering overing an expression in the infoview will give you what type it is and you can manually compare the exact types against what you see in the docs.

[Ruben Van de Velde]

I'm not sure it would have helped in this case, but what I often do is trying to write out every (part of a) sentence of the proof as a have proved by sorry, and then when I've got the structure set up, start knocking out these sorrys one by one (splitting them up again as needed). That way you've got lots of small, hopefully achievable goals - and it's easier to ask with a small, self-contained goal than your whole theorem

[Becker A.]

Ruben Van de Velde said:

I'm not sure it would have helped in this case, but what I often do is trying to write out every (part of a) sentence of the proof as a have proved by sorry, and then when I've got the structure set up, start knocking out these sorrys one by one (splitting them up again as needed). That way you've got lots of small, hopefully achievable goals - and it's easier to ask with a small, self-contained goal than your whole theorem

I kind of tried to do that using calc syntax, which tbh is a little weird, but I imagine makes for a much more readable proof if you do it right...? anyway eventually I just split off the calc'd mini statement into the function k_moment_sum_expand.

from you experience, any preference of calc over have, based on the situation?

[Becker A.]

Vlad Tsyrklevich said:

As for the rest of the statement about the rw/apply not matching: ...The next time it happens and you are confused by it, ask on Zulip.

I will, thanks :slight_smile: I always hesitate to ask because I spend a good chunk of time trying to make a "minimum reproducible example". but spending 20-30 minutes doing that is better than being confused for hours! :upside_down:

[Ruben Van de Velde]

calc is great when it applies, yeah

[Vlad Tsyrklevich]

Becker A. said:

I always hesitate to ask because I spend a good chunk of time trying to make a "minimum reproducible example". but spending 20-30 minutes doing that is better than being confused for hours! :upside_down:

I think MWEs are vital when the question is about help with a question that involves applying logical/mathematical reasoning to help the questioner, otherwise the view can be obscured by everything hanging around. If your question is more about Lean, something like "I think I should be able to apply a lemma here but I cannot" you can just minimize it to the exact place you are stuck using the extract_goal tactic and you're done.