Inequalities · medium

Statement, exactly as the model and Lean see it

theorem lg_target {ι : Type u_1} {f : ι → ℂ} (hf : Summable f) : Summable fun i => Complex.log (1 + f i) := by

Mathlib declaration: Complex.summable_log_one_add_of_summable
Held-out module: Mathlib.Analysis.SpecialFunctions.Log.Summable
Banned modules (itself + downstream): 16
Reference proof premises (reachable / held-out): 23 / 0

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.00007

Attempts

sample 0 · round 0Lean 3 syntax1.8 s model time

Proof

intro i,
rw Complex.log_def,
simp only [Complex.ofReal_add, Complex.ofReal_one],
have h : 0 < 1 + f i := by simp [add_pos zero_lt_one (real.pos_of_nonneg (re f i) (le_rfl))],
apply real.log_pos,
exact h

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

ι : Type u_1
f : ι → ℂ
hf : Summable f
⊢ Summable fun i => Complex.log (1 + f i)
4:9: 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 summable_log_one_add_of_summable {f : ι → ℂ} (hf : Summable f) :
    Summable (fun i ↦ log (1 + f i)) := by
  apply (hf.norm.mul_left (3 / 2)).of_norm_bounded_eventually
  filter_upwards [hf.norm.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi
    using norm_log_one_add_half_le_self hi