awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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 : CompleteSpace E
inst_5 : Countable R
inst_6 : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : @Integrable _ _ _ _ inst_2 f Po(R, 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))
have rw : Eq.{u_1 + 1} (α := E) (∫ (x : ℕ), f (↑x : R) ∂Po(r))
  (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
Tactic: rw [integral_map .of_discrete .of_discrete]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (hypothesis)
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 : CompleteSpace E
inst_5 : Countable R
inst_6 : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : @Integrable _ _ _ _ inst_2 f Po(R, r)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℕ), f (↑x : R) ∂Po(r))
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
have hf₁ : Integrable (f ∘ Nat.cast) Po(r)
Tactic: rw [integrable_map_cast_poissonMeasure_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ Eq.{u_1 + 1} (α := E) (∫ (n : ℕ), f n ∂Po(r)) (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n)
have rw : 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: rw [poissonMeasure, integral_sum_dirac (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ Eq.{u_1 + 1} (α := E) (∑' (i : ℕ), (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal • f i)
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n)
have e_f : ∀ (n : ℕ),
  (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n =
    (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n
Tactic: congr with n
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n =
    (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n
have e_f : (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n = (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n
Tactic: rw [ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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
⊢ 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))
have rw : Eq.{u_1 + 1} (α := E) (∫ (x : ℕ), f (↑x : R) ∂Po(r))
  (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
Tactic: rw [integral_map .of_discrete .of_discrete, integral_poissonMeasure]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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))
⊢ 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))
have rw₁ : Eq.{u_1 + 1} (α := E) (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
  (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))
Tactic: rw [integral_map .of_discrete .of_discrete, integral_poissonMeasure]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
⊢ charFun (mE := Real.measurableSpace) Po(ℝ, r) t = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
have rw : ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑(inner ℝ (↑n : ℝ) t) : ℂ) * I) =
  cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
Tactic: rw [charFun_apply, integral_map .of_discrete (by fun_prop), integral_poissonMeasure r]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
⊢ ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑(inner ℝ (↑n : ℝ) t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
have simp_rw : ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑((↑n : ℝ) * t) : ℂ) * I) =
  cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
Tactic: simp_rw [Real.inner_apply]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
⊢ Eq (α := ℂ) (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I))
    (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ)))
have e_f : ∀ (a : ℕ),
  (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
a : ℕ
⊢ (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))
have e_f : cexp (-(↑(↑r : ℝ) : ℂ)) * (↑(↑r : ℝ) : ℂ) ^ a / (↑a ! : ℂ) * cexp ((↑a : ℂ) * (↑t : ℂ) * I) =
  cexp (-(↑(↑r : ℝ) : ℂ)) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
a : ℕ
⊢ cexp (-(↑(↑r : ℝ) : ℂ)) * (↑(↑r : ℝ) : ℂ) ^ a / (↑a ! : ℂ) * cexp ((↑a : ℂ) * (↑t : ℂ) * I) =
    cexp (-(↑(↑r : ℝ) : ℂ)) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ))
have e_f : cexp (-(↑(↑r : ℝ) : ℂ)) * (↑(↑r : ℝ) : ℂ) ^ a / (↑a ! : ℂ) * cexp ((↑a : ℂ) * (↑t : ℂ) * I) =
  cexp (-(↑(↑r : ℝ) : ℂ)) * ((↑(↑r : ℝ) : ℂ) ^ a * cexp ((↑a : ℂ) * ((↑t : ℂ) * I)) / (↑a ! : ℂ))
Tactic: rw [mul_pow, ← Complex.exp_nat_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
⊢ (↑(rexp (-(↑r : ℝ))) : ℂ) * ∑' (a : ℕ), ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))
have rw : (↑(rexp (-(↑r : ℝ))) : ℂ) * NormedSpace.exp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) =
  (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))
Tactic: rw [(NormedSpace.expSeries_div_hasSum_exp (r * cexp (t * I))).tsum_eq, exp_eq_exp_ℂ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
rw :
  (↑(rexp (-(↑r : ℝ))) : ℂ) * NormedSpace.exp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))
⊢ (↑(rexp (-(↑r : ℝ))) : ℂ) * ∑' (a : ℕ), ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ) =
    (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))
