Theorems / mh_numb_7d6af5
Mathlib held-out
Number theory · medium
theorem lg_target {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun x => Φ ↑x) s := by- Mathlib declaration
- ZMod.LSeriesSummable_of_one_lt_re
- Held-out module
- Mathlib.NumberTheory.LSeries.ZMod
- Banned modules (itself + downstream)
- 5
- Reference proof premises (reachable / held-out)
- 6 / 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.00030
Attempts
- sample 0 · round 0Syntax error11.3 s model time
Proof intro N Φ s hs apply LSeriesSummable.of_abs_convergent apply abs_convergent_of_terminating_at_zero apply terminating_at_zero_of_terminating_at_zero' apply terminating_at_zero_of_terminating_at_zero'' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_terminating_at_zero''' apply terminating_at_zero_of_termin......
What Lean printed (this is all the model sees on repair) 55:40: error: unexpected token '...'; expected term
Reference proof
Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.
/-- If `Φ` is a periodic function, then the L-series of `Φ` converges for `1 < re s`. -/
lemma LSeriesSummable_of_one_lt_re (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < re s) :
LSeriesSummable (Φ ·) s := by
let c := max' _ <| univ_nonempty.image (norm ∘ Φ)
refine LSeriesSummable_of_bounded_of_one_lt_re (fun n _ ↦ le_max' _ _ ?_) (m := c) hs
exact mem_image_of_mem _ (mem_univ _)