Theorems / mh_numb_485b85
Mathlib held-out
Number theory · hard
theorem lg_target {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E] [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] (f : C(ℤ_[p], E)) : Filter.Tendsto (fun x => (fwdDiff 1)^[x] (⇑f) 0) Filter.atTop (nhds 0) := by- Mathlib declaration
- PadicInt.fwdDiff_tendsto_zero
- Held-out module
- Mathlib.NumberTheory.Padics.MahlerBasis
- Banned modules (itself + downstream)
- 2
- Reference proof premises (reachable / held-out)
- 56 / 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.00029
Attempts
- sample 0 · round 0Lean 3 syntax14.4 s model time
Proof intro x, rw [functor.pow_apply, fwdDiff_pow], simp only [functor.pow_zero, nat.cast_zero, zero_add, add_zero], apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact Filter.atTop_ne_bot, apply tendsto_const, exact......
What Lean printed (this is all the model sees on repair) 3:254: error: unsolved goals p : ℕ hp : Fact (Nat.Prime p) E : Type u_1 inst✝³ : NormedAddCommGroup E inst✝² : Module ℤ_[p] E inst✝¹ : IsBoundedSMul ℤ_[p] E inst✝ : IsUltrametricDist E f : C(ℤ_[p], E) x : Set E ⊢ x ∈ nhds 0 → x ∈ Filter.map (fun x => (fwdDiff 1)^[x] (⇑f) 0) Filter.atTop 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.
/-- Key lemma for Mahler's theorem: for `f` a continuous function on `ℤ_[p]`, the sequence
`n ↦ Δ^[n] f 0` tends to 0. See `PadicInt.fwdDiff_iter_le_of_forall_le` for an explicit
estimate of the decay rate. -/
lemma fwdDiff_tendsto_zero (f : C(ℤ_[p], E)) : Tendsto (Δ_[1]^[·] f 0) atTop (𝓝 0) := by
-- first extract an `s`
refine NormedAddGroup.tendsto_nhds_zero.mpr (fun ε hε ↦ ?_)
have : Tendsto (fun s ↦ ‖f‖ / p ^ s) _ _ := tendsto_const_nhds.div_atTop
(tendsto_pow_atTop_atTop_of_one_lt (mod_cast hp.out.one_lt))
obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists
refine .mp ?_ (.of_forall fun x hx ↦ lt_of_le_of_lt hx hs)
-- use uniform continuity to find `t`
obtain ⟨t, ht⟩ : ∃ t : ℕ, ∀ x y, ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s := by
rcases eq_or_ne f 0 with rfl | hf
· -- silly case : f = 0
simp
have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)
obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this
obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos
exact ⟨t, fun x y hxy ↦ by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩
filter_upwards [eventually_ge_atTop (s * p ^ t)] with m hm
simpa only [Nat.sub_add_cancel hm] using fwdDiff_iter_le_of_forall_le ht (m - s * p ^ t)