compact unit ball

Stream: maths

[Kevin Buzzard]

@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]

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

[Kenny Lau]

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]

elaboration of test took 4.81s

[Kenny Lau]

why does this take so long??

[Kevin Buzzard]

You have to say the magic words

[Kenny Lau]

ok that seems to fix the problem

[Kenny Lau]

why?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I tidied up ball_span_ash a bit.

[Kenny Lau]

what a coincidence, I'm also working on that

[Kenny Lau]

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]

what does ash mean?

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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]

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]

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

[Sebastien Gouezel]

In the field, yes, but that's satisfied by my example. In the vector space, 1doesn't make sense.

[Johan Commelin]

Ooh, sorry. You're completely right

[Kevin Buzzard]

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

[Lambert A'Campo]

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]

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

[Kevin Buzzard]

We need a tactic to generate the magic incantations!

[Sebastien Gouezel]

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]

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]

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]

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]

Thank you Patrick, I'll learn from it!