awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
hf : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))) x} a
hf₁ hf₂ : ∀ (x : ℝ) (hx : x ∈ Ici t), 0 x ≤ r * t ^ r * x ^ (-(r + 1))
⊢ ∀ᵐ (x : ℝ), x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
filter_upwards with x hx using by positivity [lt_of_lt_of_le ht hx]
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
hfm :
  paretoPDFReal t r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici t))] fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1)))
    (Measure.restrict volume (Ici t))

Tactic:
apply (measurable_paretoPDFReal t r).aestronglyMeasurable.congr

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Measurable.aestronglyMeasurable, ProbabilityTheory.measurable_paretoPDFReal
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ paretoPDFReal t r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici t))] fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))

Tactic:
(ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : t ≤ x) ↦ ?_

Premises used: Iff.mpr, Filter.EventuallyEq, MeasureTheory.ae_of_all, MeasureTheory.ae_restrict_iff', measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
hfm : ∀ (x : ℝ) (hx : t ≤ x), paretoPDFReal t r x = (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))) x
⊢ paretoPDFReal t r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici t))] fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))

Tactic:
refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : t ≤ x) ↦ ?_

Premises used: Iff.mpr, MeasureTheory.ae_of_all, MeasureTheory.ae_restrict_iff', measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
x : ℝ
hx : t ≤ x
hfm hfm₁ : paretoPDFReal t r x = r * t ^ r * x ^ (-(r + 1))
hfm₂ : (if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0) = r * t ^ r * x ^ (-(r + 1))
hfm₃ : (if True then r * t ^ r * x ^ (-(r + 1)) else 0) = r * t ^ r * x ^ (-(r + 1))
⊢ paretoPDFReal t r x = (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))) x

Tactic:
simp_rw [paretoPDFReal, eq_true_intro hx, ite_true]

Premises used: eq_true_intro, ProbabilityTheory.paretoPDFReal, ite_true
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
⊢ Eq (α := ℝ≥0∞) ((paretoMeasure t r : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [paretoMeasure, lintegral_paretoPDF_eq_one ht hr]

Premises used: ProbabilityTheory.paretoMeasure, ProbabilityTheory.lintegral_paretoPDF_eq_one
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ IsProbabilityMeasure (paretoMeasure t r)

Tactic:
have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
rw :
  (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ paretoPDFReal t r x
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ paretoPDFReal t r x

Tactic:
rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]

Premises used: ProbabilityTheory.paretoMeasure, ProbabilityTheory.cdf_eq_real, measurableSet_Iic, MeasureTheory.measureReal_def, MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ paretoPDFReal t r x

Tactic:
(integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae, ProbabilityTheory.paretoPDF, Eq.symm
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
refine_1 : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Iic x))] paretoPDFReal t r
refine_2 :
  AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (paretoPDFReal t r) (Measure.restrict volume (Iic x))
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ paretoPDFReal t r x

Tactic:
refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Eq.symm
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
x_1 : ℝ
⊢ 0 x_1 ≤ paretoPDFReal t r x_1

Tactic:
simp only [Pi.zero_apply, paretoPDFReal_nonneg ht.le hr.le]

Premises used: Pi.zero_apply, LT.lt.le, ProbabilityTheory.paretoPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Iic x))] paretoPDFReal t r

Tactic:
exact ae_of_all _ fun _ ↦ by simp only [Pi.zero_apply, paretoPDFReal_nonneg ht.le hr.le]

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (paretoPDFReal t r) (Measure.restrict volume (Iic x))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Pareto
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
rw : (paretoMeasure t r).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
rw₁ :
  Measure.real (m := measurableSpace) (Measure.withDensity volume (paretoPDF t r)) (Iic x) =
    (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
rw₂ :
  ENNReal.toReal ((Measure.withDensity volume (paretoPDF t r) : (a : Set ℝ) → ℝ≥0∞) (Iic x)) =
    (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
rw₃ rw₄ : (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal

Tactic:
rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]

Premises used: ProbabilityTheory.paretoMeasure, ProbabilityTheory.cdf_eq_real, measurableSet_Iic, MeasureTheory.measureReal_def, MeasureTheory.withDensity_apply
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
n : ℕ
rw :
  (Measure.sum fun (n : ℕ) ↦
          HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)))
            (Measure.dirac n) :
        (a : Set ℕ) → ENNReal)
      {n} =
    ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))
