mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Decision.Risk.Countable

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝¹ : Fintype 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
μ : Measure 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
⊢ avgRisk ℓ (Kernel.const Θ μ) κ π = ∑ y, ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ μ) {y} ∂π

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂⇑(Kernel.boolKernel μ ν) ∘ₘ π,
    (((Kernel.boolKernel μ ν)†π) x) {true} = π {true} * (∂ν/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
⊢ Ber(x, y, 0) = dirac y

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
⊢ Ber(x, y, 1) = dirac x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Ber(x, y, p) s = if x ∈ s then if y ∈ s then 1 else ↑(toNNReal p) else if y ∈ s then ↑(toNNReal (σ p)) else 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Ber(x, y, p).real s = if x ∈ s then if y ∈ s then 1 else ↑(toNNReal p) else if y ∈ s then ↑(toNNReal (σ p)) else 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∈ s
⊢ Ber(x, y, p) s = 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∈ s
⊢ Ber(x, y, p).real s = 1

Tactic:
by

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ beta α β = ((↑α).betaIntegral ↑β).re

Tactic:
by

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

Goal state before:
pp: α β x : ℝ
hx : x ≤ 0
⊢ betaPDF α β x = 0

Tactic:
by

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

Goal state before:
pp: α β x : ℝ
hx : 1 ≤ x
⊢ betaPDF α β x = 0

Tactic:
by

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

Goal state before:
pp: α β x : ℝ
hx_pos : 0 < x
hx_lt : x < 1
⊢ betaPDF α β x = ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∉ s
⊢ Ber(x, y, p) s = ↑(toNNReal p)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hl : Measurable (Function.uncurry ℓ)
h : HasArgminEstimator ℓ P π
⊢ bayesRisk ℓ P π = ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∈ s
hy : y ∉ s
⊢ Ber(x, y, p).real s = ↑p

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∈ s
⊢ Ber(x, y, p) s = ↑(toNNReal (σ p))

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∈ s
⊢ Ber(x, y, p).real s = 1 - ↑p

Tactic:
by

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

Goal state before:
pp: α β : ℝ
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∉ s
⊢ Ber(x, y, p) s = 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
hx : x ∉ s
hy : y ∉ s
⊢ Ber(x, y, p).real s = 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
x y : X
p : ↑I
⊢ Ber(x, y, p) Set.univ = 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
x : X
p : ↑I
⊢ Ber(x, x, p) = dirac x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : MeasurableSingletonClass X
inst✝ : MeasurableSingletonClass Y
x✝ y : X
f : X → Y
p : ↑I
x : X
⊢ AEMeasurable f (dirac x)

Tactic:
by

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

Goal state before:
pp: α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
⊢ 0 < 1 - x

Tactic:
by

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

Goal state before:
pp: α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
⊢ 0 < betaPDFReal α β x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : MeasurableSingletonClass X
inst✝ : MeasurableSingletonClass Y
x y : X
f : X → Y
p : ↑I
hf : ∀ (x : X), AEMeasurable f (dirac x)
⊢ AEMeasurable f (toNNReal p • dirac x)

Tactic:
by

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

Goal state before:
pp: α β : ℝ
⊢ Measurable fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
by

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

Goal state before:
pp: α β : ℝ
⊢ Measurable fun x ↦ 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : MeasurableSingletonClass X
inst✝ : MeasurableSingletonClass Y
x y : X
f : X → Y
p : ↑I
hf : ∀ (x : X), AEMeasurable f (dirac x)
⊢ AEMeasurable f (toNNReal (σ p) • dirac y)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : MeasurableSingletonClass X
inst✝ : MeasurableSingletonClass Y
x y : X
f : X → Y
p : ↑I
⊢ map f Ber(x, y, p) = Ber(f x, f y, p)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
x y : X
f : X → Y
hf : Measurable f
p : ↑I
⊢ map f Ber(x, y, p) = Ber(f x, f y, p)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ Integrable f Ber(x, y, p)

Tactic:
by

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 ≤ 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ ‖f x‖ₑ < ∞

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ ‖f y‖ₑ < ∞

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ ∫ (z : X), f z ∂Ber(x, y, p) = ↑p • f x + (1 - ↑p) • f y

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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ a) x₀)
⊢ ∀ᵐ (x : (i : ℕ) → X i) ∂(traj κ a) x₀, Integrable f ((traj κ b) (frestrictLe b x))

Tactic:
by

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 < (↑α).re

Tactic:
by

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 < (↑β).re

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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
hf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ ∀ᵐ (x : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, AEStronglyMeasurable f ((traj κ b) x)

Tactic:
by

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Measurable fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
by

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫⁻ (x : ℝ), betaPDF α β x = 1

Tactic:
rw [lintegral_betaPDF, ← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae]
  · simp_rw [mul_assoc, integral_const_mul]
    field_simp
    rw [div_eq_one_iff_eq (ne_of_gt (beta_pos hα hβ)), beta_eq_betaIntegralReal α β hα hβ,
      betaIntegral, intervalIntegral.integral_of_le (by norm_num),
      ← integral_Ioc_eq_integral_Ioo, ← RCLike.re_to_complex, ← integral_re]
    · refine setIntegral_congr_fun measurableSet_Ioc fun x ⟨hx1, hx₂⟩ ↦ ?_
      norm_cast
      rw [← Complex.ofReal_cpow, ← Complex.ofReal_cpow, RCLike.re_to_complex,
        Complex.re_mul_ofReal, Complex.ofReal_re]
      all_goals linarith
    convert! betaIntegral_convergent (u := α) (v := β) (by simpa) (by simpa)
    rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp), IntegrableOn]
  · refine ae_restrict_of_forall_mem measurableSet_Ioo (fun x hx ↦ ?_)
    convert! betaPDFReal_pos hx.1 hx.2 hα hβ |>.le using 1
    rw [betaPDFReal, if_pos ⟨hx.1, hx.2⟩]
  · exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫⁻ (x : ℝ), betaPDF α β x = 1

