-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- Auxiliary lemma for `rpow_abs_le_mul_max_exp`. -/
lemma rpow_abs_le_mul_max_exp_of_pos (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : 0 < t) :
    |x| ^ p ≤ (p / t) ^ p * max (exp (t * x)) (exp (- t * x))

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ |x| ≤ (t / p)⁻¹ * (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

Result:
case h.e'_4.h.e'_6.h.e'_4.h.e'_1.h.e'_5
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ -t / p = -(t / p)

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ 0 ≤ rexp (t / p * x)

Tactic:
positivity

Result:
no goals

Proof state:
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⁻¹ * rexp (-c * x) ≤ c⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))

Tactic:
gcongr

Result:
case refine_1.h
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
⊢ rexp (-c * x) ≤ rexp (c * x) ⊔ rexp (-c * x)

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ rexp (t / p * x * p) ⊔ rexp (-t / p * x * p) = rexp (t * x) ⊔ rexp (-t * x)

Tactic:
ring_nf

Result:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ rexp (t * p * p⁻¹ * x) ⊔ rexp (-(t * p * p⁻¹ * x)) = rexp (t * x) ⊔ rexp (-(t * x))

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ ((t / p)⁻¹ * (rexp (t / p * x) ⊔ rexp (-t / p * x))) ^ p = (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Tactic:
rw [mul_rpow (by positivity) (by positivity)]

Result:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ (t / p)⁻¹ ^ p * (rexp (t / p * x) ⊔ rexp (-t / p * x)) ^ p = (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Proof state:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 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

Result:
no goals

Proof state:
case pos
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)

Result:
no goals

Proof state:
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
⊢ c⁻¹ * rexp (c * x) ≤ c⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))

Tactic:
gcongr

Result:
case refine_2.h
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
⊢ rexp (c * x) ≤ rexp (c * x) ⊔ rexp (-c * x)

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ 0 ≤ (t / p)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ rexp (t * p * p⁻¹ * x) ⊔ rexp (-(t * p * p⁻¹ * x)) = rexp (t * x) ⊔ rexp (-(t * x))

Tactic:
congr <;> rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]

Result:
no goals

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ 0 ≤ rexp (-t / p * x)

Tactic:
positivity

Result:
no goals

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ (rexp (t / p * x) ⊔ rexp (-t / p * x)) ^ p = rexp (t * x) ⊔ rexp (-t * x)

Tactic:
rw [rpow_max (by positivity) (by positivity) hp, ← exp_mul, ← exp_mul]

Result:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ rexp (t / p * x * p) ⊔ rexp (-t / p * x * p) = rexp (t * x) ⊔ rexp (-t * x)

Proof state:
case h.e'_4.h.e'_6.h.e'_4.h.e'_1.h.e'_5
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ -t / p = -(t / p)

Tactic:
rw [neg_div]

Result:
no goals

Proof state:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ |x| ^ p ≤ ((t / p)⁻¹ * (rexp (t / p * x) ⊔ rexp (-t / p * x))) ^ p

Tactic:
refine rpow_le_rpow (abs_nonneg _) ?_ hp

Result:
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⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))
⊢ |x| ≤ (t / p)⁻¹ * (rexp (t / p * x) ⊔ rexp (-t / p * x))

Proof state:
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
⊢ -x ≤ c⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))

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

Result:
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⁻¹ * rexp (-c * x) ≤ c⁻¹ * (rexp (c * x) ⊔ rexp (-c * x))

Proof state:
case refine_1.h
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
⊢ rexp (-c * x) ≤ rexp (c * x) ⊔ rexp (-c * x)

Tactic:
exact le_max_right _ _

Result:
no goals