have rw₁ : (↑(rexp (-(↑r : ℝ))) : ℂ) * NormedSpace.exp ((↑(↑r : ℝ) : ℂ) * NormedSpace.exp ((↑t : ℂ) * I)) =
  (↑(rexp (-(↑r : ℝ))) : ℂ) * NormedSpace.exp ((↑(↑r : ℝ) : ℂ) * NormedSpace.exp ((↑t : ℂ) * I))
Tactic: rw [(NormedSpace.expSeries_div_hasSum_exp (r * cexp (t * I))).tsum_eq, exp_eq_exp_ℂ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
⊢ (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
have rw : cexp ((↑(-(↑r : ℝ)) : ℂ) + (↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
Tactic: rw [ofReal_exp, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
⊢ cexp ((↑(-(↑r : ℝ)) : ℂ) + (↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
have push_cast : cexp (-(↑(↑r : ℝ) : ℂ) + (↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) = cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
t : ℝ
⊢ ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑((↑n : ℝ) * t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
have calc : Eq (α := ℂ) (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ a / (↑a ! : ℝ)) : ℂ) * cexp ((↑((↑a : ℝ) * t) : ℂ) * I))
  (∑' (a : ℕ), (↑(rexp (-(↑r : ℝ))) : ℂ) * (((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ)))
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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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 ! : ℂ)))
⊢ ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑((↑n : ℝ) * t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
have calc₁ : (↑(rexp (-(↑r : ℝ))) : ℂ) * ∑' (a : ℕ), ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I)) ^ a / (↑a ! : ℂ) =
  (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑t : ℂ) * I))
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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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))
⊢ ∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • cexp ((↑((↑n : ℝ) * t) : ℂ) * I) =
    cexp ((↑(↑r : ℝ) : ℂ) * (cexp ((↑t : ℂ) * I) - 1))
have calc₂ : (↑(rexp (-(↑r : ℝ))) : ℂ) * cexp ((↑(↑r : ℝ) : ℂ) * cexp ((↑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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r₁ r₂ : ℝ≥0
⊢ Eq (α := Measure ℝ) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) Po(ℝ, r₁ + r₂)
have h : Eq (α := (t : ℝ) → ℂ) (charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)))
  (charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂))
Tactic: apply Measure.ext_of_charFun
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r₁ r₂ : ℝ≥0
⊢ Eq (α := (t : ℝ) → ℂ) (charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)))
    (charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂))
have h : ∀ (t : ℝ), charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) t = charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r₁ r₂ : ℝ≥0
t : ℝ
⊢ charFun (mE := measurableSpace) (Po(ℝ, r₁) ∗ Po(ℝ, r₂)) t = charFun (mE := measurableSpace) Po(ℝ, r₁ + r₂) t
have 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))
Tactic: simp only [charFun_conv, charFun_map_cast_poissonMeasure, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r₁ r₂ : ℝ≥0
t : ℝ
⊢ 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))
have h : (↑(↑r₁ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) +
    (↑(↑r₂ : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1) =
  (↑(↑(r₁ + r₂) : ℝ) : ℂ) * (Complex.exp ((↑t : ℂ) * Complex.I) - 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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)
have h : (↑(↑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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r₁ r₂ : ℝ≥0
⊢ Po(r₁) ∗ Po(r₂) = Po(r₁ + r₂)
have a : Eq (α := Measure ℝ) (Measure.map Nat.cast (Po(r₁) ∗ Po(r₂))) Po(ℝ, r₁ + r₂)
Tactic: apply (MeasurableEmbedding.natCast (α := ℝ)).map_injective
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r₁ r₂ : ℝ≥0
⊢ Measurable (α := ℕ) (β := ℝ) (⇑(Nat.castAddMonoidHom ℝ) : (a : ℕ) → ℝ)
have funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r₁ r₂ : ℝ≥0
⊢ Eq (α := Measure ℝ) (Measure.map Nat.cast (Po(r₁) ∗ Po(r₂))) Po(ℝ, r₁ + r₂)
have 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₂))
Tactic: rw [← Nat.coe_castAddMonoidHom, Measure.map_conv_addMonoidHom _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
mR : MeasurableSpace R
inst_1 : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
⊢ Measurable (α := ℕ) (β := R) (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R)
have funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
mR : MeasurableSpace R
inst_1 : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
⊢ Eq.{u_1 + 1} (α := Measure R) (Po(R, r₁) ∗ Po(R, r₂)) Po(R, r₁ + r₂)
have 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₂))
Tactic: rw [← Nat.coe_castAddMonoidHom, ← Measure.map_conv_addMonoidHom _ (by fun_prop),
    poissonMeasure_conv_poissonMeasure]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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₂))
