timeout at 'whnf'

Stream: mathlib4

[Alex Nekrasov]

Hello, everyone!
I'm currently trying to prove some basic facts about conditional convergence and I'm currently stuck with some error.

import Mathlib
set_option maxHeartbeats 500000

open Classical BigOperators Topology Filter Nat Finset Metric Real ENNReal NNReal

def CondConvergesTo [AddCommMonoid α] [TopologicalSpace α] (f : ℕ → α) (a : α) : Prop :=
  Tendsto (fun s => ∑ i in range s, f i) atTop (𝓝 a)

def HasCondSum [AddCommMonoid α] [TopologicalSpace α] (f : ℕ → α) : Prop :=
  ∃ a, CondConvergesTo f a

theorem epsilon_def [NormedAddCommGroup α] {f : ℕ → α} {b : α} :
    CondConvergesTo f b ↔ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ n, N ≤ n → ‖(fun s => (∑ i in range s, f i)) n - b‖ < ε := by
  let g := fun s => ∑ i in range s, f i
  have hg : g = (fun s => ∑ i in range s, f i) := by exact rfl
  rw [← hg]
  exact NormedAddCommGroup.tendsto_atTop

theorem  cauchy_criterion [NormedAddCommGroup α] [TopologicalSpace α] [Ring α] [IsAbsoluteValue (norm : α → ℝ)] [CauSeq.IsComplete α norm] {f : ℕ → α} :
    HasCondSum f ↔ IsCauSeq norm (fun s => (∑ i in range s, f i)) := by
  simp_rw [HasCondSum]
  rw [IsCauSeq]
  constructor
  · intro ⟨a, ha⟩
    have hb := epsilon_def.1 ha

Last line in this code (which is where I'm currently trying to make progress) gives this error:
(deterministic) timeout at 'whnf', maximum number of heartbeats (500000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Am I doing anything wrong?

[Patrick Massot]

Lean is probably utterly confused by your [NormedAddCommGroup α] [Ring α] combination which endows αwith two totally unrelated additions.

[Patrick Massot]

Or maybe it is utterly confused by your [NormedAddCommGroup α] [TopologicalSpace α] combination which endows αwith two totally unrelated topologies.

[Alex Nekrasov]

Oh, thanks! Turns out it was both. Replacing this three instances with [NormedRing α] fixed everything.

[Patrick Massot]

We should probably make the warning on top of Mathlib/Data/Real/CauSeq.lean even more frightening. Something like: this is not the file you want to use if you are not refactoring our construction of real or p-adic numbers.

[Patrick Massot]

I am pretty sure you wanted to state and prove:

theorem  cauchy_criterion [NormedAddCommGroup α] [CompleteSpace α] {f : ℕ → α} :
    HasCondSum f ↔ CauchySeq (fun s ↦ ∑ i in range s, f i)

[Patrick Massot]

And I am pretty sure this is already in Mathlib (but still a nice exercise if your want to learn).

[Alex Nekrasov]

I looked at CauchySeq and it looked a little bit scary. CauSeq seemed more similar to what I had learned at university. That's why I decided to prove this statement.
Also I couldn't find many theorems that used series convergence instead of Summable. None of them used CauchySeq or CauSeq.

[Yakov Pechersky]

https://www.moogle.ai/search/raw?q=a%20cauchy%20sequence%20over%20the%20naturals%20is%20one%20in%20which%20above%20a%20threshold%2C%20the%20norm%20is%20less%20than%20epsilon
docs#cauchySeq_bdd

[Yakov Pechersky]

which brought me to docs#cauchySeq_iff_le_tendsto_0, docs#Metric.cauchySeq_iff also