mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this : (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) = fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n
⊢ HasSum (fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n)
    (∫ (n : ℕ), f n ∂Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n)

Tactic:
]

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this : (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) = fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n
⊢ HasSum (fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n)
    (∫ (n : ℕ), f n ∂Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n)
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this : (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) = fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n
n : ℕ
⊢ (1 - ↑p) ^ n * ↑p = (1 - ↑p) ^ n * ↑p

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
]

Goal state after:
case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
⊢ ∑' (i : ℕ), (ENNReal.ofReal ((1 - ↑p) ^ i * ↑p)).toReal • f i = ∑' (n : ℕ), ((1 - ↑p) ^ n * ↑p) • f n

Tactic:
]

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
⊢ ∑' (i : ℕ), (ENNReal.ofReal ((1 - ↑p) ^ i * ↑p)).toReal • f i = ∑' (n : ℕ), ((1 - ↑p) ^ n * ↑p) • f n
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x ↦ rexp (-(r * x))) (Ioc 0 x) volume

Tactic:
]

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x ↦ rexp (-(r * x))) (Ioc 0 x) volume
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: case e_f
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
n : ℕ
⊢ ((1 - ↑p) ^ n * ↑p) • f n = ((1 - ↑p) ^ n * ↑p) • f n

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i ↦ (1 - p) ^ i * p) 1
⊢ HasSum (fun n ↦ (1 - p) ^ n * p) 1

Tactic:
]

Goal state after:
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
this : HasSum (fun i ↦ (1 - p) ^ i * p) 1
⊢ HasSum (fun n ↦ (1 - p) ^ n * p) 1
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x ↦ r * rexp (-(r * x))) (Ioc 0 x) volume

Tactic:
]

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (fun x ↦ r * rexp (-(r * x))) (Ioc 0 x) volume
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < (1 - p) ^ n * p

Tactic:
]

Goal state after:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < (1 - p) ^ n * p
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ (1 - p) ^ n * p

Tactic:
]

Goal state after:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ (1 - p) ^ n * p
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p✝ : ↑unitInterval
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun a ↦ (geometricPMFReal p a).toNNReal) (toNNReal 1)

Tactic:
]

Goal state after:
p✝ : ↑unitInterval
p : ℝ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ HasSum (fun a ↦ (geometricPMFReal p a).toNNReal) (toNNReal 1)
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0

Tactic:
]

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case refine_1
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
t : Set ((i : ↥(Iic b)) → X ↑i)
mt : MeasurableSet t
⊢ ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' t, f y ∂(traj κ a) x₀ =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' t, f y ∂(traj κ a) x₀

pp: case refine_1.hf
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
t : Set ((i : ↥(Iic b)) → X ↑i)
mt : MeasurableSet t
⊢ Measurable (frestrictLe b)

pp: case refine_1
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
t : Set ((i : ↥(Iic b)) → X ↑i)
mt : MeasurableSet t
⊢ AEMeasurable (frestrictLe b) ((traj κ a) x₀)

Tactic:
]

Goal state after:
case refine_1.hf
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
t : Set ((i : ↥(Iic b)) → X ↑i)
mt : MeasurableSet t
⊢ Measurable (frestrictLe b)

case refine_1
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
t : Set ((i : ↥(Iic b)) → X ↑i)
mt : MeasurableSet t
⊢ AEMeasurable (frestrictLe b) ((traj κ a) x₀)
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: 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)))
⊢ ∫ (a : ℝ) in Ici t, r * t ^ r * a ^ (-(r + 1)) = 1

pp: case hf
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)))
⊢ 0 ≤ᵐ[volume.restrict (Ici t)] fun x ↦ r * t ^ r * x ^ (-(r + 1))

pp: case hfm
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 (fun x ↦ r * t ^ r * x ^ (-(r + 1))) (volume.restrict (Ici t))

Tactic:
]

Goal state after:
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)))
⊢ ∫ (a : ℝ) in Ici t, r * t ^ r * a ^ (-(r + 1)) = 1

case hf
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)))
⊢ 0 ≤ᵐ[volume.restrict (Ici t)] fun x ↦ r * t ^ r * x ^ (-(r + 1))

case hfm
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 (fun x ↦ r * t ^ r * x ^ (-(r + 1))) (volume.restrict (Ici t))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: 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 * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1

pp: 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

Tactic:
]

Goal state after:
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 * t ^ r * (-t ^ (-(r + 1) + 1) / (-(r + 1) + 1)) = 1

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
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case hf
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))

Tactic:
]

