Lp norm of matrix with PiLp?

Stream: Is there code for X?

[fra guu]

I want to imitate what frobeniusSeminormedAddCommGroup does to get lpMatrixSeminormedAddCommGroup.

@[local instance]
def frobeniusSeminormedAddCommGroup [SeminormedAddCommGroup α] :
    SeminormedAddCommGroup (Matrix m n α) :=
  inferInstanceAs (SeminormedAddCommGroup (PiLp 2 fun _i : m => PiLp 2 fun _j : n => α))

import Mathlib.Analysis.Normed.Lp.PiLp

noncomputable section

open scoped ENNReal Matrix

variable {m n 𝕜 : Type*} (p : ℝ≥0∞)
variable [RCLike 𝕂] [Fintype m] [Fintype n]

-- @[local instance]
def lpMatrixSeminormedAddCommGroup [Fact (1 ≤ p)] [SeminormedAddCommGroup 𝕂] :
  SeminormedAddCommGroup (Matrix m n 𝕂) :=
  inferInstanceAs (SeminormedAddCommGroup (PiLp p fun _i : m => PiLp p fun _j : n => 𝕂))

end

Q1. But it would fail as below if not commented out @[local instance].

cannot find synthesization order for instance @lpMatrixSeminormedAddCommGroup with type
  {𝕂 : Type u_4} →
    {m : Type u_1} →
      {n : Type u_2} →
        (p : ℝ≥0∞) →
          [inst : Fintype m] →
            [inst : Fintype n] →
              [inst : Fact (1 ≤ p)] → [inst : SeminormedAddCommGroup 𝕂] → SeminormedAddCommGroup (Matrix m n 𝕂)
all remaining arguments have metavariables:
  Fact (1 ≤ ?p)Lean 4

Q2. Moreover, if I change the p value from 2 to 3, it fails to synthesize.

failed to synthesize
  SeminormedAddCommGroup (PiLp 3 fun _i ↦ PiLp 2 fun _j ↦ 𝕂)
use `set_option diagnostics true` to get diagnostic information

I have read the souce code of WithLp and PiLp but didn't get the answer. Maybe I'm missing some information or my usage is wrong?

[Eric Wieser]

Q1: This doesn't work because Matrix m n 𝕂 doesn't mention p

[Jireh Loreaux]

Q2: I bet you're missing a Fact (1 \le 3) instance.

[fra guu]

I tried to define an abbrev MatrixP with p in its parameter list and it works. But now I haven't seen all the troubles that come with doing so.

abbrev MatrixP (m n α : Type*) (_p : ℝ≥0∞) : Type _ := Matrix m n α

@[local instance]         -- it works now
def lpMatrixSeminormedAddCommGroup [Fact (1 ≤ p)] [SeminormedAddCommGroup 𝕂] :
  SeminormedAddCommGroup (MatrixP m n 𝕂 p) :=...

[Eric Wieser]

I'm a little surprised that abbrev works here, I would have expected you to need def.

[Jireh Loreaux]

You also don't want to use abbrev because when you put that instance on your synonym it will also put it on matrices.

[Eric Wieser]

Is that true? On Matrix, the lack of p will cause the instance to never be found, right?

[Jireh Loreaux]

Maybe? But @Frédéric Dupuis and I recently realized that abbrevs can work backward like this, which is kind of unfortunate. I guess it makes sense to some extent, but it meant we couldn't do something the way we wanted for exactly this reason; that is, we had to use an actual default transparency def for matrices instead of an abbrev.