awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
e_f :
  ∀ (n : ℕ),
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n =
      (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n
⊢ Eq.{u_1 + 1} (α := E) (∑' (i : ℕ), (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal • f i)
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n)

Tactic:
congr with n
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ 0 ≤ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
n : ℕ
e_f e_f₁ : (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n = (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n
⊢ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n =
    (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n

Tactic:
rw [ENNReal.toReal_ofReal (by positivity)]

Premises used: ENNReal.toReal_ofReal
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
R : Type u_2
inst_1 : NatCast R
inst_2 : MeasurableSpace R
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
r : ℝ≥0
inst_5 : Countable R
inst_6 : MeasurableSingletonClass R
f : R → E
rw :
  Eq.{u_1 + 1} (α := E) (∫ (x : ℕ), f (↑x : R) ∂Po(r))
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := E) (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ inst_2 Po(R, r) fun (x : R) ↦ f x)
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))

Tactic:
rw [integral_map .of_discrete .of_discrete, integral_poissonMeasure]

Premises used: MeasureTheory.integral_map, MeasureTheory.AEStronglyMeasurable.of_discrete, ProbabilityTheory.integral_poissonMeasure, AEMeasurable.of_discrete
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ cexp ((↑(inner ℝ x t) : ℂ) * I)) Po(ℝ, r)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
rw :
  ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑(inner ℝ (↑n : ℝ) t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
⊢ charFun (mE := Real.measurableSpace) Po(ℝ, r) t = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))

Tactic:
rw [charFun_apply, integral_map .of_discrete (by fun_prop), integral_poissonMeasure r]

Premises used: MeasureTheory.charFun_apply, MeasureTheory.integral_map, ProbabilityTheory.integral_poissonMeasure, AEMeasurable.of_discrete
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
simp_rw :
  ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑((↑n : ℝ) * t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
⊢ ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑(inner ℝ (↑n : ℝ) t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))

Tactic:
simp_rw [Real.inner_apply]

Premises used: Real.inner_apply
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
e_f :
  ∀ (a : ℕ),
    (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I) =
      (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))
⊢ Eq (α := ℂ) (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I))
    (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ)))

Tactic:
congr with a
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
a : ℕ
e_f :
  cexp (-(↑(↑r : ℝ) : ℂ)) * (↑(↑r : ℝ) : ℂ) ^ a / (↑a ! : ℂ) * cexp ((↑a : ℂ) * (↑t : ℂ) * I) =
    cexp (-(↑(↑r : ℝ) : ℂ)) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))
⊢ (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))

Tactic:
push_cast
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
a : ℕ
e_f :
  cexp (-(↑(↑r : ℝ) : ℂ)) * (↑(↑r : ℝ) : ℂ) ^ a / (↑a ! : ℂ) * cexp ((↑a : ℂ) * (↑t : ℂ) * I) =
    cexp (-(↑(↑r : ℝ) : ℂ)) * ((↑(↑r : ℝ) : ℂ) ^ a * cexp ((↑a : ℂ) * ((↑t : ℂ) * I)) / (↑a ! : ℂ))
⊢ cexp (-(↑(↑r : ℝ) : ℂ)) * (↑(↑r : ℝ) : ℂ) ^ a / (↑a ! : ℂ) * cexp ((↑a : ℂ) * (↑t : ℂ) * I) =
    cexp (-(↑(↑r : ℝ) : ℂ)) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))

Tactic:
rw [mul_pow, ← Complex.exp_nat_mul]

Premises used: Complex.exp_nat_mul, mul_pow
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
a : ℕ
⊢ cexp (-(↑(↑r : ℝ) : ℂ)) * (↑(↑r : ℝ) : ℂ) ^ a / (↑a ! : ℂ) * cexp ((↑a : ℂ) * (↑t : ℂ) * I) =
    cexp (-(↑(↑r : ℝ) : ℂ)) * ((↑(↑r : ℝ) : ℂ) ^ a * cexp ((↑a : ℂ) * ((↑t : ℂ) * I)) / (↑a ! : ℂ))