rw₁ rw₂ :
  ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) =
    ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))
⊢ (Po(r) : (a : Set ℕ) → ENNReal) {n} = ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))

Tactic:
rw [poissonMeasure, Measure.sum_smul_dirac_singleton]

Premises used: ProbabilityTheory.poissonMeasure, MeasureTheory.Measure.sum_smul_dirac_singleton
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
n : ℕ
⊢ 0 ≤ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
n : ℕ
rw : ENNReal.toReal ((Po(r) : (a : Set ℕ) → ENNReal) {n}) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
rw₁ :
  (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
rw₂ rw₃ : rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
⊢ Po(r).real {n} = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)

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

Premises used: ENNReal.toReal_ofReal, ProbabilityTheory.poissonMeasure_singleton, MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
n : ℕ
hr : 0 < r
rw : 0 < rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
⊢ 0 < Po(r).real {n}

Tactic:
rw [poissonMeasure_real_singleton]

Premises used: ProbabilityTheory.poissonMeasure_real_singleton
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
⊢ HasSum (fun (i : ℕ) ↦ rexp (-(↑r : ℝ)) * ((↑r : ℝ) ^ i / (↑i ! : ℝ))) (rexp (-(↑r : ℝ)) * NormedSpace.exp (↑r : ℝ))

Tactic:
(NormedSpace.expSeries_div_hasSum_exp (r : ℝ)).mul_left (exp (-r))

Premises used: HasSum.mul_left, Real.exp, NormedSpace.expSeries_div_hasSum_exp, NNReal.toReal, Neg.neg
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
h :
  Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) fun (i : ℕ) ↦
    rexp (-(↑r : ℝ)) * ((↑r : ℝ) ^ i / (↑i ! : ℝ))
h₁ : 1 = rexp (-(↑r : ℝ)) * NormedSpace.exp (↑r : ℝ)
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) 1

Tactic:
convert! (NormedSpace.expSeries_div_hasSum_exp (r : ℝ)).mul_left (exp (-r)) using 1

Premises used: HasSum.mul_left, Real.exp, NormedSpace.expSeries_div_hasSum_exp, NNReal.toReal, Neg.neg
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) fun (i : ℕ) ↦
    rexp (-(↑r : ℝ)) * ((↑r : ℝ) ^ i / (↑i ! : ℝ))

Tactic:
simp_rw [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
⊢ 1 = rexp (-(↑r : ℝ)) * NormedSpace.exp (↑r : ℝ)

Tactic:
simp [← exp_eq_exp_ℝ, ← exp_add]

Premises used: Real.exp_eq_exp_ℝ, Real.exp_add
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
x : ℕ
⊢ 0 ≤ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
r : ℝ≥0
R : Type u_1
inst : NatCast R
inst_1 : MeasurableSpace R
⊢ IsProbabilityMeasure.{u_1} (α := R) (m0 := inst_1) Po(R, r)

Tactic:
Measure.isProbabilityMeasure_map .of_discrete

Premises used: AEMeasurable.of_discrete, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ ∀ (i : ℕ), ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ)) ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
rw :
  (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) * ‖f n‖
⊢ Integrable f Po(r) ↔ Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) * ‖f n‖

Tactic:
rw [poissonMeasure, integrable_sum_dirac_iff (by simp)]

Premises used: ProbabilityTheory.poissonMeasure, MeasureTheory.integrable_sum_dirac_iff
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
a :
  ∀ (n : ℕ),
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal =
      rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
⊢ (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) * ‖f n‖

Tactic:
congrm Summable (fun n ↦ ?_ * _)

Premises used: HMul.hMul, Summable, SummationFilter.unconditional
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup 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
r : ℝ≥0
f : ℕ → E
n : ℕ
a a₁ : rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
⊢ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑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
r : ℝ≥0
inst_3 : Countable R
inst_4 : MeasurableSingletonClass R
f : R → E
⊢ @Integrable _ _ _ _ inst_2 f Po(R, r) ↔ Integrable (f ∘ Nat.cast) Po(r)

Tactic:
integrable_map_measure .of_discrete .of_discrete

Premises used: MeasureTheory.AEStronglyMeasurable.of_discrete, AEMeasurable.of_discrete, MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
h :
  ∀ (x : ℕ),
    (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)) • f x =
      (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ))).toReal • f x
⊢ Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
x : ℕ
⊢ 0 ≤ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)

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

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
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
⊢ Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n

Tactic:
have : (fun n ↦ (exp (-r) * r ^ n / (n)!) • f n) =
      fun n ↦ (ENNReal.ofReal (exp (-r) * r ^ n / (n)!)).toReal • f n := by
    ext; rw [ENNReal.toReal_ofReal (by positivity)]
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n
rw :
  HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n)
    (∫ (n : ℕ), f n ∂Po(r))
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) (∫ (n : ℕ), f n ∂Po(r))

Tactic:
rw [this]
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n
⊢ ∀ (i : ℕ), ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ)) ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n
apply : Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n)
    (∫ (n : ℕ), f n ∂Po(r))

Tactic:
apply hasSum_integral_sum_dirac (by simp)

Premises used: MeasureTheory.hasSum_integral_sum_dirac
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) * ‖f n‖

Tactic:
integrable_poissonMeasure_iff.1 hf

Premises used: Iff.mp, ProbabilityTheory.integrable_poissonMeasure_iff
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n
h :
  ∀ (x : ℕ),
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ))).toReal =
      rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖

Tactic:
convert! integrable_poissonMeasure_iff.1 hf

Premises used: Iff.mp, ProbabilityTheory.integrable_poissonMeasure_iff
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n
x : ℕ
⊢ 0 ≤ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Poisson.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this :
  Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) fun (n : ℕ) ↦
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n
x : ℕ
h h₁ : rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)
⊢ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)

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
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
⊢ Eq.{u_1 + 1} (α := E) (∫ (n : ℕ), f n ∂Po(r)) (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n)

Tactic:
(hasSum_integral_poissonMeasure hf).tsum_eq.symm

Premises used: ProbabilityTheory.hasSum_integral_poissonMeasure, HasSum.tsum_eq, Eq.symm
-- 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 : CompleteSpace E
inst_5 : Countable R
inst_6 : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : @Integrable _ _ _ _ inst_2 f Po(R, r)
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))

Tactic:
rw [integral_map .of_discrete .of_discrete]

Premises used: MeasureTheory.integral_map, MeasureTheory.AEStronglyMeasurable.of_discrete, AEMeasurable.of_discrete
-- 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 : CompleteSpace E
inst_5 : Countable R
inst_6 : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : @Integrable _ _ _ _ inst_2 f Po(R, r)
⊢ Integrable (f ∘ Nat.cast) Po(r)

Tactic:
rw [integrable_map_cast_poissonMeasure_iff] at hf

Premises used: ProbabilityTheory.integrable_map_cast_poissonMeasure_iff
-- 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 : CompleteSpace E
inst_5 : Countable R
inst_6 : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable (f ∘ Nat.cast) Po(r)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℕ), f (↑x : R) ∂Po(r))
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))

Tactic:
integral_poissonMeasure' hf

Premises used: ProbabilityTheory.integral_poissonMeasure'
-- 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 : CompleteSpace E
inst_5 : Countable R
inst_6 : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable (f ∘ Nat.cast) Po(r)
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℕ), f (↑x : R) ∂Po(r))
    (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f (↑n : R))

Tactic:
exact integral_poissonMeasure' hf

Premises used: ProbabilityTheory.integral_poissonMeasure'
-- 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
⊢ ∀ (i : ℕ), ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ)) ≠ ⊤

Tactic:
simp
-- 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
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)
⊢ Eq.{u_1 + 1} (α := E) (∫ (n : ℕ), f n ∂Po(r)) (∑' (n : ℕ), (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n)

Tactic:
rw [poissonMeasure, integral_sum_dirac (by simp)]

Premises used: ProbabilityTheory.poissonMeasure, MeasureTheory.integral_sum_dirac