mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case 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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ AEStronglyMeasurable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)

Tactic:
·

Goal state after:
case 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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ AEStronglyMeasurable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: case hf
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 ≤ᵐ[volume.restrict (Ioo 0 1)] fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

pp: case hfm
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (volume.restrict (Ioo 0 1))

Tactic:
·

Goal state after:
case hf
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 ≤ᵐ[volume.restrict (Ioo 0 1)] fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: case hfm
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (volume.restrict (Ioo 0 1))

Tactic:
·

Goal state after:
case hfm
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (volume.restrict (Ioo 0 1))
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ (betaMeasure α β) univ = 1

Tactic:
by simp [betaMeasure, lintegral_betaPDF_eq_one hα hβ]

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

Goal state before:
pp: case hφ
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
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀)

pp: case hfm
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
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ AEStronglyMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))

Tactic:
·

Goal state after:
case hφ
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
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hfm
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
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ AEStronglyMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))

Tactic:
·

Goal state after:
case hfm
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
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
mf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ AEStronglyMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))
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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X ↑i), ((traj κ b) a) (Prod.mk a ⁻¹' s) ∂(partialTraj κ a b) u =
    ∫⁻ (b_1 : (i : ↥(Iic b)) → X ↑i), ((traj κ b) b_1) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s) ∂(partialTraj κ a b) u

pp: case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

pp: case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, x)

pp: case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X ↑i), ((traj κ b) a) (Prod.mk a ⁻¹' s) ∂(partialTraj κ a b) u =
    ∫⁻ (b_1 : (i : ↥(Iic b)) → X ↑i), ((traj κ b) b_1) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s) ∂(partialTraj κ a b) u
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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) =
    ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' (fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

pp: case e_f.hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ Measurable fun x_1 ↦ updateFinset x_1 (Iic b) x

pp: case e_f.hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

pp: case e_f.hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ Measurable fun x_1 ↦ updateFinset x_1 (Iic b) x

pp: case e_f.hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet (Prod.mk x ⁻¹' s)

Tactic:
·

Goal state after:
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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) =
    ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' (fun x ↦ (frestrictLe b x, x)) ⁻¹' s)
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: case pos
x₀ : ℝ
γ : ℝ≥0
x : ℝ
h : γ = 0
⊢ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹ = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹

pp: case neg
x₀ : ℝ
γ : ℝ≥0
x : ℝ
h : ¬γ = 0
⊢ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹ = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹

Tactic:
·

Goal state after:
case pos
x₀ : ℝ
γ : ℝ≥0
x : ℝ
h : γ = 0
⊢ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹ = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

pp: x a r : ℝ
hx : x ≤ 0
⊢ EqOn (gammaPDF a r) (fun x ↦ 0) (Iio x)

Tactic:
·

Goal state after:
x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: x a r : ℝ
hx : x ≤ 0
⊢ EqOn (gammaPDF a r) (fun x ↦ 0) (Iio x)

Tactic:
·

Goal state after:
x a r : ℝ
hx : x ≤ 0
⊢ EqOn (gammaPDF a r) (fun x ↦ 0) (Iio x)
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: case pos
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ Integrable (cauchyPDFReal x₀ γ) volume

pp: case neg
x₀ : ℝ
γ : ℝ≥0
h : γ ≠ 0
⊢ Integrable (cauchyPDFReal x₀ γ) volume

Tactic:
·

Goal state after:
case pos
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ Integrable (cauchyPDFReal x₀ γ) volume
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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (n : ℕ) → X n), A.indicator (fun x_1 ↦ f x_1 x) (frestrictLe b x) ∂(traj κ a) u =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f (frestrictLe b y) y ∂(traj κ a) u

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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ Integrable (uncurry fun x y ↦ A.indicator (fun x ↦ f x y) x) ((partialTraj κ a b) u ⊗ₘ traj κ b)

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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ ∫ (x : (n : ℕ) → X n), A.indicator (fun x_1 ↦ f x_1 x) (frestrictLe b x) ∂(traj κ a) u =
    ∫ (y : (n : ℕ) → X n) in frestrictLe b ⁻¹' A, f (frestrictLe b y) y ∂(traj κ a) u
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
k : ℕ
⊢ ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) =
    (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k}

pp: case h₀
n : ℕ
p : ↑I
k : ℕ
⊢ ∀ b ∈ Finset.Iic n, b ≠ k → (ENNReal.ofReal (↑(n.choose b) * ↑p ^ b * (1 - ↑p) ^ (n - b)) • dirac b) {k} = 0

pp: case h₁
n : ℕ
p : ↑I
k : ℕ
⊢ k ∉ Finset.Iic n → (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k} = 0

Tactic:
·

Goal state after:
n : ℕ
p : ↑I
k : ℕ
⊢ ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) =
    (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k}
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: case h₀
n : ℕ
p : ↑I
k : ℕ
⊢ ∀ b ∈ Finset.Iic n, b ≠ k → (ENNReal.ofReal (↑(n.choose b) * ↑p ^ b * (1 - ↑p) ^ (n - b)) • dirac b) {k} = 0

