Inequalities · medium

Statement, exactly as the model and Lean see it

theorem lg_target : StrictConcaveOn ℝ (Set.Ici 0) fun x => √x := by

Mathlib declaration: Real.strictConcaveOn_sqrt
Held-out module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 60 / 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.00017

Attempts

sample 0 · round 0Syntax error10.2 s model time

Proof

intro x y hxy
rw [lt_iff_le_and_lt, le_antisymm]
rcases hxy with (h1 : x ≤ y) (h2 : x < y)
have h3 : y ≥ 0 := Ici_subset_univ.2 h1
have h4 : x ≥ 0 := Ici_subset_univ.2 h1
have h5 : y > 0 := lt_iff_le_and_gt.2 h2
have h6 : x > 0 := lt_iff_le_and_gt.1 h2
have h7 : √y - √x < (√y - √x) * (y - x) / (2 * √x) :=
  mul_pos (sub_pos h2) (inv_pos (mul_pos (gt_zero_of_gt_zero h5) (gt_zero_of_gt_zero h6)))
rw [mul_div_assoc, div_mul_eq_mul_div] at h7
have h8 : (√y - √x) * (y - x) / (2 * √x) < √y - √x :=
  mul_div_lt_mul_div (sub_pos h2) (inv_pos (mul_pos (gt_zero_of_gt_zero h5) (gt_zero_of_gt_zero h6))) (lt_iff_le_and_lt.2 h7)
exact h8

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

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

⊢ StrictConcaveOn ℝ (Set.Ici 0) fun x => √x
6:31: error: unexpected token '('; expected command

Reference proof

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

lemma strictConcaveOn_sqrt : StrictConcaveOn ℝ (Set.Ici 0) (√· : ℝ → ℝ) := by
  rw [funext Real.sqrt_eq_rpow]
  exact strictConcaveOn_rpow (by positivity) (by linarith)