Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) : |x| ^ p ≤ (p / |t|) ^ p * max (Real.exp (t * x)) (Real.exp (-t * x)) := by

Mathlib declaration: ProbabilityTheory.rpow_abs_le_mul_max_exp
Held-out module: Mathlib.Probability.Moments.IntegrableExpMul
Banned modules (itself + downstream): 20
Reference proof premises (reachable / held-out): 12 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00018

Attempts

sample 0 · round 0Lean 3 syntax10.6 s model time

Proof

cases p with p_nonneg p_zero
case p_nonneg =>
  have hp_pos : 0 < p := by simp [hp, p_nonneg]
  have h1 : |x| ^ p ≤ (p / |t|) ^ p * Real.exp (t * x) :=
    by
      rw [Real.exp_add]
      rw [Real.exp_neg]
      rw [Real.exp_neg]
      rw [Real.exp_add]
      apply Real.exp_le_exp
      exact (Real.mul_le_mul_left (Real.exp (t * x)) (Real.exp (-t * x)) (Real.exp (t * x)))
      exact (Real.mul_le_mul_left (Real.exp (t * x)) (Real.exp (-t * x)) (Real.exp (t * x)))
  have h2 : |x| ^ p ≤ (p / |t|) ^ p * Real.exp (-t * x) :=
    by
      rw [Real.exp_add]
      rw [Real.exp_neg]
      rw [Real.exp_neg]
      rw [Real.exp_add]
      apply Real.exp_le_exp
      exact (Real.mul_le_mul_left (Real.exp (t * x)) (Real.exp (-t * x)) (Real.exp (-t * x)))
      exact (Real.mul_le_mul_left (Real.exp (t * x)) (Real.exp (-t * x)) (Real.exp (-t * x)))
  exact (Real.le_max h1 h2)
case p_zero =>
  contradiction

What Lean printed (this is all the model sees on repair)

4:16: error: unknown tactic
4:10: error: Invalid syntax for case analysis tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `p_nonneg`.

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

lemma rpow_abs_le_mul_max_exp (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) :
    |x| ^ p ≤ (p / |t|) ^ p * max (exp (t * x)) (exp (-t * x)) := by
  rcases lt_or_gt_of_ne ht with ht_neg | ht_pos
  · rw [abs_of_nonpos ht_neg.le, sup_comm]
    convert! rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])
    simp
  · rw [abs_of_nonneg ht_pos.le]
    exact rpow_abs_le_mul_max_exp_of_pos x hp ht_pos