Design feedback: Mean of Poisson Distribution

Stream: new members

[Peter Hansen]

Hi everyone!

After a great experience with my first PR a few days ago (thanks EtienneC30!), I was excited to try contributing a new result and decided to work on the expectation of the Poisson distribution.

Before I get too far, I'd love to get some feedback on the overall design to make sure I'm on the right track. My approach was to prove a core HasSum lemma for the underlying Real-valued function, and then derive the user-facing tsum results from it. Here's what I have:

import Mathlib.Probability.Distributions.Poisson
import Mathlib.Probability.ProbabilityMassFunction.Integrals
open ProbabilityTheory ENNReal
open scoped NNReal ENNReal

theorem poissonPMFReal_Mul_Sum (r : ℝ≥0) : HasSum (fun n ↦ poissonPMFReal r n * n) r.toReal := by
  suffices HasSum _ (poissonPMFReal r 0 * ↑(0 : ℕ) + ↑r * 1) by simpa using this
  have : (fun n ↦ poissonPMFReal r (n + 1) * ↑(n + 1)) = fun n ↦ r * poissonPMFReal r n := by
    simp_rw [poissonPMFReal, div_mul, Nat.factorial_succ, pow_succ]
    field_simp [← mul_rotate']
  exact (this ▸ (poissonPMFRealSum r).mul_left r.toReal).zero_add

theorem poissonPMFReal_Mul_tsum (r : ℝ≥0) : ∑' n, (poissonPMF r n).toReal * n = r.toReal := by
  simp_rw [poissonPMF, DFunLike.coe, toReal_ofReal poissonPMFReal_nonneg]
  exact (poissonPMFReal_Mul_Sum r).tsum_eq

theorem poissonPMF_Mul_tsum (r : ℝ≥0) : ∑' n, ((poissonPMF r n) * (n : ℝ≥0∞)) = r := by
  simp_rw [poissonPMF, DFunLike.coe, ← ofReal_natCast, ← ofReal_mul poissonPMFReal_nonneg]
  have (n : ℕ) : 0 ≤ poissonPMFReal r n * n := mul_nonneg poissonPMFReal_nonneg n.cast_nonneg
  rw [← ofReal_tsum_of_nonneg this (poissonPMFReal_Mul_Sum r).summable,
    (poissonPMFReal_Mul_Sum r).tsum_eq, ofReal_coe_nnreal]

My specific questions are:

1. Structure: Is this split into a core HasSum lemma and derived PMF theorems the idiomatic way to structure proofs like this?
2. API: I noticed PMF.bernoulli_expectation is stated using ∫ n, ... ∂p.toMeasure. Should the main, public-facing theorem for Poisson's expectation also use this integral form, with my theorems above serving as lemmas for its proof?
3. Naming: Are the names I chose reasonable, or is there a better convention I should follow?

Thanks for any guidance!