awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (hypothesis)
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
⊢ ∫⁻ (x : ℝ), paretoPDF t r x = 1
have leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
Tactic: have leftSide : ∫⁻ x in Iio t, paretoPDF t r x = 0 := lintegral_paretoPDF_of_le (le_refl t)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (hypothesis)
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
⊢ ∫⁻ (x : ℝ), paretoPDF t r x = 1
have rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
Tactic: have rightSide : ∫⁻ x in Ici t, paretoPDF t r x =
      ∫⁻ x in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1))) :=
    setLIntegral_congr_fun measurableSet_Ici (fun _ ↦ paretoPDF_of_le)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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 : ℝ), paretoPDF t r x = 1
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici t)) fun (a : ℝ) ↦
    r * t ^ r * a ^ (-(r + 1)))
  1
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
    leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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)))
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici t)) fun (a : ℝ) ↦
      r * t ^ r * a ^ (-(r + 1)))
    1
⊢ ∫⁻ (x : ℝ), paretoPDF t r x = 1
have hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ici t))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
    leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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)))
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici t)) fun (a : ℝ) ↦
      r * t ^ r * a ^ (-(r + 1)))
    1
hf :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ici t))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    r * t ^ r * x ^ (-(r + 1))
⊢ ∫⁻ (x : ℝ), paretoPDF t r x = 1
have hfm : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1)))
  (Measure.restrict volume (Ici t))
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
    leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici t)) fun (a : ℝ) ↦
      r * t ^ r * a ^ (-(r + 1)))
    1
have rw : r * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1
Tactic: rw [integral_Ici_eq_integral_Ioi, integral_const_mul, integral_Ioi_rpow_of_lt _ ht]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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)))
rw : r * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici t)) fun (a : ℝ) ↦
      r * t ^ r * a ^ (-(r + 1)))
    1
have rw₁ : -(r + 1) < -1
Tactic: rw [integral_Ici_eq_integral_Ioi, integral_const_mul, integral_Ioi_rpow_of_lt _ ht]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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)))
⊢ -(r + 1) < -1
have linarith : -1 ≤ -(r + 1) → 0 - r + (-1 - -(r + 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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)))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ici t))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    r * t ^ r * x ^ (-(r + 1))
have hf : ∀ᵐ (x : ℝ), x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))
Tactic: rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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 : x ∈ Ici t
⊢ 0 x ≤ r * t ^ r * x ^ (-(r + 1))
have positivity : 0 < x → 0 x ≤ r * t ^ r * x ^ (-(r + 1))
Tactic: positivity [lt_of_lt_of_le ht hx]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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 : ℝ), x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))
have hf : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))) x} a
Tactic: filter_upwards with x hx using by positivity [lt_of_lt_of_le ht hx]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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
⊢ ∀ᵐ (x : ℝ), x ∈ Ici t → 0 x ≤ r * t ^ r * x ^ (-(r + 1))
have hf₁ : ∀ a ∈ Ici t, 0 a ≤ r * t ^ r * a ^ (-(r + 1))
Tactic: filter_upwards with x hx using by positivity [lt_of_lt_of_le ht hx]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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)))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1)))
    (Measure.restrict volume (Ici t))
have hfm : paretoPDFReal t r =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ici t))] fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))
Tactic: apply (measurable_paretoPDFReal t r).aestronglyMeasurable.congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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))
have hfm : ∀ (x : ℝ) (hx : t ≤ x), paretoPDFReal t r x = (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))) x
Tactic: refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : t ≤ x) ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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))
⊢ paretoPDFReal t r x = (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))) x
have hfm₂ : (if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0) = r * t ^ r * x ^ (-(r + 1))
Tactic: simp_rw [paretoPDFReal, eq_true_intro hx, ite_true]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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))
⊢ paretoPDFReal t r x = (fun (x : ℝ) ↦ r * t ^ r * x ^ (-(r + 1))) x
have hfm₃ : (if True then r * t ^ r * x ^ (-(r + 1)) else 0) = r * t ^ r * x ^ (-(r + 1))
Tactic: simp_rw [paretoPDFReal, eq_true_intro hx, ite_true]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (hypothesis)
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ paretoPDFReal t r x
have this : IsProbabilityMeasure (paretoMeasure t r)
Tactic: have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ paretoPDFReal t r x
have rw : (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal =
  @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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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
have refine_1 : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Iic x))] paretoPDFReal t r
Tactic: refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ paretoPDFReal t r x
have refine_2 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (paretoPDFReal t r) (Measure.restrict volume (Iic x))
Tactic: refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (hypothesis)
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
have this : IsProbabilityMeasure (paretoMeasure t r)
Tactic: have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
Goal:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
have rw : (paretoMeasure t r).real (Iic x) = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
Tactic: rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
have rw₁ : Measure.real (m := measurableSpace) (Measure.withDensity volume (paretoPDF t r)) (Iic x) =
  (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
Tactic: rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
have rw₂ : ENNReal.toReal ((Measure.withDensity volume (paretoPDF t r) : (a : Set ℝ) → ℝ≥0∞) (Iic x)) =
  (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
Tactic: rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Pareto (goal)
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
⊢ (↑(cdf (paretoMeasure t r)) : ℝ → ℝ) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
have rw₃ : (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal
Tactic: rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
n : ℕ
⊢ (Po(r) : (a : Set ℕ) → ENNReal) {n} = ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))
have 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 ! : ℝ))
Tactic: rw [poissonMeasure, Measure.sum_smul_dirac_singleton]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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 ! : ℝ))
⊢ (Po(r) : (a : Set ℕ) → ENNReal) {n} = ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))
have rw₁ : ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) =
  ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))
