awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : rexp (t * |X ω| + v * X ω) ≤ |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|
⊢ ‖rexp (t * |X ω| + v * X ω)‖ ≤ ‖rexp ((v + t) * X ω) + rexp ((v - t) * X ω)‖

Tactic:
simp only [norm_eq_abs, abs_exp]

Premises used: Real.norm_eq_abs, Real.abs_exp
-- 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)) μ
ω : Ω
⊢ 0 ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
positivity
-- 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)) μ
ω : Ω
rw : rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
| |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|

Tactic:
rw [abs_of_nonneg (by positivity)]

Premises used: abs_of_nonneg
-- 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_2 : rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
⊢ rexp (t * |X ω| + v * X ω) ≤ |rexp ((v + t) * X ω) + rexp ((v - t) * X ω)|

Tactic:
conv_rhs => rw [abs_of_nonneg (by positivity)]

Premises used: abs_of_nonneg
-- 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_2 : ∀ (h_nonneg : 0 ≤ X ω), rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
refine_2₁ : ∀ (h_nonpos : X ω ≤ 0), rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
rcases le_total 0 (X ω) with h_nonneg | h_nonpos

Premises used: le_total, OfNat.ofNat
-- 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)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
refine_2 : 0 ≤ rexp ((v - t) * X ω)
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
rw [abs_of_nonneg h_nonneg, ← add_mul, add_comm, le_add_iff_nonneg_right]

Premises used: add_mul, le_add_iff_nonneg_right, add_comm, abs_of_nonneg
-- 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)) μ
ω : Ω
h_nonneg : 0 ≤ X ω
⊢ 0 ≤ rexp ((v - t) * X ω)

Tactic:
positivity
-- 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)) μ
ω : Ω
h_nonpos : X ω ≤ 0
refine_2 : 0 ≤ rexp ((v + t) * X ω)
⊢ rexp (t * |X ω| + v * X ω) ≤ rexp ((v + t) * X ω) + rexp ((v - t) * X ω)

Tactic:
rw [abs_of_nonpos h_nonpos, mul_neg, mul_comm, ← mul_neg, mul_comm, ← add_mul, add_comm,
        ← sub_eq_add_neg, le_add_iff_nonneg_left]

Premises used: add_mul, sub_eq_add_neg, add_comm, abs_of_nonpos, mul_comm, le_add_iff_nonneg_left, mul_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)) μ
ω : Ω
h_nonpos : X ω ≤ 0
⊢ 0 ≤ rexp ((v + t) * X ω)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
refine_3 :
  ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + 0 * X ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ

Tactic:
have h := integrable_exp_mul_abs_add (t := t) (μ := μ) (X := X) (v := 0) ?_ ?_
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + 0 * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ

Tactic:
simpa using h
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ

Tactic:
simpa using ht_int_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ

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 ω)) μ
inl : ∀ (ht_nonneg : 0 ≤ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
inr : ∀ (ht_nonpos : t ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ

Tactic:
rcases le_total 0 t with ht_nonneg | ht_nonpos

Premises used: le_total, OfNat.ofNat
-- 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 ω)) μ
ht_nonneg : 0 ≤ t
inl : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ

Tactic:
simp_rw [abs_of_nonneg ht_nonneg]

Premises used: abs_of_nonneg
-- 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 ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
integrable_exp_mul_abs_add ht_int_pos ht_int_neg

Premises used: ProbabilityTheory.integrable_exp_mul_abs_add
-- 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 ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω| + v * X ω)) μ

Tactic:
exact integrable_exp_mul_abs_add ht_int_pos ht_int_neg

Premises used: ProbabilityTheory.integrable_exp_mul_abs_add
-- 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 ω)) μ
ht_nonpos : t ≤ 0
inr : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * |X ω| + v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω| + v * X ω)) μ

Tactic:
simp_rw [abs_of_nonpos ht_nonpos]

Premises used: abs_of_nonpos
-- 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 ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - -t) * X ω)) μ

Tactic:
simpa using ht_int_pos
-- 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 ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * |X ω| + v * X ω)) μ

Tactic:
exact integrable_exp_mul_abs_add ht_int_neg (by simpa using ht_int_pos)

Premises used: ProbabilityTheory.integrable_exp_mul_abs_add
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
inl : ∀ (ht_nonneg : 0 ≤ t), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
inr : ∀ (ht_nonpos : t ≤ 0), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ

Tactic:
rcases le_total 0 t with ht_nonneg | ht_nonpos

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
inl : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ

Tactic:
simp_rw [abs_of_nonneg ht_nonneg]

Premises used: abs_of_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ

Tactic:
integrable_exp_mul_abs ht_int_pos ht_int_neg

Premises used: ProbabilityTheory.integrable_exp_mul_abs
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonneg : 0 ≤ t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * |X ω|)) μ

Tactic:
exact integrable_exp_mul_abs ht_int_pos ht_int_neg

Premises used: ProbabilityTheory.integrable_exp_mul_abs
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
inr : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * |X ω|)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (|t| * |X ω|)) μ

Tactic:
simp_rw [abs_of_nonpos ht_nonpos]

Premises used: abs_of_nonpos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (- -t * X ω)) μ

Tactic:
simpa using ht_int_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
ht_nonpos : t ≤ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * |X ω|)) μ

Tactic:
exact integrable_exp_mul_abs ht_int_neg (by simpa using ht_int_pos)

Premises used: ProbabilityTheory.integrable_exp_mul_abs
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
pos : ∀ (hp_zero : p = 0), |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
neg : ∀ (hp_zero : ¬p = 0), |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
by_cases hp_zero : p = 0
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : p = 0
pos : 0 ≤ t * x ∨ t * x ≤ 0
⊢ |x| ^ p ≤ (p / t) ^ p * max (rexp (t * x)) (rexp (-t * x))

Tactic:
simp only [hp_zero, rpow_zero, zero_div, neg_mul, one_mul, le_sup_iff, one_le_exp_iff,
      Left.nonneg_neg_iff]

Premises used: Real.one_le_exp_iff, zero_div, Real.rpow_zero, le_sup_iff, neg_mul, one_mul, Left.nonneg_neg_iff
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : p = 0
⊢ 0 ≤ t * x ∨ t * x ≤ 0

Tactic:
le_total 0 (t * x)

Premises used: HMul.hMul, le_total, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : p = 0
⊢ 0 ≤ t * x ∨ t * x ≤ 0

Tactic:
exact le_total 0 (t * x)

Premises used: HMul.hMul, le_total, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
⊢ ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)

Tactic:
have h_x_le c (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := le_inv_mul_exp x hc
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
c : ℝ
hc : 0 < c
⊢ -x ≤ c⁻¹ * rexp (-c * x)

Tactic:
simpa using le_inv_mul_exp (-x) hc

Premises used: Real.le_inv_mul_exp, Neg.neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
⊢ ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)

Tactic:
have h_neg_x_le c (hc : 0 < c) : -x ≤ c⁻¹ * exp (-c * x) := by simpa using le_inv_mul_exp (-x) hc
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
⊢ |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

Tactic:
abs_le.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_le, And.intro
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
refine_1 : -(c⁻¹ * max (rexp (c * x)) (rexp (-c * x))) ≤ x
refine_2 : x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

Tactic:
refine abs_le.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_le, And.intro
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
refine_1 : -x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ -(c⁻¹ * max (rexp (c * x)) (rexp (-c * x))) ≤ x

Tactic:
rw [neg_le]

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

Tactic:
(h_neg_x_le c hc).trans ?_

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

Tactic:
refine (h_neg_x_le c hc).trans ?_

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

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

Tactic:
le_max_right _ _

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

Tactic:
exact le_max_right _ _

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

Tactic:
(h_x_le c hc).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
refine_2 : c⁻¹ * rexp (c * x) ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ x ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

Tactic:
refine (h_x_le c hc).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
c : ℝ
hc : 0 < c
refine_2 : rexp (c * x) ≤ max (rexp (c * x)) (rexp (-c * x))
⊢ c⁻¹ * rexp (c * x) ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

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

Tactic:
le_max_left _ _

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

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
⊢ ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))

Tactic:
have h_abs_le c (hc : 0 < c) : |x| ≤ c⁻¹ * max (exp (c * x)) (exp (-c * x)) := by
    refine abs_le.mpr ⟨?_, ?_⟩
    · rw [neg_le]
      refine (h_neg_x_le c hc).trans ?_
      gcongr
      exact le_max_right _ _
    · refine (h_x_le c hc).trans ?_
      gcongr
      exact le_max_left _ _
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
h₁ : |x| ≤ (t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))
⊢ |x| ^ p ≤ ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p

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

Tactic:
h_abs_le (t / p) (div_pos ht (hp.lt_of_ne' hp_zero))

Premises used: HDiv.hDiv, div_pos, LE.le.lt_of_ne'
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
h : -t / p = -(t / p)
⊢ |x| ≤ (t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))

Tactic:
convert! h_abs_le (t / p) (div_pos ht (hp.lt_of_ne' hp_zero)) using 5

Premises used: HDiv.hDiv, div_pos, LE.le.lt_of_ne'
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ) (hc : 0 < c), x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ) (hc : 0 < c), -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ) (hc : 0 < c), |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
h h₁ : -(t / p) = -(t / p)
⊢ -t / p = -(t / p)

Tactic:
rw [neg_div]

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

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

Tactic:
positivity