Theorems · Theorem · probability

ProbabilityTheory.map_cast_poissonMeasure_conv

∀ {R : Type u_1} [inst : AddMonoidWithOne R] {mR : MeasurableSpace R} [MeasurableAdd₂ R] (r₁ r₂ : NNReal),
  (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₁)).conv
      (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₂)) =
    MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure (r₁ + r₂))

Defined in: Mathlib.Probability.Distributions.Poisson.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddMonoidWithOne MeasurableAdd₂

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
NNRealstatement and proof · cited by 4,310
MeasureTheory.Measure.mapstatement and proof · cited by 858
AddMonoidWithOnestatement and proof · cited by 313
MeasurableAdd₂statement and proof · cited by 155
MeasureTheory.Measure.convstatement and proof · cited by 41
ProbabilityTheory.poissonMeasurestatement and proof · cited by 16
Nat.castAddMonoidHomproof · cited by 16
Measurable.of_discreteproof · cited by 10
MeasureTheory.Measure.map_conv_addMonoidHomproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.IndepFun.hasLaw_add_map_cast_poissonMeasureproof · cited by 0