notation: sum with two indices

Stream: mathlib4

[Johan Commelin]

-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean:174
theorem Matrix.toLinearMapₛₗ₂'_apply (M : Matrix n m N₂) (x : n → R₁) (y : m → R₂) :
    -- porting note: we don't seem to have `∑ i j` as valid notation yet
    Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ M x y = ∑ i, ∑ j, σ₁ (x i) •  σ₂ (y j) • M i j := by
  rw [toLinearMapₛₗ₂', toMatrixₛₗ₂', LinearEquiv.coe_symm_mk, toLinearMap₂'Aux, mk₂'ₛₗ_apply]
  apply Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by
    rw [smul_comm]

(https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean#L174)

Does anybody know how to make the ∑ i j notation work?

[Aaron Liu]

Try ∑ (i) (j)?

[Eric Wieser]

Perhaps relevant:

import Mathlib

#check ∃ i j, i ≠ j -- ok
#check ⨆ i j, i ≠ j -- fails

[Eric Wieser]

I guess we can copy something from the elaborator for Exists?

[Eric Wieser]

@Kyle Miller, can notation3 be made to support explicitBinders ?

[Kyle Miller]

Fixing limitations in extendedBinders is on the radar.

mathlib4#7227 was an experiment awhile back, but I had reservations about it being so complicated. I think it might be flexible enough to accommodate all the Finset.sum elaboration features as part of a notation3-defined notation.

[Floris van Doorn]

Eric Wieser said:

Perhaps relevant:

import Mathlib

#check ∃ i j, i ≠ j -- ok
#check ⨆ i j, i ≠ j -- fails

cf. #mathlib4 > uniformize binders @ 💬

[Eric Wieser]

Can we ignore Finset.sum binders for now and at least make Union and iSup match Exists?

[Kyle Miller]

That's just a side comment about how flexible the binders in that PR are

[Kyle Miller]

Have you investigated why it is that Exists supports this yet? There are multiple distinct Exists syntaxes.

[Kyle Miller]

We're thinking about trying to regularize how binders work in core. If we can get to doing that, that might give a nice resolution to this problem.

[Kyle Miller]

If there's some acceptable enough hack that can be done to notation3 in the meantime, I'm happy to review the idea and the PR

[Kyle Miller]

Or maybe there's enough will to have mathlib take on the risk of the complexity of #7227?

[Johan Commelin]

@Kyle Miller what do you think the risks are?
Also, should we rename notation3 by now?

[Kevin Buzzard]

I think it's about time we removed all references to "3" and "4"