awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
calc exp (t * X ω)
      _ ≤ exp (a * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonpos_right hat h)
      _ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_right (exp_nonneg _)

Premises used: Iff.mpr, mul_le_mul_of_nonpos_right, HMul.hMul, Real.exp, Real.exp_le_exp, le_add_of_nonneg_right, Real.exp_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 (t * X ω)) μ

Tactic:
integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_

Premises used: ProbabilityTheory.integrable_exp_mul_of_le_of_le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
refine_3 : -|u| ≤ t
refine_4 : t ≤ |u|
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
refine integrable_exp_mul_of_le_of_le (a := -|u|) (b := |u|) ?_ ?_ ?_ ?_

Premises used: ProbabilityTheory.integrable_exp_mul_of_le_of_le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|
refine_1 : ∀ (hu : 0 ≤ u), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
refine_1₁ : ∀ (hu : u ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ

Tactic:
rcases le_total 0 u with hu | hu

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
refine_1 refine_1₁ refine_1₂ refine_1₃ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-|u| * X ω)) μ

Tactic:
rwa [abs_of_nonneg hu]

Premises used: abs_of_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
simpa [abs_of_nonpos hu]

Premises used: abs_of_nonpos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|
refine_2 : ∀ (hu : 0 ≤ u), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
refine_2₁ : ∀ (hu : u ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ

Tactic:
rcases le_total 0 u with hu | hu

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
refine_2 refine_2₁ refine_2₂ refine_2₃ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ

Tactic:
rwa [abs_of_nonneg hu]

Premises used: abs_of_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
refine_2 refine_2₁ refine_2₂ refine_2₃ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-u * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|u| * X ω)) μ

Tactic:
rwa [abs_of_nonpos hu]

Premises used: abs_of_nonpos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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|
refine_3 : -t ≤ |u|
⊢ -|u| ≤ t

Tactic:
rw [neg_le]

Premises used: neg_le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
(neg_le_abs t).trans htu

Premises used: neg_le_abs, LE.le.trans
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
exact (neg_le_abs t).trans htu

Premises used: neg_le_abs, LE.le.trans
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
(le_abs_self t).trans htu

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
exact (le_abs_self t).trans htu

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
inst : IsFiniteMeasure μ
hu : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
h_nonneg : 0 ≤ t
htu : t ≤ u
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (0 * X ω)) μ

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
inst : IsFiniteMeasure μ
hu : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
h_nonpos : t ≤ 0
htu : u ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (0 * X ω)) μ

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
h : t ∈ integrableExpSet X μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
h