Tactic:
ring_nf
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
⊢ ∑' (a : ℕ), (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ)) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * ∑' (a : ℕ), ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ)

Tactic:
tsum_mul_left

Premises used: tsum_mul_left
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
rw :
  (↑(rexp (-(↑r : ℝ))) : ℂ) * NormedSpace.exp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))
rw₁ rw₂ :
  (↑(rexp (-(↑r : ℝ))) : ℂ) * NormedSpace.exp ((↑(↑r : ℝ) : ℂ) * NormedSpace.exp ((↑t : ℂ) * I)) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * NormedSpace.exp ((↑(↑r : ℝ) : ℂ) * NormedSpace.exp ((↑t : ℂ) * I))
⊢ (↑(rexp (-(↑r : ℝ))) : ℂ) * ∑' (a : ℕ), ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))

Tactic:
rw [(NormedSpace.expSeries_div_hasSum_exp (r * cexp (t * I))).tsum_eq, exp_eq_exp_ℂ]

Premises used: HMul.hMul, Complex.exp_eq_exp_ℂ, Complex.ofReal, HasSum.tsum_eq, Complex.exp, NormedSpace.expSeries_div_hasSum_exp, NNReal.toReal, Complex.I
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
rw :
  cexp ((↑(-(↑r : ℝ)) : ℂ) + (↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
⊢ (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))

Tactic:
rw [ofReal_exp, ← Complex.exp_add]

Premises used: Complex.exp_add, Complex.ofReal_exp
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
push_cast :
  cexp (-(↑(↑r : ℝ) : ℂ) + (↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
⊢ cexp ((↑(-(↑r : ℝ)) : ℂ) + (↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))

Tactic:
push_cast
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
⊢ cexp (-(↑(↑r : ℝ) : ℂ) + (↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))

Tactic:
ring_nf
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
t : ℝ
calc :
  Eq (α := ℂ) (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I))
    (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ)))
calc₁ :
  (↑(rexp (-(↑r : ℝ))) : ℂ) * ∑' (a : ℕ), ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))
calc₂ :
  (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
⊢ ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑((↑n : ℝ) * t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))

Tactic:
calc ∑' a, (rexp (-r) * r ^ a / a ! : ℝ) * cexp ((a * t : ℝ) * I)
  _ = ∑' a, (rexp (-r)) * ((r * cexp (t * I)) ^ a / a !) := by
      congr with a
      push_cast
      rw [mul_pow, ← Complex.exp_nat_mul]
      ring_nf
  _ = (rexp (-r)) * ∑' a, ((r * cexp (t * I)) ^ a / a !) := tsum_mul_left
  _ = (rexp (-r)) * cexp (r * cexp (t * I)) := by
      rw [(NormedSpace.expSeries_div_hasSum_exp (r * cexp (t * I))).tsum_eq, exp_eq_exp_ℂ]
  _ = cexp (r * (cexp (t * I) - 1)) := by
      rw [ofReal_exp, ← Complex.exp_add]
      push_cast
      ring_nf

Premises used: HMul.hMul, HSub.hSub, tsum_mul_left, Real.exp, Complex.ofReal, Complex.exp, OfNat.ofNat, NNReal.toReal, Neg.neg, Complex.I
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
h :
  Eq (α := (t : ℝ) → ℂ) (charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)))
    (charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂))
⊢ Eq (α := Measure ℝ) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) Po(ℝ, r₁ + r₂)

Tactic:
apply Measure.ext_of_charFun

Premises used: MeasureTheory.Measure.ext_of_charFun
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
h :
  ∀ (t : ℝ),
    charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) t = charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂) t
⊢ Eq (α := (t : ℝ) → ℂ) (charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)))
    (charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂))

Tactic:
ext t
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
t : ℝ
h :
  Complex.exp
      ((↑(↑r₁ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) +
        (↑(↑r₂ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1)) =
    Complex.exp ((↑(↑(r₁ + r₂) : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1))
⊢ charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) t = charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂) t

Tactic:
simp only [charFun_conv, charFun_map_cast_poissonMeasure, ← Complex.exp_add]

Premises used: Complex.exp_add, MeasureTheory.charFun_conv, ProbabilityTheory.charFun_map_cast_poissonMeasure
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
t : ℝ
h :
  (↑(↑r₁ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) +
      (↑(↑r₂ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) =
    (↑(↑(r₁ + r₂) : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1)
⊢ Complex.exp
      ((↑(↑r₁ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) +
        (↑(↑r₂ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1)) =
    Complex.exp ((↑(↑(r₁ + r₂) : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1))

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
t : ℝ
h :
  (↑(↑r₁ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) +
      (↑(↑r₂ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) =
    ((↑(↑r₁ : ℝ) : ℂ) + (↑(↑r₂ : ℝ) : ℂ)) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1)
⊢ (↑(↑r₁ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) +
      (↑(↑r₂ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) =
    (↑(↑(r₁ + r₂) : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1)

Tactic:
push_cast
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
t : ℝ
⊢ (↑(↑r₁ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) +
      (↑(↑r₂ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) =
    ((↑(↑r₁ : ℝ) : ℂ) + (↑(↑r₂ : ℝ) : ℂ)) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1)

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
a : Eq (α := Measure ℝ) (Measure.map Nat.cast (Po(r₁) ∗ Po(r₂))) Po(ℝ, r₁ + r₂)
⊢ Po(r₁) ∗ Po(r₂) = Po(r₁ + r₂)

Tactic:
apply (MeasurableEmbedding.natCast (α := ℝ)).map_injective

Premises used: MeasurableEmbedding.map_injective, MeasurableEmbedding.natCast
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
⊢ Measurable (α := ℕ) (β := ℝ) (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
a :
  Eq (α := Measure ℝ)
    (Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₁) ∗
      Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₂))
    (Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₁ + r₂))
⊢ Eq (α := Measure ℝ) (Measure.map Nat.cast (Po(r₁) ∗ Po(r₂))) Po(ℝ, r₁ + r₂)

Tactic:
rw [← Nat.coe_castAddMonoidHom, Measure.map_conv_addMonoidHom _ (by fun_prop)]

Premises used: MeasureTheory.Measure.map_conv_addMonoidHom, Nat.coe_castAddMonoidHom
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
⊢ Eq (α := Measure ℝ)
    (Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₁) ∗
      Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₂))
    (Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₁ + r₂))

Tactic:
map_cast_poissonMeasure_conv_real _ _

Premises used: _private.0.ProbabilityTheory.map_cast_poissonMeasure_conv_real
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r₁ r₂ : ℝ≥0
⊢ Eq (α := Measure ℝ)
    (Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₁) ∗
      Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₂))
    (Measure.map (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ) Po(r₁ + r₂))

Tactic:
exact map_cast_poissonMeasure_conv_real _ _

Premises used: _private.0.ProbabilityTheory.map_cast_poissonMeasure_conv_real
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
mR : MeasurableSpace R
inst_1 : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
⊢ Measurable (α := ℕ) (β := R) (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
mR : MeasurableSpace R
inst_1 : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
rw :
  Eq (α := Measure R)
    (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₁) ∗
      Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₂))
    (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₁ + r₂))
rw₁ :
  Eq (α := Measure R) (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) (Po(r₁) ∗ Po(r₂)))
    (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₁ + r₂))
rw₂ rw₃ :
  Eq (α := Measure R) (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₁ + r₂))
    (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₁ + r₂))
⊢ Eq.{u_1 + 1} (α := Measure R) (Po(R, r₁) ∗ Po(R, r₂)) Po(R, r₁ + r₂)

Tactic:
rw [← Nat.coe_castAddMonoidHom, ← Measure.map_conv_addMonoidHom _ (by fun_prop),
    poissonMeasure_conv_poissonMeasure]

Premises used: MeasureTheory.Measure.map_conv_addMonoidHom, Nat.coe_castAddMonoidHom, ProbabilityTheory.poissonMeasure_conv_poissonMeasure
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
r₁ r₂ : ℝ≥0
X Y : Ω → ℕ
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(r₁) P
hY : HasLaw Y Po(r₂) P
rw : HasLaw (X + Y) (Po(r₁) ∗ Po(r₂)) P
⊢ HasLaw (X + Y) Po(r₁ + r₂) P

Tactic:
rw [← poissonMeasure_conv_poissonMeasure]

Premises used: ProbabilityTheory.poissonMeasure_conv_poissonMeasure
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
r₁ r₂ : ℝ≥0
X Y : Ω → ℕ
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(r₁) P
hY : HasLaw Y Po(r₂) P
⊢ HasLaw (X + Y) (Po(r₁) ∗ Po(r₂)) P

Tactic:
hXY.hasLaw_add hX hY

Premises used: ProbabilityTheory.IndepFun.hasLaw_add
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
r₁ r₂ : ℝ≥0
X Y : Ω → ℕ
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(r₁) P
hY : HasLaw Y Po(r₂) P
⊢ HasLaw (X + Y) (Po(r₁) ∗ Po(r₂)) P

Tactic:
exact hXY.hasLaw_add hX hY

Premises used: ProbabilityTheory.IndepFun.hasLaw_add
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
mR : MeasurableSpace R
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst_1 : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
X Y : Ω → R
hXY : X ⟂ᵢ[P] Y
hX : HasLaw (m𝓧 := mR) X Po(R, r₁) P
hY : HasLaw (m𝓧 := mR) Y Po(R, r₂) P
rw : HasLaw (m𝓧 := mR) (X + Y) (Po(R, r₁) ∗ Po(R, r₂)) P
⊢ HasLaw (m𝓧 := mR) (X + Y) Po(R, r₁ + r₂) P

Tactic:
rw [← map_cast_poissonMeasure_conv]

Premises used: ProbabilityTheory.map_cast_poissonMeasure_conv
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
mR : MeasurableSpace R
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst_1 : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
X Y : Ω → R
hXY : X ⟂ᵢ[P] Y
hX : HasLaw (m𝓧 := mR) X Po(R, r₁) P
hY : HasLaw (m𝓧 := mR) Y Po(R, r₂) P
⊢ HasLaw (m𝓧 := mR) (X + Y) (Po(R, r₁) ∗ Po(R, r₂)) P

Tactic:
hXY.hasLaw_add hX hY

Premises used: ProbabilityTheory.IndepFun.hasLaw_add
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
R : Type u_1
inst : AddMonoidWithOne R
mR : MeasurableSpace R
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst_1 : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
X Y : Ω → R
hXY : X ⟂ᵢ[P] Y
hX : HasLaw (m𝓧 := mR) X Po(R, r₁) P
hY : HasLaw (m𝓧 := mR) Y Po(R, r₂) P
⊢ HasLaw (m𝓧 := mR) (X + Y) (Po(R, r₁) ∗ Po(R, r₂)) P

Tactic:
exact hXY.hasLaw_add hX hY

Premises used: ProbabilityTheory.IndepFun.hasLaw_add
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
refine : HasSum (α := ENNReal) (fun (n : ℕ) ↦ ENNReal.ofReal (poissonPMFReal r n)) 1
⊢ PMF ℕ

Tactic:
refine ⟨fun n ↦ ENNReal.ofReal (poissonPMFReal r n), ?_⟩
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
apply : HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) 1
⊢ HasSum (α := ENNReal) (fun (n : ℕ) ↦ ENNReal.ofReal (poissonPMFReal r n)) 1

Tactic:
apply ENNReal.hasSum_coe.mpr

Premises used: Iff.mpr, ENNReal.hasSum_coe
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
rw : HasSum (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) (toNNReal 1)
⊢ HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) 1

Tactic:
rw [← toNNReal_one]

Premises used: Real.toNNReal_one
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
⊢ HasSum (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) (toNNReal 1)

Tactic:
(poissonPMFRealSum r).toNNReal (fun n ↦ poissonPMFReal_nonneg)

