!4#4490 Analysis.Matrix

Stream: mathlib4

[Jireh Loreaux]

I have fixed most of the errors in this file, but the remaining ones are super evil. This file adds a few normed structures as local instances on matrices using inferInstanceAs and then looking through some type equalities. This seems to cause major headaches because at times Lean chooses to see the wrong type, and then picks the wrong norm. As an example of what I mean:

import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Analysis.NormedSpace.PiLp
import Mathlib.Analysis.InnerProductSpace.PiL2

noncomputable section
open scoped BigOperators NNReal

variable {m n α : Type _} [Fintype m] [Fintype n]

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y) -- Porting note: See issue #2220

section linfty

/-- Seminormed group instance (using sup norm of L1 norm) for matrices over a seminormed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
def linftyOpSeminormedAddCommGroup [SeminormedAddCommGroup α] :
    SeminormedAddCommGroup (Matrix m n α) :=
  inferInstanceAs (SeminormedAddCommGroup (m → PiLp 1 fun _j : n => α))

variable [SeminormedAddCommGroup α]

example (A : Matrix m n α) : ‖A‖ = 0 := by
  /- with `set_option pp.explicit true`
  ⊢ @Eq ℝ
    (@norm (Matrix m n α)
      (@SeminormedAddCommGroup.toNorm (Matrix m n α) (@linftyOpSeminormedAddCommGroup m n α inst✝² inst✝¹ inst✝)) A)
    0
  -/
  have := Pi.norm_def A
  /- with `set_option pp.explicit true`
  this: @Eq ℝ
    (@norm (m → n → α)
      (@SeminormedAddGroup.toNorm (m → n → α)
        (@Pi.seminormedAddGroup m (fun i ↦ n → α) inst✝² fun i ↦
          @Pi.seminormedAddGroup n (fun a ↦ α) inst✝¹ fun i ↦ @SeminormedAddCommGroup.toSeminormedAddGroup α inst✝))
      A)
    ↑(@Finset.sup ℝ≥0 m instNNRealSemilatticeSup
        NNReal.instOrderBotNNRealToLEToPreorderToPartialOrderInstNNRealStrictOrderedSemiring (@Finset.univ m inst✝²)
        fun b ↦
        @nnnorm (n → α)
          (@SeminormedAddGroup.toNNNorm (n → α)
            (@Pi.seminormedAddGroup n (fun a ↦ α) inst✝¹ fun i ↦ @SeminormedAddCommGroup.toSeminormedAddGroup α inst✝))
          (A b))
  -/
  sorry

theorem linfty_op_norm_def (A : Matrix m n α) :
    ‖A‖ = ((Finset.univ : Finset m).sup fun i : m => ∑ j : n, ‖A i j‖₊ : ℝ≥0) := by
  -- in mathlib3, this worked: `simp [Pi.norm_def, PiLp.nnnorm_eq_sum ENNReal.one_ne_top]`
  sorry
  -- `rw [Pi.norm_def]` fails with: "synthesized type class instance is not definitionally equal
  -- to expression inferred by typing rules ..."

end linfty

end

I think this is just defeq abuse in Lean 3, but I'm not sure the best way to resolve it in Lean 4, especially because it was super convenient.

[Jireh Loreaux]

@Eric Wieser :up: because I expect you will care a lot about this and have ideas about its resolution.

[Eric Wieser]

I think this lemma is awkward because:

• We are using defeq abuse rather than using NormedAddCommGroup.induced with a map equal to the identity
• This lemma is doing two things at once; undoing the defeq abuse, and then applying a useful lemma

The first point seems pretty minor, since this is an implementation detail anyway. The solution to the second was to start the proof with a change line to express the norm without any defeq abuse.

[Eric Wieser]

(I pushed some fixes, but haven't reviewed the overall diff)

[Jireh Loreaux]

Thanks. I'll have a look in a bit.