mathlib-initiative/mathlib-tactics huggingface dataset:
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))
⊢ 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))
⊢ IntervalIntegrable (fun a ↦ r * rexp (-(r * a))) volume 0 x
Module: Mathlib.Probability.Distributions.Pareto

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

pp: t r x : ℝ
hx : x ≤ t
⊢ EqOn (paretoPDF t r) (fun x ↦ 0) (Iio x)

Tactic:
·

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

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

Tactic:
·

Goal state after:
t r x : ℝ
hx : x ≤ t
⊢ EqOn (paretoPDF t r) (fun x ↦ 0) (Iio x)
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₀))
⊢ ∀ (s : Set ((i : ℕ) → X i)),
    MeasurableSet s →
      ((traj κ a) x₀) s < ∞ →
        ∫ (x : (i : ℕ) → X i) in s,
            ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) x ∂(traj κ a) x₀ =
          ∫ (x : (i : ℕ) → X i) in s, f x ∂(traj κ a) x₀

pp: case refine_2
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₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) ((traj κ a) x₀)

Tactic:
·

Goal state after:
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₀))
⊢ ∀ (s : Set ((i : ℕ) → X i)),
    MeasurableSet s →
      ((traj κ a) x₀) s < ∞ →
        ∫ (x : (i : ℕ) → X i) in s,
            ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) x ∂(traj κ a) x₀ =
          ∫ (x : (i : ℕ) → X i) in s, f x ∂(traj κ a) x₀
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))
⊢ 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))
⊢ ContinuousOn (fun a ↦ -1 * rexp (-(r * a))) (Icc 0 x)
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))
⊢ ∀ 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))
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun a ↦ -1 * rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1
Module: Mathlib.Probability.Distributions.Pareto

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

pp: case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0

Tactic:
·

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

Goal state before:
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
⊢ AEStronglyMeasurable (fun x ↦ r * rexp (-(r * x))) (volume.restrict (Icc 0 x))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0

Tactic:
·

Goal state after:
case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
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
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
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
    apply ENNReal.hasSum_coe.mpr
    rw [← toNNReal_one]
    exact (geometricPMFRealSum hp_pos hp_le_one).toNNReal
      (fun n ↦ geometricPMFReal_nonneg hp_pos hp_le_one)

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

Goal state before:
pp: case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 1 - rexp (-(r * x))

pp: case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 ≤ 0

Tactic:
·

Goal state after:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 1 - rexp (-(r * x))
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 ≤ 0

Tactic:
·

Goal state after:
case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ 0 ≤ 0
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
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case refine_2
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₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) ((traj κ a) x₀)

Tactic:
·

Goal state after:
case refine_2
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₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ 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)))
⊢ 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
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)))
⊢ 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:
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))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
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:
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: case refine_1
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] paretoPDFReal t r

pp: case refine_2
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ AEStronglyMeasurable (paretoPDFReal t r) (volume.restrict (Iic x))

Tactic:
·

Goal state after:
case refine_1
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] paretoPDFReal t r
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case refine_2
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ AEStronglyMeasurable (paretoPDFReal t r) (volume.restrict (Iic x))

Tactic:
·

Goal state after:
case refine_2
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ AEStronglyMeasurable (paretoPDFReal t r) (volume.restrict (Iic x))
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: case e'_5
r : ℝ≥0
⊢ (fun n ↦ rexp (-↑r) * ↑r ^ n / ↑n !) = fun i ↦ rexp (-↑r) * (↑r ^ i / ↑i !)

pp: case e'_6
r : ℝ≥0
⊢ 1 = rexp (-↑r) * NormedSpace.exp ↑r

Tactic:
·

Goal state after:
case e'_5
r : ℝ≥0
⊢ (fun n ↦ rexp (-↑r) * ↑r ^ n / ↑n !) = fun i ↦ rexp (-↑r) * (↑r ^ i / ↑i !)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: case e'_6
r : ℝ≥0
⊢ 1 = rexp (-↑r) * NormedSpace.exp ↑r

Tactic:
·

Goal state after:
case e'_6
r : ℝ≥0
⊢ 1 = rexp (-↑r) * NormedSpace.exp ↑r
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 1

pp: case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 1
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

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

Tactic:
rw [pure_apply_self, mul_one]

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

Goal state before:
pp: case refine_1
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 ↦ ↑n * -p n) atTop (𝓝 (-r))

pp: case refine_2
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) ^ k)⁻¹) atTop (𝓝 (1 ^ k)⁻¹)

Tactic:
·

Goal state after:
case refine_1
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 ↦ ↑n * -p n) atTop (𝓝 (-r))
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: case refine_2
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) atTop (𝓝 1)

Tactic:
·

Goal state after:
case refine_2
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) atTop (𝓝 1)
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : p a = 0
⊢ p a * ∑' (i : β), 0 = p a

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 * ∑' (i : β), (f a h) i = p a

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : p a = 0
⊢ p a * ∑' (i : β), 0 = p a
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 * ∑' (i : β), (f a h) i = p a

Tactic:
·

Goal state after:
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 * ∑' (i : β), (f a h) i = p a
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.toMeasure (f ⁻¹' s)

Tactic:
toMeasure_apply_eq_toOuterMeasure_apply _ (measurableSet_preimage hf hs)

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.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false
p : ℝ≥0
h : p ≤ 1
⊢ false ∈ (bernoulli p h).support ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}

pp: case true
p : ℝ≥0
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
·

Goal state after:
case false
p : ℝ≥0
h : p ≤ 1
⊢ false ∈ (bernoulli p h).support ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
h : μ {ω | X ω = 1} = ⊤
⊢ ∫ (y : ℝ), id y ∂(μ (X ⁻¹' {0}) • Measure.dirac 0 + μ (X ⁻¹' {1}) • Measure.dirac 1) = μ.real {ω | X ω = 1}

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
h : ¬μ {ω | X ω = 1} = ⊤
⊢ ∫ (y : ℝ), id y ∂(μ (X ⁻¹' {0}) • Measure.dirac 0 + μ (X ⁻¹' {1}) • Measure.dirac 1) = μ.real {ω | X ω = 1}

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
h : μ {ω | X ω = 1} = ⊤
⊢ ∫ (y : ℝ), id y ∂(μ (X ⁻¹' {0}) • Measure.dirac 0 + μ (X ⁻¹' {1}) • Measure.dirac 1) = μ.real {ω | X ω = 1}
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 β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : (f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * 0)

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false.mp
p : ℝ≥0
h : p ≤ 1
⊢ 1 - ↑p = 0 → p = 1

pp: case false.mpr
p : ℝ≥0
h : p ≤ 1
⊢ p = 1 → 1 - ↑p = 0

Tactic:
·

Goal state after:
case false.mp
p : ℝ≥0
h : p ≤ 1
⊢ 1 - ↑p = 0 → p = 1
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false.mpr
p : ℝ≥0
h : p ≤ 1
⊢ p = 1 → 1 - ↑p = 0

Tactic:
·

Goal state after:
case false.mpr
p : ℝ≥0
h : p ≤ 1
⊢ p = 1 → 1 - ↑p = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : (f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * 0)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : (f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * 0)
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case true
p : ℝ≥0
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
·

Goal state after:
case true
p : ℝ≥0
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω} (hm : m ≤ m₀) {μ : Measure Ω}
    [inst : IsFiniteMeasure μ] (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1),
    Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
⊢ Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]

pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]

Tactic:
·

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω} (hm : m ≤ m₀) {μ : Measure Ω}
    [inst : IsFiniteMeasure μ] (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1),
    Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
⊢ Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
hXmeas : AEMeasurable X 0
hX : ∀ᵐ (ω : Ω) ∂0, X ω = 0 ∨ X ω = 1
⊢ Var[X; 0] = Measure.real 0 {ω | X ω = 0} * Measure.real 0 {ω | X ω = 1}

pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hμ : IsProbabilityMeasure μ
⊢ Var[X; μ] = μ.real {ω | X ω = 0} * μ.real {ω | X ω = 1}

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : IsZeroOrProbabilityMeasure 0
hXmeas : AEMeasurable X 0
hX : ∀ᵐ (ω : Ω) ∂0, X ω = 0 ∨ X ω = 1
⊢ Var[X; 0] = Measure.real 0 {ω | X ω = 0} * Measure.real 0 {ω | X ω = 1}