Parameter measurability for the Poisson distribution

Measurability in the rate lets measurable rate maps produce measurable measure-valued Poisson families and permits packaging such families as kernels.

theorem TauCeti.Probability.measurable_poissonMeasure : Measurable fun (r : NNReal) => ProbabilityTheory.poissonMeasure r

The Poisson family is measurable in its rate.

This permits composition with measurable rate maps and packages the resulting measure-valued family as a kernel.

theorem TauCeti.Probability.measurable_pi_poissonMeasure {ι : Type u_1} [Fintype ι] : Measurable fun (r : ι → NNReal) => MeasureTheory.Measure.pi fun (i : ι) => ProbabilityTheory.poissonMeasure (r i)

A finite product of Poisson laws is measurable jointly in its rate vector.

theorem TauCeti.Probability.measurable_pi_poissonMeasure_mul_toNNReal {ι : Type u_1} [Fintype ι] (p : ι → NNReal) : Measurable fun (x : ℝ) => MeasureTheory.Measure.pi fun (i : ι) => ProbabilityTheory.poissonMeasure (p i * x.toNNReal)

The finite product of Poisson laws with rates p i * Real.toNNReal x is a measurable mixing kernel on the real line.