pp: case h₁
n : ℕ
p : ↑I
k : ℕ
⊢ k ∉ Finset.Iic n → (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k} = 0

Tactic:
·

Goal state after:
case h₀
n : ℕ
p : ↑I
k : ℕ
⊢ ∀ b ∈ Finset.Iic n, b ≠ k → (ENNReal.ofReal (↑(n.choose b) * ↑p ^ b * (1 - ↑p) ^ (n - b)) • dirac b) {k} = 0
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: case h₁
n : ℕ
p : ↑I
k : ℕ
⊢ k ∉ Finset.Iic n → (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k} = 0

Tactic:
·

Goal state after:
case h₁
n : ℕ
p : ↑I
k : ℕ
⊢ k ∉ Finset.Iic n → (ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k) {k} = 0
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: case e'_8
r x : ℝ
⊢ (fun a ↦ -rexp (-(r * a))) = fun y ↦ -1 * rexp (-r * id y)

pp: case e'_9
r x : ℝ
⊢ r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))

Tactic:
·

Goal state after:
case e'_8
r x : ℝ
⊢ (fun a ↦ -rexp (-(r * a))) = fun y ↦ -1 * rexp (-r * id y)
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫ (a_1 : ℝ) in Ici 0, r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)) = 1

pp: case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ 0 ≤ᵐ[volume.restrict (Ici 0)] fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

pp: case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (volume.restrict (Ici 0))

Tactic:
·

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫ (a_1 : ℝ) in Ici 0, r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)) = 1
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → E
⊢ ∑ i ≤ n, ∫ (a : ℕ), f a ∂ENNReal.ofReal (↑(n.choose i) * ↑p ^ i * (1 - ↑p) ^ (n - i)) • dirac i =
    ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f k

pp: n : ℕ
p : ↑I
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → E
⊢ ∀ i ∈ Finset.Iic n, Integrable f (ENNReal.ofReal (↑(n.choose i) * ↑p ^ i * (1 - ↑p) ^ (n - i)) • dirac i)

Tactic:
·

Goal state after:
n : ℕ
p : ↑I
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → E
⊢ ∑ i ≤ n, ∫ (a : ℕ), f a ∂ENNReal.ofReal (↑(n.choose i) * ↑p ^ i * (1 - ↑p) ^ (n - i)) • dirac i =
    ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f k
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ AEStronglyMeasurable (fun x ↦ r * rexp (-(r * x))) (volume.restrict (Icc 0 x))

pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞

Tactic:
·

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_1
α : Type u_1
p : PMF α
s : Finset α
⊢ ∀ b ∉ s, (↑s).indicator (⇑p) b = 0

pp: case refine_2
α : Type u_1
p : PMF α
s : Finset α
⊢ ∑ b ∈ s, (↑s).indicator (⇑p) b = ∑ x ∈ s, p x

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
p : PMF α
s : Finset α
⊢ ∀ b ∉ s, (↑s).indicator (⇑p) b = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
s : Finset α
⊢ ∑ b ∈ s, (↑s).indicator (⇑p) b = ∑ x ∈ s, p x

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
p : PMF α
s : Finset α
⊢ ∑ b ∈ s, (↑s).indicator (⇑p) b = ∑ x ∈ s, p x
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0

pp: case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ 0 ≤ᵐ[volume.restrict (Ici 0)] fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

pp: case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (volume.restrict (Ici 0))

Tactic:
·

Goal state after:
case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ 0 ≤ᵐ[volume.restrict (Ici 0)] fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
⊢ a ∈ s

pp: case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
⊢ a ∈ s
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (volume.restrict (Ici 0))

Tactic:
·

Goal state after:
case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (volume.restrict (Ici 0))
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ IntervalIntegrable (fun a ↦ r * rexp (-(r * a))) volume 0 x

pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ContinuousOn (fun a ↦ -1 * rexp (-(r * a))) (Icc 0 x)

pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun a ↦ -1 * rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1

Tactic:
·

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case refine_1
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] gammaPDFReal a r

pp: case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (volume.restrict (Iic x))

Tactic:
·

Goal state after:
case refine_1
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] gammaPDFReal a r
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (volume.restrict (Iic x))

Tactic:
·

Goal state after:
case refine_2
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ AEStronglyMeasurable (gammaPDFReal a r) (volume.restrict (Iic x))
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: case pos
p : ↑unitInterval
h : p ≠ 0
⊢ IsProbabilityMeasure (Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n)

pp: case neg
p : ↑unitInterval
h : ¬p ≠ 0
⊢ IsProbabilityMeasure (Measure.dirac 0)

Tactic:
·

Goal state after:
case pos
p : ↑unitInterval
h : p ≠ 0
⊢ IsProbabilityMeasure (Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n)
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: case neg
p : ↑unitInterval
h : ¬p ≠ 0
⊢ IsProbabilityMeasure (Measure.dirac 0)

Tactic:
·

Goal state after:
case neg
p : ↑unitInterval
h : ¬p ≠ 0
⊢ IsProbabilityMeasure (Measure.dirac 0)