Theorems · Theorem · probability

ProbabilityTheory.IndepFun.hasLaw_add_map_cast_poissonMeasure

∀ {R : Type u_1} [inst : AddMonoidWithOne R] {mR : MeasurableSpace R} {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω} [MeasurableAdd₂ R] {r₁ r₂ : NNReal} {X Y : Ω → R},
  ProbabilityTheory.IndepFun X Y P →
    ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₁)) P →
      ProbabilityTheory.HasLaw Y (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₂)) P →
        ProbabilityTheory.HasLaw (X + Y)
          (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure (r₁ + r₂))) P

The sum of two independent Poisson random variables with rates r₁, r₂ taking values in R is a Poisson random variable with rate r₁ + r₂.

Defined in

Mathlib.Probability.Distributions.Poisson.Basic

Cited by

0 results in Mathlib

Foundations

Depth 289 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidWithOneMeasurableAdd₂