mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})

pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
⊢ -(c⁻¹ * max (rexp (c * x)) (rexp (-c * x))) ≤ x

pp: case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

Tactic:
·

Goal state after:
case refine_1
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
⊢ -(c⁻¹ * max (rexp (c * x)) (rexp (-c * x))) ≤ x
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

Tactic:
·

Goal state after:
case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
𝒢 : Filtration ι m
τ η : Ω → WithTop ι
i : ι
s : Set Ω
inst✝ : DecidablePred fun x ↦ x ∈ s
hτ_st : IsStoppingTime 𝒢 τ
hη_st : IsStoppingTime 𝒢 η
hτ : ∀ (ω : Ω), ↑i ≤ τ ω
hη : ∀ (ω : Ω), ↑i ≤ η ω
hs : MeasurableSet s
n : ι
this : {ω | s.piecewise τ η ω ≤ ↑n} = s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n}
hin : ¬i ≤ n
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑n} ∪ sᶜ ∩ {ω | η ω ≤ ↑n})
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case mpr
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n ↦ predictablePart f ℱ μ n ω) atTop atTop
⊢ Tendsto (fun n ↦ f n ω) atTop atTop

Tactic:
·

Goal state after:
case mpr
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n ↦ predictablePart f ℱ μ n ω) atTop atTop
⊢ Tendsto (fun n ↦ f n ω) atTop atTop
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process s n ω ≤ process s (n + 1) ω

pp: case refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
this :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ process s n ω) atTop atTop ↔ Tendsto (fun n ↦ predictablePart (process s) ℱ μ n ω) atTop atTop
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔
      Tendsto (fun n ↦ ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) atTop atTop

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ process s n ω ≤ process s (n + 1) ω
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ (t / p)⁻¹ = p / t

pp: case e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))

Tactic:
·

Goal state after:
case e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ (t / p)⁻¹ = p / t
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))

Tactic:
·

Goal state after:
case e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ max (rexp (t / p * x)) (rexp (-t / p * x)) ^ p = max (rexp (t * x)) (rexp (-t * x))
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (x : Ω), RCLike.re (↑(X x) ^ n * Complex.exp (↑t * ↑(X x))) ∂μ = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Integrable (fun ω ↦ ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω))) μ

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (x : Ω), RCLike.re (↑(X x) ^ n * Complex.exp (↑t * ↑(X x))) ∂μ = ∫ (ω : Ω), X ω ^ n * rexp (t * X ω) ∂μ
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Integrable (fun ω ↦ ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω))) μ

Tactic:
·

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t✝ : ℝ
ht : t✝ ∈ interior (integrableExpSet X μ)
n✝ n : ℕ
t : ℝ
ht' : t ∈ interior (integrableExpSet X μ)
⊢ Integrable (fun ω ↦ ↑(X ω) ^ n * Complex.exp (↑t * ↑(X ω))) μ
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ n * cexp (x * ↑(X ω))) μ

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) μ

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) μ

pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      ‖↑(X a) ^ (n + 1) * cexp (x * ↑(X a))‖ ≤ |X a| ^ (n + 1) * rexp (z.re * X a + t / 2 * |X a|)

pp: case refine_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

pp: case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (fun x ↦ ↑(X a) ^ n * cexp (x * ↑(X a))) (↑(X a) ^ (n + 1) * cexp (x * ↑(X a))) x

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ n * cexp (x * ↑(X ω))) μ
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e'_8
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝ : ℝ
⊢ mgf X μ x✝ = ∫ (x : Ω), (fun ω ↦ X ω ^ 0 * rexp (x✝ * X ω)) x ∂μ

pp: case e'_9
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝¹ x✝ : Ω
⊢ X x✝ = X x✝ ^ (0 + 1)

Tactic:
·

Goal state after:
case e'_8
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝ : ℝ
⊢ mgf X μ x✝ = ∫ (x : Ω), (fun ω ↦ X ω ^ 0 * rexp (x✝ * X ω)) x ∂μ
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case e'_9
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝¹ x✝ : Ω
⊢ X x✝ = X x✝ ^ (0 + 1)

Tactic:
·

Goal state after:
case e'_9
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ interior (integrableExpSet X μ)
x✝¹ x✝ : Ω
⊢ X x✝ = X x✝ ^ (0 + 1)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a.e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * p * p⁻¹ = t

Tactic:
rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

pp: case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
·

Goal state after:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e_a.e_a
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ t * p * p⁻¹ = t

Tactic:
rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) μ

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) μ

pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      ‖↑(X a) ^ (n + 1) * cexp (x * ↑(X a))‖ ≤ |X a| ^ (n + 1) * rexp (z.re * X a + t / 2 * |X a|)

pp: case refine_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

pp: case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (fun x ↦ ↑(X a) ^ n * cexp (x * ↑(X a))) (↑(X a) ^ (n + 1) * cexp (x * ↑(X a))) x

Tactic:
·

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

pp: case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
·

Goal state after:
case inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_neg : t < 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
hg : Integrable g ℙ
⊢ Integrable (fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
exact Integrable.comp_sub_right hg μ

Goal state after:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
·

Goal state after:
case inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
ht_pos : 0 < t
⊢ |x| ^ p ≤ (p / |t|) ^ p * max (rexp (t * x)) (rexp (-t * x))
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ 0 < |t|

pp: case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ (p / |t|) ^ p * max (rexp (|t| * x)) (rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)

Tactic:
·

Goal state after:
case refine_1
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ 0 < |t|
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ (p / |t|) ^ p * max (rexp (|t| * x)) (rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)

Tactic:
·

Goal state after:
case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ (p / |t|) ^ p * max (rexp (|t| * x)) (rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ AnalyticAt ℝ (cgf X μ) v
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)

pp: case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)

Tactic:
·

Goal state after:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) μ

pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      ‖↑(X a) ^ (n + 1) * cexp (x * ↑(X a))‖ ≤ |X a| ^ (n + 1) * rexp (z.re * X a + t / 2 * |X a|)

pp: case refine_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

pp: case refine_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (fun x ↦ ↑(X a) ^ n * cexp (x * ↑(X a))) (↑(X a) ^ (n + 1) * cexp (x * ↑(X a))) x

Tactic:
·

Goal state after:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) μ
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v