Tactic:
by

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ (betaMeasure α β) univ = 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)
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₀)
⊢ ∫ (x : (n : ℕ) → X n), f x ∂(traj κ a) x₀ = ∫ (x : (n : ℕ) → X n), f (updateFinset x (Iic a) x₀) ∂(traj κ a) 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)
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 ↦ (frestrictLe b 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)
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 (Prod.mk 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)
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)

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)
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 ↦ 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)
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 ?m.371

Tactic:
by

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
⊢ Measurable ?m.371
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
⊢ (partialTraj κ a b) u ⊗ₘ traj κ b = Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) u)

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)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
hf : (fun x ↦ (frestrictLe b x, x (b + 1))) = (Prod.map id fun x ↦ x (b + 1)) ∘ fun x ↦ (frestrictLe b x, x)
⊢ Measurable (Prod.map id fun x ↦ x (b + 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)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
hf : (fun x ↦ (frestrictLe b x, x (b + 1))) = (Prod.map id fun x ↦ x (b + 1)) ∘ fun x ↦ (frestrictLe b x, x)
⊢ Measurable fun x ↦ (frestrictLe b 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)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
hf : (fun x ↦ (frestrictLe b x, x (b + 1))) = (Prod.map id fun x ↦ x (b + 1)) ∘ fun x ↦ (frestrictLe b x, x)
⊢ Measurable fun x ↦ x (b + 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)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X ↑n
⊢ (partialTraj κ a b) x₀ ⊗ₘ κ b = Measure.map (fun x ↦ (frestrictLe b x, x (b + 1))) ((traj κ a) x₀)

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
⊢ cauchyPDFReal x₀ 0 = 0

Tactic:
by

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

Goal state before:
pp: p : ↑I
⊢ Bin(0, p) = dirac 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MeasurableSpace R
inst✝ : AddMonoidWithOne R
p : ↑I
⊢ Bin(R, 0, p) = dirac 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace R
inst✝ : AddMonoidWithOne R
m : MeasurableSpace Ω
P : Measure Ω
X : Ω → R
n : ℕ
p : ↑I
⊢ AEMeasurable ncard setBer(Iio n, p)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : ↑I
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ Measurable fun x ↦ x ≤ n

Tactic:
by

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

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : ↑I
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ AEMeasurable ncard setBer(Iio n, p)

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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
hf' : Integrable (uncurry f) (Measure.map (fun x ↦ (frestrictLe b x, x)) ((traj κ a) x₀))
⊢ AEMeasurable (fun x ↦ (frestrictLe b x, x)) ((traj κ a) x₀)

Tactic:
by

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

Goal state before:
pp: y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∫⁻ (x : ℝ) in Iic y, f x = (∫⁻ (x : ℝ) in Iio z, f x) + ∫⁻ (x : ℝ) in Icc z y, f x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a r x : ℝ
hx : x < 0
⊢ gammaPDF a r x = 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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i), ∫ (y : (n : ℕ) → X n), f x y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (x : (n : ℕ) → X n), f (frestrictLe b x) x ∂(traj κ a) x₀

Tactic:
by

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

Goal state before:
pp: a r x : ℝ
hx : 0 ≤ x
⊢ gammaPDF a r x = ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
⊢ cauchyPDF x₀ 0 = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : ↑I
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ ∀ᵐ (ω : Ω) ∂P, X ω ≤ n

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ cauchyPDF x₀ γ x = ENNReal.ofReal (cauchyPDFReal x₀ γ x)

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
⊢ Measurable (cauchyPDFReal x₀ γ)

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
⊢ StronglyMeasurable (cauchyPDFReal x₀ γ)

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
⊢ Measurable (cauchyPDF x₀ γ)

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
⊢ StronglyMeasurable (cauchyPDF x₀ γ)

Tactic:
by

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

Goal state before:
pp: n k : ℕ
p : ↑I
⊢ Bin(n, p).real {k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

Tactic:
by

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

Goal state before:
pp: n k : ℕ
p : ↑I
⊢ Bin(n, p) {k} ≠ ∞

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
x : ℝ
⊢ 0 < cauchyPDFReal x₀ γ x

Tactic:
by

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

Goal state before:
pp: x a✝¹ r : ℝ
hx : x ≤ 0
a : ℝ
a✝ : a < x
⊢ ¬0 ≤ a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∫ (x : ℝ), cauchyPDFReal x₀ γ x = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n k : ℕ
p : ↑I
⊢ Measurable Nat.cast

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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ a) x₀)
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i), ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (x : (n : ℕ) → X n), f x ∂(traj κ a) x₀

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n k : ℕ
p : ↑I
⊢ MeasurableSet {↑k}

Tactic:
by

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

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

Tactic:
by

Goal state after: