Construct $\mathbb{R}^n$ and 1, infinity norms in it.

Stream: Is there code for X?

[Miguel Marco]

I keep creating examples for my general topology course, and I am stuck in an exercise that consists on proving that $\mathbb{R}^n$ is a metric space with the norms 1 and infinity, but i haven't found a way to define them.

So my first problem is how to define $\mathbb{R}^n$. One way is could think of is

(range n) → ℝ

with the norm 1 defined as

λ u v,  ∑ i, | u  i - v i|

but then even to prove that it is nonnegative by induction, I get stuck in the zero step because I cannot even prove (in a way that my students would find similar to what we do when we prove by hand) that

∑ (i : ↥(range 0)), |u i - v i| ≥ 0

.

I also tried the approach of defining $\mathbb{R}^n$ as

(fin n) → ℝ

and then the zero step works fine, but i cannot convert the sum over (fin n.succ) to a sum involving a sum along fin n.

And finally, another problem i am finding is to define the infinity norm, that involves a max instead of a sum.

Is there a smart (and simple) way to define such things that looks moreless like what undergrad students would expect?.

[Alex J. Best]

We would normally use fin n → ℝ for this indeed. And while it is possible to manage things involving fin (n+1) it is not very nice and I don't think it would look natural to your undergrads. If you really want to prove that a finite sum of nonnegative terms is nonnegative I'd do that as a separate lemma first (which could be proved by induction on the size of the sum, but working within a fixed general type, rather than some fin n).

[Eric Wieser]

I think you'll need to use

structure With1Norm (n : ℕ) where
  coords : Fin n → ℝ

Otherwise you will have to fight against the fact that mathlib already puts a different norm on $ℝ^n$

[Eric Wieser]

This of course means you have to show a bunch of stupid results that this is a vector space structure (inherited from $ℝ^n$)

[Miguel Marco]

How does mathlib define $\mathbb{R}^n$?

[Ruben Van de Velde]

Fin n -> Real

[Eric Wieser]

Mathlib puts the ∞-norm on Fin n → ℝ by default

[Eric Wieser]

If you want the 1-norm, you can use WithLp 1 (Fin n → ℝ) instead; but I assume the point of the exercise is to build this from scratch, rather than get everything for free!

[Eric Rodriguez]

There's also EuclideanSpace as a type synonym

[Miguel Marco]

Eric Wieser said:

If you want the 1-norm, you can use WithLp 1 (Fin n → ℝ) instead; but I assume the point of the exercise is to build this from scratch, rather than get everything for free!

Yes, exactly, but i will take a look at how WithLp is implemented. If it is reasonably similar to the "by hand" approach thet we do in class, i might try to mimic it.

Edit: I just took a quick look, and I think i can forget about that idea, since the Mathlib approach for Lp spaces uses measure theory, which is beyond the scope of my course.

I guess I will just leave that kind of exercises out of the short lean demos in the course.

[Eric Wieser]

I think you're misreading things; there are multiple Lps in mathlib, but docs#WithLp uses no measure theory

[Eric Wieser]

Ah, specifically docs#PiLp is what you want

[Eric Wieser]

src#PiLp.hasNorm defines the norm

[Eric Wieser]

src#PiLp.hasNorm defines the norm

[Eric Wieser]

Perhaps for your example, you should import WithLp, but build PiLp yourself?

[Jireh Loreaux]

One thing to note: in mathlib we take some care to ensure the topology (and uniform space and bornology) generated by the Lp norm coincides with the one generated by the infinity norm, and this is a step you can simply omit from the version you present to your class.