mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : X ω ≤ 0
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)

Tactic:
·

Goal state after:
case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
ω : Ω
h : X ω ≤ 0
⊢ rexp (t * X ω) ≤ rexp (a * X ω) + rexp (b * X ω)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω ↦ rexp (-|u| * X ω)) μ

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t

pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω ↦ rexp (-|u| * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω ↦ rexp (-|u| * X ω)) μ

pp: case refine_1.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (-|u| * X ω)) μ

Tactic:
·

Goal state after:
case refine_1.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω ↦ rexp (-|u| * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (-|u| * X ω)) μ

Tactic:
·

Goal state after:
case refine_1.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (-|u| * X ω)) μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ τ ω = ↑i

pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ¬↑n ≤ τ ω

Tactic:
·

Goal state after:
case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ τ ω = ↑i
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t

pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|

Tactic:
·

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ¬↑n ≤ τ ω

Tactic:
·

Goal state after:
case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ¬↑n ≤ τ ω
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

pp: case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

Tactic:
·

Goal state after:
case refine_2.inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : 0 ≤ u
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ

Tactic:
·

Goal state after:
case refine_2.inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
hu : u ≤ 0
⊢ Integrable (fun ω ↦ rexp (|u| * X ω)) μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ i ∈ {i ∈ s | i < n}

pp: case inr.h₀
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ∀ b ∈ {i ∈ s | i < n}, b ≠ i → {ω | τ ω = ↑b}.indicator (u b) ω = 0

Tactic:
·

Goal state after:
case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ i ∈ {i ∈ s | i < n}
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t

pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|

Tactic:
·

Goal state after:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ -|u| ≤ t
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h₀
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ∀ b ∈ {i ∈ s | i < n}, b ≠ i → {ω | τ ω = ↑b}.indicator (u b) ω = 0

Tactic:
·

Goal state after:
case inr.h₀
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ∀ b ∈ {i ∈ s | i < n}, b ≠ i → {ω | τ ω = ↑b}.indicator (u b) ω = 0
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|

Tactic:
·

Goal state after:
case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
hu_int_pos : Integrable (fun ω ↦ rexp (u * X ω)) μ
hu_int_neg : Integrable (fun ω ↦ rexp (-u * X ω)) μ
htu : |t| ≤ |u|
⊢ t ≤ |u|
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)

pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Tactic:
·

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
⊢ log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : t₂ < t₁
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
·

Goal state after:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : t₂ < t₁
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Tactic:
·

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (fun ω ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t

pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a • t₁ + b • t₂

pp: case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ≤ t₂

Tactic:
·

Goal state after:
case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a • t₁ + b • t₂
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ≤ t₂

Tactic:
·

Goal state after:
case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ≤ t₂
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ = rexp (-t * ε) * mgf X μ t

Tactic:
by rw [neg_mul, exp_neg]; rfl

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω ↦ rexp (u * X ω)) μ
hv_int : Integrable (fun ω ↦ rexp (v * X ω)) μ
hu : u = 0
⊢ AEMeasurable X μ

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω ↦ rexp (u * X ω)) μ
hv_int : Integrable (fun ω ↦ rexp (v * X ω)) μ
hu : ¬u = 0
⊢ AEMeasurable X μ

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω ↦ rexp (u * X ω)) μ
hv_int : Integrable (fun ω ↦ rexp (v * X ω)) μ
hu : u = 0
⊢ AEMeasurable X μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω ↦ rexp (u * X ω)) μ
hv_int : Integrable (fun ω ↦ rexp (v * X ω)) μ
hu : ¬u = 0
⊢ AEMeasurable X μ

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω ↦ rexp (u * X ω)) μ
hv_int : Integrable (fun ω ↦ rexp (v * X ω)) μ
hu : ¬u = 0
⊢ AEMeasurable X μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)

Tactic:
refine Eq.trans_le ?_ (measure_ge_le_exp_mul_mgf (-ε) (neg_nonneg.mpr ht) ?_)

Goal state after:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} = μ.real {ω | -ε ≤ (-X) ω}

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (-t * (-X) ω)) μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} = μ.real {ω | -ε ≤ (-X) ω}

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (-t * (-X) ω)) μ

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ μ.real {ω | X ω ≤ ε} = μ.real {ω | -ε ≤ (-X) ω}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (-t * (-X) ω)) μ

Tactic:
·

Goal state after:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (-t * (-X) ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ω : Ω
⊢ ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : t = 0
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : t = 0
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case neg.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ

pp: case neg.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t ≠ v - t

Tactic:
·

Goal state after:
case neg.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * |X ω| + v * X ω)) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case neg.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t ≠ v - t

Tactic:
·

Goal state after:
case neg.refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_int_add : Integrable (fun a ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ
ht : ¬t = 0
⊢ v + t ≠ v - t