Laws of finite sums of independent random variables

This file identifies the law of a finite sum of independent random variables with common law μ as the corresponding convolution power of μ.

An independent natural-valued count gives the mixture of these convolution powers. This is the random-sum construction underlying compound Poisson laws; the count may have any law, and zero counts select the empty sum.

theorem ProbabilityTheory.iIndepFun.hasLaw_finset_sum_convolutionPower {Ω : Type u_1} {ι : Type u_2} {α : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [AddCommMonoid α] [MeasurableAdd₂ α] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure α} {X : ι → Ω → α} (hindep : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) μ P) (s : Finset ι) : HasLaw (∑ i ∈ s, X i) (μ.convolutionPower s.card) P

A finite sum of independent random variables with common law μ has law the corresponding convolution power of μ.

theorem ProbabilityTheory.iIndepFun.hasLaw_sum_convolutionPower {Ω : Type u_1} {ι : Type u_2} {α : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [AddCommMonoid α] [MeasurableAdd₂ α] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure α} {X : ι → Ω → α} [Fintype ι] (hindep : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) μ P) : HasLaw (∑ i : ι, X i) (μ.convolutionPower (Fintype.card ι)) P

The sum of a finite independent family with common law μ has law the convolution power indexed by the cardinality of the family.

theorem MeasureTheory.Measure.hasLaw_sum_pi_convolutionPower {α : Type u_1} [MeasurableSpace α] [AddCommMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [IsProbabilityMeasure μ] (n : ℕ) : ProbabilityTheory.HasLaw (fun (x : Fin n → α) => ∑ i : Fin n, x i) (μ.convolutionPower n) (Measure.pi fun (x : Fin n) => μ)

The sum of the coordinates of a finite product law has the corresponding convolution law.

theorem MeasureTheory.Measure.map_sum_pi_eq_convolutionPower {α : Type u_1} [MeasurableSpace α] [AddCommMonoid α] [MeasurableAdd₂ α] {ι : Type u_2} [Fintype ι] (μ : Measure α) [IsProbabilityMeasure μ] : map (fun (x : ι → α) => ∑ i : ι, x i) (Measure.pi fun (x : ι) => μ) = μ.convolutionPower (Fintype.card ι)

Summing the coordinates of a finite product of a probability measure gives its convolution power indexed by the cardinality of the product. This includes the empty product.

theorem MeasureTheory.Measure.map_sum_range_prod_infinitePi {α : Type u_1} [MeasurableSpace α] [AddCommMonoid α] [MeasurableAdd₂ α] (ρ : Measure ℕ) (μ : Measure α) [IsProbabilityMeasure μ] : map (fun (z : ℕ × (ℕ → α)) => ∑ i ∈ Finset.range z.1, z.2 i) (ρ.prod (infinitePi fun (x : ℕ) => μ)) = ρ.bind μ.convolutionPower

Summing an independent sequence up to a separately drawn natural-valued count gives the mixture of convolution powers against the count law. No finiteness assumption on that law or moment assumption on the jumps is required.

theorem ProbabilityTheory.iIndepFun.hasLaw_sum_range_bind {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [AddCommMonoid α] [MeasurableAdd₂ α] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure α} {ρ : MeasureTheory.Measure ℕ} {X : ℕ → Ω → α} {N : Ω → ℕ} (hindep : iIndepFun X P) (hX : ∀ (i : ℕ), HasLaw (X i) μ P) (hN : HasLaw N ρ P) (hNX : IndepFun N (fun (ω : Ω) (i : ℕ) => X i ω) P) : HasLaw (fun (ω : Ω) => ∑ i ∈ Finset.range (N ω), X i ω) (ρ.bind μ.convolutionPower) P

A random prefix sum of iid jumps has the mixture of convolution powers as its law when the count is independent of the entire jump sequence. Almost-everywhere measurability of the jumps suffices.