⊢ Eq.{u_1 + 1} (α := Measure R) (Po(R, r₁) ∗ Po(R, r₂)) Po(R, r₁ + r₂)
have 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₂))
Tactic: rw [← Nat.coe_castAddMonoidHom, ← Measure.map_conv_addMonoidHom _ (by fun_prop),
    poissonMeasure_conv_poissonMeasure]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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₂))
⊢ Eq.{u_1 + 1} (α := Measure R) (Po(R, r₁) ∗ Po(R, r₂)) Po(R, r₁ + r₂)
have rw₂ : Eq (α := Measure R) (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₁ + r₂))
  (Measure.map (⇑(Nat.castAddMonoidHom R) : (a : ℕ) → R) Po(r₁ + r₂))
Tactic: rw [← Nat.coe_castAddMonoidHom, ← Measure.map_conv_addMonoidHom _ (by fun_prop),
    poissonMeasure_conv_poissonMeasure]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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₁ + r₂) P
have rw : HasLaw (X + Y) (Po(r₁) ∗ Po(r₂)) P
Tactic: rw [← poissonMeasure_conv_poissonMeasure]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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₁ + r₂) P
have rw : HasLaw (m𝓧 := mR) (X + Y) (Po(R, r₁) ∗ Po(R, r₂)) P
Tactic: rw [← map_cast_poissonMeasure_conv]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
⊢ PMF ℕ
have refine : HasSum (α := ENNReal) (fun (n : ℕ) ↦ ENNReal.ofReal (poissonPMFReal r n)) 1
Tactic: refine ⟨fun n ↦ ENNReal.ofReal (poissonPMFReal r n), ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
⊢ HasSum (α := ENNReal) (fun (n : ℕ) ↦ ENNReal.ofReal (poissonPMFReal r n)) 1
have apply : HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) 1
Tactic: apply ENNReal.hasSum_coe.mpr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
⊢ HasSum (α := ℝ≥0) (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) 1
have rw : HasSum (fun (a : ℕ) ↦ (poissonPMFReal r a).toNNReal) (toNNReal 1)
Tactic: rw [← toNNReal_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
⊢ Measurable (poissonPMFReal r)
have funProp : Nat.instMeasurableSpace ≤ Nat.instMeasurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ (fun (n : ℕ) ↦ (↑n : ℝ) * p n * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) =ᶠ[atTop] p
have h : ∀ (n : ℕ) (hn : 1 ≤ n), (↑n : ℝ) * p n * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = p n
Tactic: filter_upwards [eventually_ge_atTop 1] with n hn
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (hypothesis)
Goal:
p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ Tendsto p atTop (𝓝 0)
have this : (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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k / (↑k.factorial : ℝ) * p n ^ k) fun (n : ℕ) ↦
    ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)
have h : ∀ (x : ℕ), HPow.hPow (α := ℝ) (↑x : ℝ) k / (↑k.factorial : ℝ) * p x ^ k = ((↑x : ℝ) * p x) ^ k / (↑k.factorial : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (hypothesis)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k) atTop (𝓝 (r ^ k / (↑k.factorial : ℝ)))
have this : 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))
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
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 : ℝ)))
have refine : Tendsto (fun (n : ℕ) ↦ ((↑n : ℝ) * p n) ^ k / (↑k.factorial : ℝ)) atTop (𝓝 (r ^ k / (↑k.factorial : ℝ)))
Tactic: refine (IsEquivalent.tendsto_nhds_iff this).mpr ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k * (1 - p n) ^ (n - k)) atTop
    (𝓝 (Real.exp (-r) * r ^ k / (↑k.factorial : ℝ)))
have rw : Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k * (1 - p n) ^ (n - k)) atTop
  (𝓝 (r ^ k / (↑k.factorial : ℝ) * Real.exp (-r)))
Tactic: rw [mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.PoissonLimitThm (goal)
Goal:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * p n) atTop (𝓝 r)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(n.choose k) : ℝ) * p n ^ k * (1 - p n) ^ (n - k)) atTop
    (𝓝 (r ^ k / (↑k.factorial : ℝ) * Real.exp (-r)))
have refine : Tendsto (fun (n : ℕ) ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))
Tactic: refine (tendsto_choose_mul_pow_atTop k hr).mul ?_