# Zulip Chat Archive

## Stream: maths

### Topic: compact unit ball

#### Kevin Buzzard (Dec 05 2019 at 00:49):

@Lambert A'Campo proved that A Normed Real Vector Space with Compact Unit Ball is Finite Dimensional. I forked the project and am trying to speed up compile time by fixing the import problems. But there are some far better speedrunners than me here. Are there better ways to formalise the statement of the theorem?

#### Kevin Buzzard (Dec 05 2019 at 01:59):

Sebastien's priority hack cuts the compile down on my machine from 16 seconds to under 1.5.

#### Kenny Lau (Dec 05 2019 at 02:57):

import analysis.normed_space.banach import analysis.normed_space.basic import linear_algebra.basic import linear_algebra.basis import linear_algebra.dimension import linear_algebra.finite_dimensional import topology.subset_properties import set_theory.cardinal import data.real.basic import topology.sequences import order.bounded_lattice import analysis.specific_limits import analysis.normed_space.finite_dimension noncomputable theory open_locale classical open metric set variables {V : Type} [normed_group V] [normed_space ℝ V] set_option profiler true def test (v : V) : V := (1 + ∥v∥)⁻¹ • v set_option profiler false

#### Kenny Lau (Dec 05 2019 at 02:57):

elaboration of test took 4.81s

#### Kenny Lau (Dec 05 2019 at 02:57):

why does this take so long??

#### Kevin Buzzard (Dec 05 2019 at 02:57):

You have to say the magic words

#### Kenny Lau (Dec 05 2019 at 02:58):

ok that seems to fix the problem

#### Kenny Lau (Dec 05 2019 at 02:58):

why?

#### Kevin Buzzard (Dec 05 2019 at 02:59):

the magic words

Type class inference just goes crazy trying to prove V is a normed field and 100 other things.

#### Kevin Buzzard (Dec 05 2019 at 03:00):

262144 characters of really stupid guesses about the type of V given that it has no `*`

#### Kevin Buzzard (Dec 05 2019 at 03:02):

I tidied up ball_span_ash a bit.

#### Kenny Lau (Dec 05 2019 at 03:02):

what a coincidence, I'm also working on that

#### Kenny Lau (Dec 05 2019 at 03:08):

lemma ball_span_ash {A : submodule ℝ V} (hyp : ∀ v : V, ∥v∥ ≤ 1 → v ∈ A) (v : V) : v ∈ A := have h1 : 0 < 1 + ∥v∥, from add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg v), have h2 : ∥(1 + ∥v∥)⁻¹ • v∥ ≤ 1, by rw [norm_smul, real.norm_eq_abs, abs_of_nonneg (le_of_lt $ inv_pos h1), ← mul_le_mul_left h1, ← mul_assoc, mul_inv_cancel (ne_of_gt h1), one_mul, mul_one]; exact le_add_of_nonneg_left zero_le_one, have h3 : (1 + ∥v∥) • (1 + ∥v∥)⁻¹ • v ∈ A, from A.smul_mem _ $ hyp _ h2, by rwa [smul_smul, mul_inv_cancel (ne_of_gt h1), one_smul] at h3

#### Kenny Lau (Dec 05 2019 at 03:08):

what does `ash`

mean?

#### Sebastien Gouezel (Dec 05 2019 at 08:26):

Are there better ways to formalise the statement of the theorem?

The conclusion should rather be that the space is finite-dimensional. And the assumption should not be that the field is the real numbers, but any nondiscrete normed field :)

#### Johan Commelin (Dec 05 2019 at 08:28):

Do you even need nondiscrete? :grimacing: :wink:

#### Sebastien Gouezel (Dec 05 2019 at 08:30):

Depends on which ball you're considering. If you assume that the ball of radius `1/2`

is compact, and in fact it is reduced to `0`

, then you can't deduce anything. The statement with the ball of radius `1`

is probably true in full generality.

#### Sebastien Gouezel (Dec 05 2019 at 08:49):

No, it's not true in fact. Take real numbers with the trivial norm equal to `1`

on all nonzero elements. This is a (discrete) normed field. Then take an infinite-dimensional real vector space with a norm equal to, say, 13, on every non-zero element. I think it satisfies all the axioms of a normed vector space. Then the closed ball of radius `1`

is compact, but the space is infinite-dimensional.

#### Johan Commelin (Dec 05 2019 at 08:55):

Don't the norm axioms require that `||1|| = 1`

?

#### Sebastien Gouezel (Dec 05 2019 at 09:04):

In the field, yes, but that's satisfied by my example. In the vector space, `1`

doesn't make sense.

#### Johan Commelin (Dec 05 2019 at 09:06):

Ooh, sorry. You're completely right

#### Kevin Buzzard (Dec 05 2019 at 17:15):

You need the norm on the field to be nontrivial and this should do it I guess

#### Lambert A'Campo (Dec 06 2019 at 00:47):

I have now generalised the proof to non discrete complete fields k. However @Sebastien Gouezel s priority magic doesn't work anymore so it's slow again. Also I'm now wondering whether there is a normed vector space over a non-complete field which contains a finite dimensional subspace that is not closed.

#### Lambert A'Campo (Dec 06 2019 at 00:47):

The code is here https://github.com/LAC1213/compact_unit_ball

#### Kevin Buzzard (Dec 06 2019 at 00:47):

We need a tactic to generate the magic incantations!

#### Sebastien Gouezel (Dec 06 2019 at 07:15):

If you don't assume completeness, you can still deduce it from the existence of a compact ball (unless the space is `0`

-dimensional, but then the result is obvious), as a ball in the field embeds isometrically in a ball in the space by the map `c -> c x`

(where `x`

is a fixed non-zero vector).

#### Sebastien Gouezel (Dec 06 2019 at 07:49):

And yes, if you drop completeness, finite-dimensional subspaces are generally not closed. A basic example is to consider `ℝ`

as a `ℚ`

vector space, but with its usual norm. Then the one-dimensional subspace `ℚ`

is not closed, as it is dense!

#### Sebastien Gouezel (Dec 06 2019 at 08:15):

With

local attribute [instance, priority 20000] nat.has_zero nat.has_one real.domain local attribute [instance, priority 10000] mul_action.to_has_scalar distrib_mul_action.to_mul_action semimodule.to_distrib_mul_action module.to_semimodule vector_space.to_module normed_space.to_vector_space ring.to_monoid normed_ring.to_ring normed_field.to_normed_ring add_group.to_add_monoid add_comm_group.to_add_group normed_group.to_add_comm_group ring.to_semiring add_comm_group.to_add_comm_monoid normed_field.to_discrete_field normed_field.to_has_norm nondiscrete_normed_field.to_normed_field zero_ne_one_class.to_has_zero zero_ne_one_class.to_has_one domain.to_zero_ne_one_class division_ring.to_domain field.to_division_ring discrete_field.to_field

all searches should be direct.

#### Patrick Massot (Dec 06 2019 at 09:20):

I just created https://github.com/LAC1213/compact_unit_ball/pull/1. I didn't think about the overall structure of the proof. I took the first lemmas and locally modified them using standard tricks.

#### Lambert A'Campo (Dec 06 2019 at 11:24):

Thank you Patrick, I'll learn from it!

Last updated: May 12 2021 at 08:14 UTC