summable_geometric_of_norm_lt_1 works for ℝ yet fails for ℂ

Stream: maths

[Mark Gerads]

summable_geometric_of_norm_lt_1_Problem.lean
Using ℂ results in a type mismatch error. This seems like a bug to me.

[Ruben Van de Velde]

import analysis.specific_limits
import analysis.normed_space.basic
import analysis.complex.basic
import data.complex.basic

noncomputable theory

open topological_space normed_space
open_locale topological_space

namespace complex

instance : topological_space ℂ  := ⊥

/-- works -/
lemma works (r : ℝ) (h0 : ∥r∥ < 1) : summable (λ(n : ℕ),r^n) :=
summable_geometric_of_norm_lt_1 h0

/-- fails -/
lemma fails (r : ℂ) (h0 : ∥r∥ < 1) : summable (λ(n : ℕ),r^n) :=
summable_geometric_of_norm_lt_1 h0

end complex

[Ruben Van de Velde]

It works if you drop the instance

[Mark Gerads]

Huh. Thanks.

[Patrick Massot]

Mark, what did you have in mind when writing this instance line?

[Mark Gerads]

Originally, I added it to stop LEAN from complaining when I was declaring
lemma prob_neg1 (f : ℕ → ℂ) (r : ℂ) (h0 : abs r < 1) (h : ∀(k : ℕ), abs (f k) < abs (r^k)) : summable f :=
...
The word 'summable' was redlined and requested an instance which I provided. This seems to have been fixed by an import I added after that, I suspect 'import analysis.complex.basic' fixed it, but I don't know.

[Yury G. Kudryashov]

Indeed, the normed_space structure on complex is defined in analysis.complex.basic

[Reid Barton]

instance : topological_space ℂ := ⊥ basically means "give $\mathbb{C}$ the discrete topology", in which case the lemma fails makes sense but is false, of course, and it's not what you want.

[Yury G. Kudryashov]

OTOH, instance : topological_space ℂ := ⊤ would make this lemma trivial ;)

[Mark Gerads]

I copied and modified 'instance : topological_space ℤ := ⊥' without understanding what it meant.

[Kevin Buzzard]

Topological space structures on a type form a lattice, with the bottom one the discrete topology and the top one the indiscrete topology. Two topologies T1 and T2 satisfy T1<=T2 iff the identity map (X,T1) -> (X,T2) is continuous.