Premises used: Set.Mem, setOf, MeasureTheory.Integrable, ProbabilityTheory.integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
inr :
  ∀
    (this :
      ∀ {Ω : 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 μ)
    (h_le : t₂ < t₁), a • t₁ + b • t₂ ∈ integrableExpSet X μ
wlog! :
  ∀ {Ω : 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 μ
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
wlog! h_le : t₁ ≤ t₂
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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₁ : ℝ⦄ (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 μ
h_le : t₂ < t₁
inr :
  ∀ (hab : b + a = 1)
    (this :
      ∀ {Ω : 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 μ)
    (h_le : t₂ < t₁), b • t₂ + a • t₁ ∈ integrableExpSet X μ
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
rw [add_comm] at hab ⊢

Premises used: add_comm
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 : b + a = 1
this :
  ∀ {Ω : 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 μ
h_le : t₂ < t₁
⊢ b • t₂ + a • t₁ ∈ integrableExpSet X μ

Tactic:
this ht₂ ht₁ hb ha hab h_le.le

Premises used: Set.Mem, LT.lt.le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 : b + a = 1
this :
  ∀ {Ω : 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 μ
h_le : t₂ < t₁
⊢ b • t₂ + a • t₁ ∈ integrableExpSet X μ

Tactic:
exact this ht₂ ht₁ hb ha hab h_le.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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:
integrable_exp_mul_of_le_of_le ht₁ ht₂ ?_ ?_

Premises used: Set.Mem, setOf, MeasureTheory.Integrable, ProbabilityTheory.integrableExpSet, ProbabilityTheory.integrable_exp_mul_of_le_of_le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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₂
refine_1 : t₁ ≤ a • t₁ + b • t₂
refine_2 : a • t₁ + b • t₂ ≤ t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
refine integrable_exp_mul_of_le_of_le ht₁ ht₂ ?_ ?_

Premises used: ProbabilityTheory.integrable_exp_mul_of_le_of_le
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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₂
rw : t₁ = (a + b) * t₁
rw₁ : t₁ = 1 * t₁
rw₂ rw₃ : t₁ = t₁
⊢ t₁ = a * t₁ + b * t₁

Tactic:
rw [← add_mul, hab, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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₂
bc : 0 ≤ b
⊢ a * t₁ + b * t₁ ≤ a * t₁ + b * t₂

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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₂
calc : t₁ = a * t₁ + b * t₁
calc₁ : a * t₁ + b * t₁ ≤ a * t₁ + b * t₂
⊢ t₁ ≤ a * t₁ + b * t₂

Tactic:
calc t₁
    _ = a * t₁ + b * t₁ := by rw [← add_mul, hab, one_mul]
    _ ≤ a * t₁ + b * t₂ := by gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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₂
bc : 0 ≤ a
⊢ a * t₁ + b * t₂ ≤ a * t₂ + b * t₂

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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₂
rw : (a + b) * t₂ = t₂
rw₁ : 1 * t₂ = t₂
rw₂ rw₃ : t₂ = t₂
⊢ a * t₂ + b * t₂ = t₂

Tactic:
rw [← add_mul, hab, one_mul]

Premises used: add_mul, one_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω_1 : Type u_1
m_1 : MeasurableSpace Ω_1
X_1 : Ω_1 → ℝ
μ_1 : Measure Ω_1
Ω : 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₂
calc : a * t₁ + b * t₂ ≤ a * t₂ + b * t₂
calc₁ : a * t₂ + b * t₂ = t₂
⊢ a * t₁ + b * t₂ ≤ t₂

Tactic:
calc a * t₁ + b * t₂
    _ ≤ a * t₂ + b * t₂ := by gcongr
    _ = t₂ := by rw [← add_mul, hab, one_mul]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
pos : ∀ (hu : u = 0), AEMeasurable X μ
neg : ∀ (hu : ¬u = 0), AEMeasurable X μ
⊢ AEMeasurable X μ

Tactic:
by_cases hu : u = 0
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
⊢ v ≠ 0

Tactic:
have hv : v ≠ 0 := ne_of_ne_of_eq huv.symm hu
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
hv : v ≠ 0
⊢ AEMeasurable X μ

Tactic:
aemeasurable_of_aemeasurable_exp_mul hv hv_int.aemeasurable

Premises used: MeasureTheory.Integrable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
hv : v ≠ 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hv hv_int.aemeasurable

Premises used: MeasureTheory.Integrable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
aemeasurable_of_aemeasurable_exp_mul hu hu_int.aemeasurable

Premises used: MeasureTheory.Integrable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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:
exact aemeasurable_of_aemeasurable_exp_mul hu hu_int.aemeasurable

Premises used: MeasureTheory.Integrable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v - t) * X a)) μ

Tactic:
simpa using ht_int_neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ rexp ((v + t) * X a) + rexp ((v - t) * X a)) μ

Tactic:
have h_int_add : Integrable (fun a ↦ exp ((v + t) * X a) + exp ((v - t) * X a)) μ :=
    ht_int_pos.add <| by simpa using ht_int_neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
Integrable.mono h_int_add ?_ (ae_of_all _ fun ω ↦ ?_)

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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)) μ
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
refine_2 : ∀ (ω : Ω), ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
refine Integrable.mono h_int_add ?_ (ae_of_all _ fun ω ↦ ?_)

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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)) μ
pos : ∀ (ht : t = 0), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
neg : ∀ (ht : ¬t = 0), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
by_cases ht : t = 0
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
pos :
  ∀ (ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
simp only [ht, zero_mul, zero_add, add_zero] at ht_int_pos ⊢

Premises used: MulZeroClass.zero_mul, zero_add, add_zero
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
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
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ

Tactic:
ht_int_pos.1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
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
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (v * X ω)) μ

Tactic:
exact ht_int_pos.1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
neg : ∀ (hX : AEMeasurable X μ), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
neg₁ : v + t ≠ v - t
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ ht_int_pos ht_int_neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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 ω)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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
neg : v + t - (v - t) ≠ 0
⊢ v + t ≠ v - t

Tactic:
rw [← sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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) ≠ 0

Tactic:
simp [ht]