Tactic: rw [poissonMeasure, Measure.sum_smul_dirac_singleton]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
n : ℕ
⊢ Po(r).real {n} = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
have rw : ENNReal.toReal ((Po(r) : (a : Set ℕ) → ENNReal) {n}) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
Tactic: rw [measureReal_def, poissonMeasure_singleton, ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
n : ℕ
rw : ENNReal.toReal ((Po(r) : (a : Set ℕ) → ENNReal) {n}) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
⊢ Po(r).real {n} = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
have rw₁ : (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
Tactic: rw [measureReal_def, poissonMeasure_singleton, ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
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 ! : ℝ)
⊢ Po(r).real {n} = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
have rw₂ : rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
Tactic: rw [measureReal_def, poissonMeasure_singleton, ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < Po(r).real {n}
have rw : 0 < rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
Tactic: rw [poissonMeasure_real_singleton]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) 1
have h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) fun (i : ℕ) ↦
  rexp (-(↑r : ℝ)) * ((↑r : ℝ) ^ i / (↑i ! : ℝ))
Tactic: convert! (NormedSpace.expSeries_div_hasSum_exp (r : ℝ)).mul_left (exp (-r)) using 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
r : ℝ≥0
h :
  Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) fun (i : ℕ) ↦
    rexp (-(↑r : ℝ)) * ((↑r : ℝ) ^ i / (↑i ! : ℝ))
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) 1
have h₁ : 1 = rexp (-(↑r : ℝ)) * NormedSpace.exp (↑r : ℝ)
Tactic: convert! (NormedSpace.expSeries_div_hasSum_exp (r : ℝ)).mul_left (exp (-r)) using 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ Integrable f Po(r) ↔ Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) * ‖f n‖
have rw : (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖) ↔
  Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) * ‖f n‖
Tactic: rw [poissonMeasure, integrable_sum_dirac_iff (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ (Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖) ↔
    Summable (α := ℝ) fun (n : ℕ) ↦ rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) * ‖f n‖
have a : ∀ (n : ℕ),
  (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
Tactic: congrm Summable (fun n ↦ ?_ * _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)
have a : rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑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
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
have h : ∀ (x : ℕ),
  (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)) • f x =
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ))).toReal • f x
Tactic: ext
-- 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 : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
x : ℕ
⊢ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)) • f x =
    (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ))).toReal • f x
have h : (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)) • f x = (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)) • f x
Tactic: rw [ENNReal.toReal_ofReal (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Poisson.Basic (hypothesis)
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)
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) (∫ (n : ℕ), f n ∂Po(r))
have 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
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)]
-- 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 : 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
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ)) • f n) (∫ (n : ℕ), f n ∂Po(r))
have rw : HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n)
  (∫ (n : ℕ), f n ∂Po(r))
Tactic: rw [this]
-- 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 : 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
⊢ HasSum.{u_1, 0} (α := E) (fun (n : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ n / (↑n ! : ℝ))).toReal • f n)
    (∫ (n : ℕ), f n ∂Po(r))
have apply : Summable (α := ℝ) fun (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖
Tactic: apply hasSum_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 : 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 (i : ℕ) ↦ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ i / (↑i ! : ℝ))).toReal * ‖f i‖
have h : ∀ (x : ℕ),
  (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)
Tactic: convert! integrable_poissonMeasure_iff.1 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 : 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 : ℕ
⊢ (ENNReal.ofReal (rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ))).toReal = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)
have h : rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ) = rexp (-(↑r : ℝ)) * (↑r : ℝ) ^ x / (↑x ! : ℝ)
Tactic: rw [ENNReal.toReal_ofReal (by positivity)]