Rayleigh quotient of a matrix

Stream: new members

[Adrian Wüthrich]

I would like to use the Rayleigh quotient of a matrix in a theorem, I tried

variable (M : Matrix E' E' ℝ) [Fintype E'] [DecidableEq E']

#check ContinuousLinearMap.rayleighQuotient (LinearMap.toContinuousLinearMap (Matrix.toLin' M))

This raises the following error

application type mismatch
  ContinuousLinearMap.rayleighQuotient (LinearMap.toContinuousLinearMap (toLin' M))
argument
  LinearMap.toContinuousLinearMap (toLin' M)
has type
  @ContinuousLinearMap ℝ ℝ DivisionSemiring.toSemiring DivisionSemiring.toSemiring (RingHom.id ℝ) (E' → ℝ)
    Pi.topologicalSpace (@AddCommGroup.toAddCommMonoid (E' → ℝ) Pi.addCommGroup) (E' → ℝ) Pi.topologicalSpace
    (@AddCommGroup.toAddCommMonoid (E' → ℝ) Pi.addCommGroup) (Pi.module E' (fun a ↦ ℝ) ℝ)
    (Pi.module E' (fun a ↦ ℝ) ℝ) : Type u_5
but is expected to have type
  @ContinuousLinearMap ℝ ℝ DivisionSemiring.toSemiring DivisionSemiring.toSemiring (RingHom.id ℝ) (E' → ℝ)
    UniformSpace.toTopologicalSpace (@AddCommGroup.toAddCommMonoid (E' → ℝ) NormedAddCommGroup.toAddCommGroup) (E' → ℝ)
    UniformSpace.toTopologicalSpace (@AddCommGroup.toAddCommMonoid (E' → ℝ) NormedAddCommGroup.toAddCommGroup)
    NormedSpace.toModule NormedSpace.toModule : Type u_5

To find the issue I tried

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : E →L[ℝ] E)
variable {E' : Type*} [NormedAddCommGroup (E' → ℝ)] [InnerProductSpace ℝ (E' → ℝ)] (T' : (E' → ℝ) →L[ℝ] E' → ℝ)

#check ContinuousLinearMap.rayleighQuotient T --This works
#check ContinuousLinearMap.rayleighQuotient T' --This does not

which raises a similar error. How can this be when both E and E' → ℝ fulfill the same assumptions?

Thanks in advance for any help.

[Eric Wieser]

You want

#check ContinuousLinearMap.rayleighQuotient (Matrix.toEuclideanCLM (𝕜 := ℝ) M)

[Eric Wieser]

Your second code block is interesting but a distraction from the problem in your first one

[Eric Wieser]

Your first problem is caused by E' → ℝ not being an inner product space, because it has the wrong norm

[Eric Wieser]

Using docs#Matrix.toEuclideanCLM gives you the L2 norm, which is an inner product space

[Adrian Wüthrich]

Thanks a lot, it's working now. Just out of curiosity what could be the issue in the second block?

[Eric Wieser]

The issue in the second block is that NormedAddCommGroup (E' → ℝ) means "assume some random normed structure on the type of vectors", but Mathlib already has an existing norm structure (the sup-norm) that is not apriori equal to this one

[Adrian Wüthrich]

Thank you for clarifying

[Adrian Wüthrich]

I have a question which I think relates to the same issue. I want to get the orthogonal complement of a vector E → ℝ, this is what I tried:

variable {E : Type*} [Fintype E] [InnerProductSpace ℝ (E → ℝ)] [Fintype (E → ℝ)]

#check (ℝ ∙ (fun _ ↦ 1 : E → ℝ))ᗮ

which raises the error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  Pi.module E (fun x ↦ ℝ) ℝ
inferred
  NormedSpace.toModule

What I understan is that Submodule.orthogonal implicitly infers InnerProductSpace. In this case it tries to build the inner product space using the sup norm which of course doesn't work. Now when i define the variable [InnerProductSpace ℝ (E → ℝ)] , its norm might not agree with the NormedAddCommGroup implicitly infered. I would like lean to use the L2 norm and InnerProductSpace ℝ (EuclideanSpace ℝ (E → ℝ)) instead. How do I tell lean to do so?

[Eric Wieser]

You want

#check (ℝ ∙ ((WithLp.equiv 2 _).symm <| fun _ ↦ 1 : E → ℝ))ᗮ

You have fun _ ↦ 1 : E → ℝ, but you want a term of type EuclideanSpace ℝ E, which WithLp.equiv 2 _ converts to

[Eric Wieser]

You should never write [InnerProductSpace ℝ (E → ℝ)], because this conflicts with the norm that mathlib already equips functions with

[Eric Wieser]

Note that [Fintype (E → ℝ)] is false unless IsEmpty E

[Adrian Wüthrich]

Wow, thank you for the instant response. [Fintype (E → ℝ)] is silly , I put that there without thinking trying to fix things.

[Eric Wieser]

Generally speaking, if lean says it can't find an instance for something involving a concrete type (like ℝ), adding [...] is the wrong fix

[Eric Wieser]

A better strategy in that case is to try adding

instance : InnerProductSpace ℝ (E → ℝ) := sorry

and see if you can fill the sorry

[Eric Wieser]

(in this case you'd find it impossible, because the inner product induces the wrong norm)

[Adrian Wüthrich]

Got it, i'll try that in the future.