Probability · hard

Statement, exactly as the model and Lean see it

theorem lg_target {p : ℕ → ℝ} {r : ℝ} (k : ℕ) (hr : Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r)) : Filter.Tendsto (fun n => ↑(n.choose k) * p n ^ k) Filter.atTop (nhds (r ^ k / ↑k.factorial)) := by

Mathlib declaration: ProbabilityTheory.tendsto_choose_mul_pow_atTop
Held-out module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 66 / 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.00020

Attempts

sample 0 · round 0Syntax error9.1 s model time

Proof

intro k hr
let f := fun n => ↑(n.choose k) * p n ^ k
let g := fun n => ↑n * p n
have h : Filter.Tendsto g Filter.atTop (nhds r) := hr
let m : ℕ → ℕ := fun n => n
let l : ℕ → ℕ := fun n => n
let a : ℕ → ℝ := fun n => ↑(n.choose k) / ↑k.factorial
let b : ℕ → ℝ := fun n => (p n ^ k) / (↑n ^ k)
have h1 : Filter.Tendsto (fun n => ↑(n.choose k) / ↑k.factorial) Filter.atTop (nhls (r^k / ↑k.factorial)) :=
  by apply tendsto_mul; [exact tendsto_const, exact tendsto_div' (tendsto_pow' (tendsto_const (nhns r)) k) (tendsto_const (nhns (↑k.factorial))) ]
have h2 : Filter.Tendsto (fun n => (p n ^ k) / (↑n ^ k)) Filter.atTop (nhns (r^k / ↑k.factorial)) :=
  by apply tendsto_div'; [exact tendsto_pow' (tendsto_const (nhns r)) k, exact tendsto_const (nhns (↑k.factorial)) ]
have h3 : Filter.Tendsto (fun n => ↑(n.choose k) * p n ^ k) Filter.atTop (nhns (r^k / ↑k.factorial)) :=
  by apply tendsto_mul; [exact h1, exact h2]
exact h3

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

5:36: error: failed to synthesize instance of type class
  HPow ℝ (Set ℝ) ?m.57

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
5:31: error: Application type mismatch: The argument
  k
has type
  Set ℝ
but is expected to have type
  ℕ
in the application
  n.choose k
3:208: error: unsolved goals
p : ℕ → ℝ
r : ℝ
k✝ : ℕ
hr✝ : Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r)
k : Set ℝ
hr : k ∈ nhds (r ^ k✝ / ↑k✝.factorial)
⊢ k ∈ Filter.map (fun n => ↑(n.choose k✝) * p n ^ k✝) Filter.atTop
13:26: 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 tendsto_choose_mul_pow_atTop (hr : Tendsto (fun n => n * p n) atTop (𝓝 r)) :
    Tendsto (fun n => n.choose k * (p n) ^ k) atTop (𝓝 (r ^ k / k.factorial)) := by
  have : (fun n => n.choose k * (p n) ^ k) ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
    calc
    _ ~[atTop] (fun n => (n ^ k / k.factorial) * (p n) ^ k) :=
      (isEquivalent_choose k).mul IsEquivalent.refl
    _ ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
      EventuallyEq.isEquivalent (.of_eq (by ext; field))
  refine (IsEquivalent.tendsto_nhds_iff this).mpr ?_
  simpa [div_eq_mul_inv] using (hr.pow k).mul_const ((k.factorial : ℝ)⁻¹)