ContinuousMultilinearMap curry/uncurry

Stream: mathlib4

[A.]

Hi! It seems to me that the first two are currying but the third is uncurrying. Any thoughts?

import Mathlib.Analysis.NormedSpace.Multilinear.Curry

variable {n : ℕ} {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']

#check (continuousMultilinearCurryFin0 𝕜 G G' : (G [×0]→L[𝕜] G') →L[𝕜] G')

#check (continuousMultilinearCurryFin1 𝕜 G G' : (G [×1]→L[𝕜] G') →L[𝕜] (G →L[𝕜] G'))

#check (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) G :
  (E →L[𝕜] E [×n]→L[𝕜] G) →L[𝕜] (E [×(n + 1)]→L[𝕜] G))

[A.]

These are really LinearIsometryEquivs and in each case the name of the function given for the forward direction is a variant of uncurry. So, conversely, that function would seem to be correctly named in the third case only.

[A.]

@Sébastien Gouëzel

[Eric Wieser]

docs#continuousMultilinearCurryFin0,
docs#continuousMultilinearCurryFin1,
docs#continuousMultilinearCurryLeftEquiv

[Eric Wieser]

I think the names of those first two are correct, and it's the names of the functions used to implement them which are wrong

[Eric Wieser]

@loogle Equiv, "curry"

[loogle]

:search: Equiv.curry, Equiv.piCurry, and 24 more

[A.]

That’s what I said :grinning: I’m going to assume I can take that as agreement. Thanks Eric.

[A.]

#15530

[A.]

Something has gone wrong with the CI. What on earth does this mean?

build archive

packing Mathlib/Util/SynthesizeUsing.lean as f38776054285fbfc.ltar
uncaught exception: failure in curl #[--no-progress-meter, -H, x-ms-blob-type: BlockBlob, -H, If-None-Match: *, --retry, 5, -X, PUT, --parallel, -K, /home/lean/.cache/mathlib/curl.cfg]:
curl: (56) OpenSSL SSL_read: Connection reset by peer, errno 104
…
Attempting to upload 4945 file(s)
Error: Process completed with exit code 1.

[Kevin Buzzard]

I would just try running CI again

[Yury G. Kudryashov]

BTW, we have both curry0/uncurry0 and constOfIsEmpty, similarly for continuousMultilinearCurryFin1 and ofSubsingleton. Should we deduplicate here?

[Yury G. Kudryashov]

Also, I'm going to introduce curryMid based on Fin.insertNth/Fin.succAbove, because I need it for alternating forms.

[Yury G. Kudryashov]

CC: @Sébastien Gouëzel

[Sébastien Gouëzel]

Yes, deduplicating is definitely a good idea, and curryMid also!

[Yury G. Kudryashov]

Which definitions do you prefer to stay?

[Sébastien Gouëzel]

I don't really care. Maybe keep all names with curry in them for coherence?

[Yury G. Kudryashov]

Formally, constOfIsEmpty and ofSubsingleton are more general.

[Yury G. Kudryashov]

/me is going offline for at leat 8 hrs.

[Sébastien Gouëzel]

Then only keep the more general ones as definitions, and add aliases with curry in the name for ease of discoverability?