Zulip Chat Archive

Stream: maths

Topic: compact unit ball


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 05 2019 at 02:57):

elaboration of test took 4.81s

view this post on Zulip Kenny Lau (Dec 05 2019 at 02:57):

why does this take so long??

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 02:57):

You have to say the magic words

view this post on Zulip Kenny Lau (Dec 05 2019 at 02:58):

ok that seems to fix the problem

view this post on Zulip Kenny Lau (Dec 05 2019 at 02:58):

why?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 03:00):

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

view this post on Zulip Kevin Buzzard (Dec 05 2019 at 03:02):

I tidied up ball_span_ash a bit.

view this post on Zulip Kenny Lau (Dec 05 2019 at 03:02):

what a coincidence, I'm also working on that

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 05 2019 at 03:08):

what does ash mean?

view this post on Zulip 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 :)

view this post on Zulip Johan Commelin (Dec 05 2019 at 08:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 05 2019 at 08:55):

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

view this post on Zulip Sebastien Gouezel (Dec 05 2019 at 09:04):

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

view this post on Zulip Johan Commelin (Dec 05 2019 at 09:06):

Ooh, sorry. You're completely right

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Lambert A'Campo (Dec 06 2019 at 00:47):

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

view this post on Zulip Kevin Buzzard (Dec 06 2019 at 00:47):

We need a tactic to generate the magic incantations!

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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