Goal state after:
case hf
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))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
]

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
⊢ IsProbabilityMeasure (⇑(traj κ 0) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀)

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
⊢ IsProbabilityMeasure (⇑(traj κ 0) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
⊢ IsProbabilityMeasure (⇑(traj κ 0) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀)

Tactic:
have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piUnique ((fun i : Iic 0 ↦ X i))).symm) :=
    Measure.isProbabilityMeasure_map <| by fun_prop

Goal state after:
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
this : IsProbabilityMeasure (Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀)
⊢ IsProbabilityMeasure (⇑(traj κ 0) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
a : ℕ
⊢ ⇑(Kernel.id ×ₖ κ a ∘ₖ partialTraj κ 0 a) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀ =
    ⇑((traj κ 0).map fun x ↦ (frestrictLe a x, x (a + 1))) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
a : ℕ
⊢ ⇑(Kernel.id ×ₖ κ a ∘ₖ partialTraj κ 0 a) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀ =
    ⇑((traj κ 0).map fun x ↦ (frestrictLe a x, x (a + 1))) ∘ₘ Measure.map (⇑(piUnique fun i ↦ X ↑i).symm) μ₀
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e_f
X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X ↑i
⊢ Measure.map (fun x ↦ (frestrictLe a x, x (a + 1))) ((traj κ 0) x₀) =
    Measure.map (fun x ↦ (frestrictLe a x, x (a + 1))) ((traj κ 0) x₀)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !) = ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ rexp (-↑r) * ↑r ^ n / ↑n ! = rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
]

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

Goal state before:
pp: 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‖

Tactic:
]

Goal state after:
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‖
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ rexp (-↑r) * ↑r ^ n / ↑n ! = rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
x✝ : ℕ
⊢ (rexp (-↑r) * ↑r ^ x✝ / ↑x✝!) • f x✝ = (rexp (-↑r) * ↑r ^ x✝ / ↑x✝!) • f x✝

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: 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)))

Tactic:
]

Goal state after:
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)))
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this : (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) = fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n
⊢ HasSum (fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n) (∫ (n : ℕ), f n ∂Po(r))

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this : (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) = fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n
⊢ HasSum (fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n) (∫ (n : ℕ), f n ∂Po(r))
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
n : ℕ
hn : k ≤ n
hne : p n < 1 / 2
⊢ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹ = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this : (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) = fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n
x✝ : ℕ
⊢ rexp (-↑r) * ↑r ^ x✝ / ↑x✝! = rexp (-↑r) * ↑r ^ x✝ / ↑x✝!

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = s.indicator 1 a

Tactic:
]

Goal state after:
α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = s.indicator 1 a
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable f Po(R, r)
⊢ ∫ (x : ℕ), f ↑x ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable f Po(R, r)
⊢ ∫ (x : ℕ), f ↑x ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
h : MeasurableSingletonClass α
⊢ Measure.dirac a = Measure.dirac a

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable (f ∘ Nat.cast) Po(r)
⊢ ∫ (x : ℕ), f ↑x ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable (f ∘ Nat.cast) Po(r)
⊢ ∫ (x : ℕ), f ↑x ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : (fun n ↦ (1 - p n) ^ (n - k)) =ᶠ[atTop] fun n ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
this : Real.exp (-r) = Real.exp (-r) * (1 ^ k)⁻¹
⊢ Tendsto (fun n ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r) * (1 ^ k)⁻¹))

Tactic:
]

Goal state after:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
hEq : (fun n ↦ (1 - p n) ^ (n - k)) =ᶠ[atTop] fun n ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
this : Real.exp (-r) = Real.exp (-r) * (1 ^ k)⁻¹
⊢ Tendsto (fun n ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) atTop (𝓝 (Real.exp (-r) * (1 ^ k)⁻¹))
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
p : PMF α
x : α
⊢ p x = p x

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
⊢ q x = q x

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ ∑' (i : ℕ), (ENNReal.ofReal (rexp (-↑r) * ↑r ^ i / ↑i !)).toReal • f i =
    ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f n

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ ∑' (i : ℕ), (ENNReal.ofReal (rexp (-↑r) * ↑r ^ i / ↑i !)).toReal • f i =
    ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f n
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : ¬p a = 0
⊢ p a = p a

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: case e_f
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
n : ℕ
⊢ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n = (rexp (-↑r) * ↑r ^ n / ↑n !) • f n

Tactic:
]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ (map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ (map f p).toOuterMeasure s = p.toOuterMeasure (f ⁻¹' s)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
r : ℝ≥0
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
]

Goal state after: