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

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < geometricPMFReal p n

Tactic:
by

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

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ geometricPMFReal p n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℝ
⊢ Measurable (geometricPMFReal p)

Tactic:
by

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)

Tactic:
by

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

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

Tactic:
by

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)
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₀)
⊢ ((traj κ a) x₀)[f | ↑piLE b] =ᵐ[(traj κ a) x₀] fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) (frestrictLe b x)

Tactic:
by

Goal state after:
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)))
x : ℝ
hx : x ∈ Ici t
⊢ 0 x ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
by

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
⊢ ∫⁻ (x : ℝ), paretoPDF t r x = 1

Tactic:
by

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
⊢ (paretoMeasure t r) univ = 1

Tactic:
by

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
x✝ : ℝ
⊢ 0 x✝ ≤ paretoPDFReal t r x✝

Tactic:
by

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ ↑(cdf (paretoMeasure t r)) x = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
by

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

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

Tactic:
by

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)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
⊢ ((traj κ a) x₀)[f | ↑piLE b] =ᵐ[(traj κ a) x₀] fun x ↦
    ∫ (y : (i : ↥(Iic c)) → X ↑i),
      ((traj κ a) x₀)[f | ↑piLE c] (updateFinset x (Iic c) y) ∂(partialTraj κ b c) (frestrictLe b x)

Tactic:
by

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 μ₀
⊢ AEMeasurable (⇑(piUnique fun i ↦ X ↑i).symm) μ₀

Tactic:
by

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 (trajMeasure μ₀ κ)

Tactic:
by

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 μ₀
a : ℕ
⊢ Measurable (frestrictLe a)

Tactic:
by

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 μ₀
a : ℕ
⊢ Measurable fun x ↦ (frestrictLe a x, x (a + 1))

Tactic:
by

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 μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X ↑i
⊢ Measurable fun x ↦ (frestrictLe a x, x (a + 1))

Tactic:
by

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 μ₀
a : ℕ
⊢ Measure.map (frestrictLe a) (trajMeasure μ₀ κ) ⊗ₘ κ a =
    Measure.map (fun x ↦ (frestrictLe a x, x (a + 1))) (trajMeasure μ₀ κ)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 μ₀
a : ℕ
inst✝¹ : StandardBorelSpace (X (a + 1))
inst✝ : Nonempty (X (a + 1))
⊢ Measurable (frestrictLe a)

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < Po(r).real {n}

Tactic:
by

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

Goal state before:
pp: r : ℝ≥0
⊢ HasSum (fun n ↦ rexp (-↑r) * ↑r ^ n / ↑n !) 1

Tactic:
by

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

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

Tactic:
by

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 μ₀
a : ℕ
inst✝¹ : StandardBorelSpace (X (a + 1))
inst✝ : Nonempty (X (a + 1))
⊢ Measurable fun x ↦ x (a + 1)

Tactic:
by

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

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
⊢ (fun n ↦ ↑n * p n * (1 / ↑n)) =ᶠ[atTop] p

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ ∀ (i : ℕ), ENNReal.ofReal (rexp (-↑r) * ↑r ^ i / ↑i !) ≠ ⊤

Tactic:
by

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

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
⊢ Tendsto p atTop (𝓝 0)

Tactic:
by

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 μ₀
a : ℕ
inst✝¹ : StandardBorelSpace (X (a + 1))
inst✝ : Nonempty (X (a + 1))
⊢ ⇑(condDistrib (fun x ↦ x (a + 1)) (frestrictLe a)
        (trajMeasure μ₀ κ)) =ᵐ[Measure.map (frestrictLe a) (trajMeasure μ₀ κ)]
    ⇑(κ a)

Tactic:
by

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)
⊢ (fun n ↦ ↑n ^ k / ↑k.factorial * p n ^ k) = fun n ↦ (↑n * p n) ^ k / ↑k.factorial

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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✝ : ℕ
⊢ 0 ≤ rexp (-↑r) * ↑r ^ x✝ / ↑x✝!

Tactic:
by

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) atTop (𝓝 (r ^ k / ↑k.factorial))

Tactic:
by

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)
⊢ (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) = fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n

Tactic:
by

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)
⊢ 0 < 1 / 2

Tactic:
by

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

Tactic:
by

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)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
n : ℕ
hn : k ≤ n
hne : p n < 1 / 2
⊢ 1 - p n ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a a' : α
⊢ a' ∈ (pure a).support ↔ a' ∈ {a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a a' : α
⊢ a' ∈ (pure a).support ↔ a' = a

Tactic:
by

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✝ : ℕ
⊢ 0 ≤ rexp (-↑r) * ↑r ^ x✝ / ↑x✝!

Tactic:
by

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)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
⊢ (fun n ↦ (1 - p n) ^ (n - k)) =ᶠ[atTop] fun n ↦ (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹

Tactic:
by

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)
⊢ HasSum (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) (∫ (n : ℕ), f n ∂Po(r))

Tactic:
by

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)
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)⁻¹
⊢ Real.exp (-r) = Real.exp (-r) * (1 ^ k)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ (pure a).toOuterMeasure s = if a ∈ s then 1 else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (pure a).toMeasure s = (Measure.dirac a) s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : α → PMF β
⊢ ∑' (b : α) (a : β), p b * (f b) a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ b ∈ ⋃ a ∈ p.support, (f a).support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ ∃ a ∈ p.support, b ∈ (f a).support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → PMF β
⊢ (pure a).bind f = f a

Tactic:
by

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

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

Tactic:
by

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 Po(R, r)
⊢ ∫ (x : R), f x ∂Po(R, r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : PMF α
x : α
⊢ p x * (pure x) x = p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
⊢ (p.bind fun x ↦ q) x = q x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : α → PMF β
g : β → PMF γ
b : γ
⊢ ((p.bind f).bind g) b = (p.bind fun a ↦ (f a).bind g) b

Tactic:
by

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)
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)⁻¹
⊢ 1 ^ k ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : α → β → PMF γ
b : γ
⊢ (p.bind fun a ↦ q.bind (f a)) b = (q.bind fun b ↦ p.bind fun a ↦ f a b) b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (b : β), if b ∈ s then ∑' (a : α), p a * (f a) b else 0

Tactic:
by

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 !) ≠ ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), p a * (f a) b else 0) = ∑' (a : α), p a * if b ∈ s then (f a) b else 0

Tactic:
by

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 (𝓝 (Real.exp (-r) * r ^ k / ↑k.factorial))

Tactic:
by

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 (𝓝 (Real.exp (-r) * r ^ k / ↑k.factorial))

Tactic:
by
  rw [mul_div_assoc, mul_comm]
  refine (tendsto_choose_mul_pow_atTop k hr).mul ?_
  have hp_lt_half : ∀ᶠ n in atTop, p n < 1 / 2 :=
    (tendsto_zero_of_tendsto_mul_atTop hr).eventually (Iio_mem_nhds (by norm_num))
  have hEq : (fun n => (1 - p n) ^ (n - k)) =ᶠ[atTop]
      (fun n => (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹) := by
    filter_upwards [eventually_ge_atTop k, hp_lt_half] with n hn hne
    rw [pow_sub₀ _ (by grind) hn]
  refine Tendsto.congr' hEq.symm ?_
  have : Real.exp (-r) = Real.exp (-r) * (1 ^ k)⁻¹ := by field
  rw [this]
  refine Tendsto.mul (Real.tendsto_one_add_pow_exp_of_tendsto ?_) ?_
  · simpa using hr.neg
  refine Tendsto.inv₀ (.pow ?_ k) (by simp)
  · simpa using tendsto_const_nhds.sub (tendsto_zero_of_tendsto_mul_atTop hr)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
⊢ (if b ∈ s then (f a) b else 0) = if b ∈ s then (f a) b else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
⊢ (p a * ∑' (b : β), if b ∈ s then (f a) b else 0) = p a * (f a).toOuterMeasure s

Tactic:
by

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

Goal state before:
pp: k : ℕ
r : ℝ≥0
p : ℕ → ↑unitInterval
hr : Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s

Tactic:
by

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

Goal state before:
pp: k : ℕ
r : ℝ≥0
p : ℕ → ↑unitInterval
hr : Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ ENNReal.ofReal (↑(n.choose k) * ↑(p n) ^ k * (1 - ↑(p n)) ^ (n - k))) atTop (𝓝 (Po(r) {k}))

Tactic:
by

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

Goal state before:
pp: k : ℕ
r : ℝ≥0
p : ℕ → ↑unitInterval
hr : Tendsto (fun n ↦ ↑n * ↑(p n)) atTop (𝓝 ↑r)
⊢ Tendsto (fun n ↦ Bin(n, p n) {k}) atTop (𝓝 (Po(r) {k}))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
⊢ (∑' (b : β) (a : α), p a * if h : p a = 0 then 0 else (f a h) b) = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
⊢ (p.bindOnSupport f).support = ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ b ∈ (p.bindOnSupport f).support ↔ ∃ a, ∃ (h : a ∈ p.support), b ∈ (f a h).support

Tactic:
by

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
n : ℕ
⊢ 0 ≤ rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
⊢ (p.bindOnSupport fun a x ↦ f a) = p.bind f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ (map f p) b = ∑' (a : α), if b = f a then p a else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ b ∈ (map f p).support ↔ b ∈ f '' p.support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ b ∈ (map f p).support ↔ ∃ a ∈ p.support, f a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : PMF α
g : β → γ
⊢ map g (map f p) = map (g ∘ f) p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
b : β
⊢ map (Function.const α b) p = pure b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (p.bindOnSupport f) b = 0 ↔ ∀ (a : α) (ha : p a ≠ 0), (f a ha) b = 0

Tactic:
by

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

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

Tactic:
by

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
⊢ ∫ (n : ℕ), f n ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f n

Tactic:
by

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).toMeasure s = p.toMeasure (f ⁻¹' s)

Tactic:
by

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✝² : FiniteDimensional ℝ E
r : ℝ≥0
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ ∫ (x : R), f x ∂Po(R, r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
by

Goal state after: