Type-ascript to a Euclidean space

Stream: Is there code for X?

[Yaël Dillies]

Because @Heather Macbeth is so reluctant to adding the "identity" euclidean_space 𝕜 n ≃ (n → 𝕜), I still don't know how to correctly type-ascript something to euclidean_space. How do people do it?

[Yaël Dillies]

Update: Adding it instantly solve my problem. Are you really that against it, Heather?

def to_euclidean_space {𝕜 n : Type*} [is_R_or_C 𝕜] [fintype n] :
  (n → 𝕜) ≃ euclidean_space 𝕜 n := equiv.refl _

[Heather Macbeth]

What's your use case? I usually use id.

[Yaël Dillies]

I have some x : fin n → ℕ and want to talk about its Euclidean norm as an element of euclidean_space ℝ (fin n) but writing down ∥(λ i : fin n, (x i : ℝ) : euclidean_space ℝ (fin n))∥ results in the wrong norm being picked up.

[Heather Macbeth]

Can you make x of type Euclidean space initially?

[Yaël Dillies]

No, unfortunately not, because I need it to be in my discrete fin n → ℕ for combinatorial reasons in the assumptions of the lemma.

[Heather Macbeth]

Hmm ... can you share the code?

[Yaël Dillies]

It might not be very workable right now but you can have a look at branch#behrend

[Yaël Dillies]

The relevant declaration is slice_norm.

[Eric Wieser]

FWIW, I'm in favor of such a definition since it seems to work out well for multiplicative, but 1) I haven't used this bit of the library much so Heather's opinion is worth more in context, and 2) we maybe want to bundle as much as the weakest case permits (more than an equiv), to save us writing to_euclidean_space_zero lemmas and similar. On the other hand, the advantage of writing such lemmas manually is they become available to dsimp.

[Yaël Dillies]

Yes, I took the weakest bundling because I didn't know which was the correct one, but we could surely go for the strongest generically true one.

[Heather Macbeth]

Looking at your use case, what you really want is to turn {x : fin n → ℕ} to Euclidean space. And this is a headache I've encountered with regular pi-types before. So maybe we should have

def euclidean_space.mk (𝕜 : Type*) [is_R_or_C 𝕜] {n : Type*} [fintype n] {α : Type*}
  (f : α → 𝕜) (v : n → α) :
  euclidean_space 𝕜 n :=
f ∘ v

[Heather Macbeth]

which allows you to write, in your use case,

lemma slice_norm {n d k : ℕ} {x : fin n → ℕ} (hx : x ∈ sphere_slice n d k) :
  ∥euclidean_space.mk ℝ coe x∥ = real.sqrt k :=

[Sebastien Gouezel]

Does id x : euclidean_space 𝕜 n work for you? It's the standard trick of inserting an id to make sure that Lean has no freedom to get it wrong.

[Eric Wieser]

What's the benefit of using id vs having a dedicated name?

[Eric Wieser]

As soon as you start simplifying, your id is going to vanish and your types are likely to stop making sense in the goal view

[Eric Wieser]

With a dedicated name you can control when it does and does not vanish

[Eric Wieser]

(probably you only want it to vanish for to_euclidean v i = v i, to_euclidean 0 = 0, etc)

[Eric Wieser]

A notation !ₑ[x, y, z] = to_euclidean ![x, y, z] might be a nice way to prevent it being too verbose in the goal view in some cases

[Sebastien Gouezel]

The point of id is that this trick is useful all over the place, and doesn't need any new API. I agree that a proper API around to_euclidean would be nicer, but if it is solving a problem that you can avoid with a simple trick like that I'm not sure it is worth investing manpower in it.

[Yaël Dillies]

This is a path to being sloppy in type-checking and letting the wrong norm slip in accidentally. id is a hack and should be treated as such. I am trying to manipulate some fin n → ℕ as terms of euclidean_space ℝ (fin n) and this is a mess. to_euclidean is an easy lasting solution. It requires 7 lemmas of API (cf docs#to_lex) and a correction of the existing lemmas, then it will just work.

[Eric Wieser]

It turns out we already have from_euclidean_space, it's docs#pi_Lp.equiv