Premises used: HasSum.toNNReal, ProbabilityTheory.poissonPMFRealSum, ProbabilityTheory.poissonPMFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
⊢ HasSum (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) (toNNReal 1)

Tactic:
exact (poissonPMFRealSum r).toNNReal (fun n ↦ poissonPMFReal_nonneg)

Premises used: HasSum.toNNReal, ProbabilityTheory.poissonPMFRealSum, ProbabilityTheory.poissonPMFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal (poissonPMFReal r n) =
    (Subtype.mk (p := fun (f : ℕ → ENNReal) ↦ HasSum f 1) (fun (n : ℕ) ↦ ENNReal.ofReal (poissonPMFReal r n)) ⋯ :
        (a : ℕ) → ENNReal)
      n

Tactic:
rfl
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
⊢ Measurable (poissonPMFReal r)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
⊢ StronglyMeasurable (poissonPMFReal r)

Tactic:
stronglyMeasurable_iff_measurable.mpr (measurable_poissonPMFReal r)

Premises used: Iff.mpr, ProbabilityTheory.measurable_poissonPMFReal, stronglyMeasurable_iff_measurable
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
h : ∀ (n : ℕ) (hn : 1 ≤ n), (↑n : ℝ) * p n * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = p n
⊢ (fun (n : ℕ) ↦ (↑n : ℝ) * p n * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =ᶠ[atTop] p

Tactic:
filter_upwards [eventually_ge_atTop 1] with n hn

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
n : ℕ
hn : 1 ≤ n
⊢ (↑n : ℝ) * p n * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = p n

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ (fun (n : ℕ) ↦ (↑n : ℝ) * p n * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =ᶠ[atTop] p

Tactic:
have : (fun n => (n * p n) * (1 / n)) =ᶠ[atTop] p := by
    filter_upwards [eventually_ge_atTop 1] with n hn
    field
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
this : (fun (n : ℕ) ↦ (↑n : ℝ) * p n * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =ᶠ[atTop] p
⊢ Tendsto p atTop (𝓝 0)

Tactic:
simpa using (hr.mul tendsto_one_div_atTop_nhds_zero_nat).congr' this

Premises used: Filter.Tendsto.mul, tendsto_one_div_atTop_nhds_zero_nat, Filter.Tendsto.congr'
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
h : ∀ (x : ℕ), HPow.hPow (α := ℝ) (↑x : ℝ) k / (↑k.factorial : ℝ) * p x ^ k = ((↑x : ℝ) * p x) ^ k / (↑k.factorial : ℝ)
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k.factorial : ℝ) * p n ^ k) fun (n : ℕ) ↦
    ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
x : ℕ
⊢ HPow.hPow (α := ℝ) (↑x : ℝ) k / (↑k.factorial : ℝ) * p x ^ k = ((↑x : ℝ) * p x) ^ k / (↑k.factorial : ℝ)

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k) fun (n : ℕ) ↦
    ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)

Tactic:
have : (fun n => n.choose k * (p n) ^ k) ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
    calc
    _ ~[atTop] (fun n => (n ^ k / k.factorial) * (p n) ^ k) :=
      (isEquivalent_choose k).mul IsEquivalent.refl
    _ ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
      EventuallyEq.isEquivalent (.of_eq (by ext; field))
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
this :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k) fun (n : ℕ) ↦
    ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k) atTop (𝓝 (r ^ k / (↑k.factorial : ℝ)))

Tactic:
(IsEquivalent.tendsto_nhds_iff this).mpr ?_

Premises used: Iff.mpr, Asymptotics.IsEquivalent.tendsto_nhds_iff
-- Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
this :
  IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k) fun (n : ℕ) ↦
    ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)
refine : Tendsto (fun (n : ℕ) ↦ ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)) atTop (𝓝 (r ^ k / (↑k.factorial : ℝ)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k) atTop (𝓝 (r ^ k / (↑k.factorial : ℝ)))

Tactic:
refine (IsEquivalent.tendsto_nhds_iff this).mpr ?_

Premises used: Iff.mpr, Asymptotics.IsEquivalent.tendsto_nhds_iff