NormedSpace.exp to rexp

Stream: new members

[Josha Dekker]

I'm trying to prove that the pmf for the Poisson distribution sums to 1 in lean (I'm aware of PMF, but I want to check the summability condition first), but I'm having a bit of a hard time rewriting the HasSum statement: I know that the usual proof is just a matter of multiplying through by rexp r and writing out the exponential series, but in lean I get a NormedSpace.exp instead of rexp; is there a way to convert between these, or should I be using a different result? I couldn't find what I was looking for through Loogle & Moogle! Thanks in advance!

import Mathlib.Analysis.NormedSpace.Exponential

open scoped ENNReal NNReal

open Real Set Filter Topology

namespace ProbabilityTheory

section PoissonPmf

/-- The pmf of the Poisson distribution depending on its rate-/
noncomputable
def poissonPmfReal (r : ℝ) (x : ℕ) : ℝ := (exp (- r) * r ^ x / (Nat.factorial x))

lemma poissonPmfRealSum (r : ℝ) : HasSum (fun x ↦ poissonPmfReal r x) 1 := by
  unfold poissonPmfReal
  have := NormedSpace.expSeries_div_hasSum_exp ℝ r
  have : rexp r = NormedSpace.exp ℝ r := by
    sorry
  sorry

[Eric Wieser]

@loogle Real.exp, NormedSpace.exp

[loogle]

:search: Real.exp_eq_exp_ℝ

[Eric Wieser]

(I was too lazy to type $\mathbb{R}$)

[Josha Dekker]

Thanks! I was using rexp, I should've used Real.exp in the Loogle search turns out!

[Eric Wieser]

They're the same thing :)

[Josha Dekker]

Eric Wieser said:

They're the same thing :)

Yeah, I meant in the Loogle search (or I failed horribly)

[Eric Wieser]

@Joachim Breitner, is there a way to run open Real in loogle before a search?

[Josha Dekker]

my Loogle query was
"Real.exp", "NormedSpace.exp"
instead of
Real.exp, NormedSpace.exp
that was the problem apparently! Thanks!

[Joachim Breitner]

Nope, at least not yet.

[Joachim Breitner]

"Real.exp" will find all lemmas with Real.exp somewhere in the name; Real.exp will find all lemmas that mention that constant in their type.

[Eric Wieser]

Perhaps it's worth a note in the help text along the lines of "Note that scoped notations like n ! or rexp x or \sum x, x^2 are not currently supported"

[Joachim Breitner]

Ah, the open Real would not only affect name resolution!
Right now these give parse errors, right?

[Eric Wieser]

I guess I mean open scoped Real

[Eric Wieser]

@loogle (open scoped Real in rexp), NormedSpace.exp

[loogle]

:search: Real.exp_eq_exp_ℝ

[Eric Wieser]

Expression-scoped open is great!