-- 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:
case pos
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : p = 0
⊢ |x| ^ p ≤ (p / t) ^ p * (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]

Result:
case pos
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : p = 0
⊢ 0 ≤ t * x ∨ t * x ≤ 0

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

Tactic:
rw [neg_le]

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

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

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

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

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

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

Result:
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))

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

Tactic:
congr

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

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)

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

Tactic:
exact le_max_left _ _

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) ⊔ rexp (-t / p * x)

Tactic:
positivity

Result:
no goals

Proof state:
case neg
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Tactic:
have h_x_le c (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := le_inv_mul_exp x hc

Result:
case neg
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Proof state:
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

Tactic:
by_cases hp_zero : p = 0

Result:
case pos
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : p = 0
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

case neg
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))

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

Tactic:
field_simp

Result:
no goals

Proof state:
case neg
x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * 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

Result:
case neg
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)
⊢ |x| ^ p ≤ (p / t) ^ p * (rexp (t * x) ⊔ rexp (-t * x))