More currying of continuous multilinear maps

Stream: Is there code for X?

[Anatole Dedecker]

Just to be sure, we don't have currying of docs#ContinuousMultilinearMap in the following form, right?

import Mathlib.Analysis.NormedSpace.Multilinear
import Mathlib.Analysis.NormedSpace.OperatorNorm

variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 E] [NormedSpace 𝕜 F]

set_option synthInstance.maxHeartbeats 50000 in
def foo {m n : ℕ} : (E [×m]→L[𝕜] (E [×n]→L[𝕜] F)) ≃ₗᵢ[𝕜] E [×(m+n)]→L[𝕜] F := sorry

[Anatole Dedecker]

(Yes, even the type causes the typclass system to go nuts. There is something fishy going on with continuous multilinear maps that I'm trying to minimize, I've been fighting with >2s TC synthesis of some CoeFun... -- although in this case it's Module that's taking some time)

[Yury G. Kudryashov]

We have docs#ContinuousMultilinearMap.currySumEquiv

[Yury G. Kudryashov]

Together with docs#ContinuousMultilinearMap.domDomCongrₗᵢ it should give what you want.

[Yury G. Kudryashov]

Scratch that, we have docs#ContinuousMultilinearMap.curryFinFinset

[Yury G. Kudryashov]

To get your version, just take s to be the first m elements of Fin (m + n).

[Anatole Dedecker]

Thanks!

[Yury G. Kudryashov]

I wonder if #2202 will help with CoeFun synth here and there.

[Yury G. Kudryashov]

But this is a big refactor.

[Anatole Dedecker]

Leaving the CoeFun example aside for the moment (I'll try to minimize it), I'd be interested if someone understand why the typeclass inference takes such a long time in this example. On my computer it ends up spending .8s to prove that two instances of AddMonoid are equal, which is very fishy.

[Anatole Dedecker]

But when I write the corresponding equality and try to prove it by rfl it takes "only" .2s

[Eric Wieser]

I think it has a lot of tower problems it has to solve, though I'm not sure

[Anatole Dedecker]

To be clear most of the time here is actually spent on defeq-checking, not typeclass synthesis. EDIT: that's a stupid comment, this is always what takes a long time...

[Yury G. Kudryashov]

Can we help the defeq checker somehow?

[Anatole Dedecker]

I'm wondering wether the fact that docs#ContinuousMultilinearMap.normedAddCommGroup is defined using docs#AddGroupNorm.toNormedAddCommGroup could be a problem

[Yury G. Kudryashov]

Why is this a problem?

[Anatole Dedecker]

I don't know :sweat_smile: I'm trying to guess why it has to unfold so much things to see that the two AddMonoid instances are equal.

[Yury G. Kudryashov]

Will it become faster if you explicitly override toAddCommGroup?

[Eric Wieser]

It would likely become faster if you did that inside GroupNorm.toNormedCommGroup

[Anatole Dedecker]

Yury G. Kudryashov said:

Will it become faster if you explicitly override toAddCommGroup?

Overriding toAddCommGroup itself does not have a significant impact, but overriding add, nsmul and zero do!

[Yury G. Kudryashov]

So, you force Lean to flatten the constructor.

[Eric Wieser]

That's the opposite of the behavior I would expect

[Eric Wieser]

Did you do this in GroupNorm.toNormedCommGroup or your instance?

[Anatole Dedecker]

I did that directly in docs#ContinuousMultilinearMap.normedAddCommGroup

[Yury G. Kudryashov]

Maybe, Lean has to unify this instance with some flat instance; then it's easier to do it if both instances are flat. I don't know how to verify this guess.

[Eric Wieser]

But there's no such thing as a flat instance

[Eric Wieser]

Only nested instances where the nested bits are also nested

[Eric Wieser]

Eric Wieser said:

It would likely become faster if you did that inside GroupNorm.toNormedCommGroup

Can you try this and see if it helps?