norm on continuous_multilinear_map

Stream: general

[Jireh Loreaux]

Can someone tell me why this complains that it failed to synthesize the typeclass instance for has_norm (continuous_multilinear_map ℂ (λ (i : fin n), ℂ) A)?

import analysis.complex.basic
import analysis.normed_space.multilinear

variables
{A : Type*} [normed_ring A] [normed_algebra ℂ A] [complete_space A]

example {n : ℕ} {p : ℂ [×n]→L[ℂ] A} : ℝ :=
∥p∥

because it seems to me that it is defined here docs#continuous_multilinear_map.has_op_norm

[Oliver Nash]

I only have a moment but I agree this looks like it should work and I note that the following works:

noncomputable example {n : ℕ} {p : ℂ [×n]→L[ℂ] A} : ℝ :=
begin
  haveI _inst := @continuous_multilinear_map.has_op_norm ℂ (fin n) (λ i, ℂ) A _ _ _ _ _ _ _,
  exact ∥p∥,
end

or even

noncomputable example {n : ℕ} {p : ℂ [×n]→L[ℂ] A} : ℝ :=
@has_norm.norm _ (@continuous_multilinear_map.has_op_norm ℂ (fin n) (λ i, ℂ) A _ _ _ _ _ _ _) p

[Oliver Nash]

I'll have time later this morning and look into it then if it's still pending.

[Eric Wieser]

Does

example : has_norm (ℂ [×n]→L[ℂ] A) :=
continuous_multilinear_map.has_op_norm

Work?

[Oliver Nash]

Good question, no it does not:

import analysis.complex.basic
import analysis.normed_space.multilinear

noncomputable theory

variables {A : Type*} [normed_ring A] [normed_algebra ℂ A] [complete_space A] {n : ℕ}

/- Works; cannot drop any of the provided arguments `ℂ`, `fin n`, or `(λ i, ℂ)`. -/
example : has_norm (ℂ [×n]→L[ℂ] A) :=
@continuous_multilinear_map.has_op_norm ℂ (fin n) (λ i, ℂ) _ _ _ _ _ _ _ _

/- Fails with:

type mismatch, term
  continuous_multilinear_map.has_op_norm
has type
  has_norm (continuous_multilinear_map ?m_1 ?m_3 ?m_4) : Type (max ? ? ?)
but is expected to have type
  has_norm (continuous_multilinear_map ℂ (λ (i : fin n), ℂ) A) : Type u_1
-/
example : has_norm (ℂ [×n]→L[ℂ] A) :=
continuous_multilinear_map.has_op_norm

[Oliver Nash]

I don't understand why this fails.

[Eric Wieser]

I think this is the standard "pi types confuse typeclass search" problem

[Eric Wieser]

I think it gets stuck trying to unify the typeclass arguments while trying to unify the non-typeclass arguments. Ideally it would not attempt to unify the typeclass arguments at all.

[Oliver Nash]

Thanks! I see (sort of). Do we have a note / thread / issue for this?

[Jireh Loreaux]

So, if I understand correctly, the problem is that Lean is having trouble constructing the pi type typeclass for the normed group instance associated to complex? Some sort of reference for this problem would be greatly appreciated.

[Eric Wieser]

I think there was a similar problem for dfinsupp that @Kevin Buzzard tracked down into a mwe, and that particular mwe was fixed in Lean 4.

[Kevin Buzzard]

Maybe lean4#509 ?

[Oliver Nash]

So there’s a good chance this issue is fixed in Lean 4 and we just work around it till then.