Norm Problem

Stream: new members

[Wenjie Huang]

Who can help me?
How to prove that the norm of a matrix power is less than or equal to the power of the matrix norm？
Thanks for any guidance!

import Mathlib


variable {n : ℕ}
variable [NormedAddCommGroup (Fin n → ℝ)] [NormedSpace ℝ (Fin n → ℝ)]
variable [NormedRing (Matrix (Fin n) (Fin n) ℝ)] [NormedAlgebra ℝ (Matrix (Fin n) (Fin n) ℝ)]
variable [NormOneClass (Matrix (Fin n) (Fin n) ℝ)]

example  {M : (Matrix (Fin n) (Fin n) ℝ)} (k : ℕ) : ‖M ^ k‖ ≤ ‖M‖ ^ k := by
  apply norm_pow_le M k -- why it fails?
  /- failed to synthesize
  NormOneClass (Matrix (Fin n) (Fin n) ℝ)
  -/

[Eric Wieser]

Which norm do you want?

[Wenjie Huang]

I want this to hold true for the matrix norm.

[Eric Wieser]

What you've written above says "let Fin n → ℝ have an arbitrary meaning of + that isn't the natural one".

[Wenjie Huang]

sorry, I'll delete this condition. I want this for arbitrary matrix norm.

import Mathlib


variable {n : ℕ}
variable [NormedRing (Matrix (Fin n) (Fin n) ℝ)] [NormedAlgebra ℝ (Matrix (Fin n) (Fin n) ℝ)]
variable [NormOneClass (Matrix (Fin n) (Fin n) ℝ)]

example  {M : (Matrix (Fin n) (Fin n) ℝ)} (k : ℕ) : ‖M ^ k‖ ≤ ‖M‖ ^ k := by
  apply norm_pow_le M k -- why it fails?
  /- failed to synthesize
  NormOneClass (Matrix (Fin n) (Fin n) ℝ)
  -/

[Eric Wieser]

[NormedRing (Matrix (Fin n) (Fin n) ℝ)] says "let matrices have an arbitrary meaning of * and +", unfortunately

[Wenjie Huang]

How can I modify this? I want the matrix to maintain its usual ring structure

[Eric Wieser]

There is currently no existing way to say "let this existing ring have an arbitrary compatible norm"

[Eric Wieser]

If you're happy to pick a particular matrix norm, then you can make things work

[Eric Wieser]

docs#Matrix.linftyOpNormedRing is one such norm

[Wenjie Huang]

Thanks for your help.
I really need a conclusion that holds for any norm, because I want to prove some conclusions about the convergence of matrix sequences. Is there really no way?

[Kenny Lau]

hmm is there a possible argument to be made to unmix norm and ring?

[Kenny Lau]

will we ever need to talk about two norms at the same time?

[Kenny Lau]

or i guess in this case, two matrix norms (since WithLp wouldnt work on matrix)

[Kenny Lau]

Wenjie Huang said:

Thanks for your help.
I really need a conclusion that holds for any norm, because I want to prove some conclusions about the convergence of matrix sequences. Is there really no way?

you can instead prove that in any normed ring, ||x^k|| <= ||x||^k.

[Kenny Lau]

it has nothing to do with matrixes

[Wenjie Huang]

Yes, I also want to separate the matrix ring and the norm, but our proof of the convergence of the matrix sequence requires the properties of both the matrix and the norm. This is a small part of it, which has nothing to do with the specifics of the matrix, but the whole needs

[Kenny Lau]

then why cant you just use the default norm

[Wenjie Huang]

I want this proof holds universally for any norm, thereby avoiding the need for repeated derivations across different norm specifications.

[Kenny Lau]

but we will only ever have one matrix norm

[Kenny Lau]

also, could you tell us what is the actual result you want to prove?

[Kenny Lau]

convergence kind of requires completeness

[Kenny Lau]

and if you’re complete, then any norms are equivalent right

[Wenjie Huang]

I want to prove that the spectral radius of a matrix is less than or equal to any norm of the matrix

[Kenny Lau]

could you be more specific about “any norm”?

[Wenjie Huang]

What I want to prove is that the matrix norm is compatible with the matrix ring.

[Aaron Liu]

Can't you just arbitrarily scale the norm to be smaller than the spectral radius?

[Aaron Liu]

If it really is "any" norm

[Kenny Lau]

can you define the “norm”s in your sentence?

[Kenny Lau]

can you make a statement in maths without using the word norm?

[Wenjie Huang]

These is the proposition I want to prove,
image.png

[Aaron Liu]

That looks like it's referring to some particular norm which was defined earlier

[Kenny Lau]

without the word norm

[Wenjie Huang]

image.png
It's all definition about norm.

[Kenny Lau]

seems like 2 is the key point

[Kenny Lau]

in current mathlib there is no way to talk about an arbitrary compatible norm i’m afraid

[Kenny Lau]

could you explain why we might want different matrix norms?

[Wenjie Huang]

Oh, so we have to pick a specific norm

[Kenny Lau]

it’s not impossible to make a new typeclass of compatible norms

[Kenny Lau]

@Yakov Pechersky has done excellent work in the valuation library, (but it’s not about norm)

[Wenjie Huang]

I am currently working on the formalization of numerical algebra and have encountered many problems related to norms.

[Kenny Lau]

@Wenjie Huang if you really feel like this is the right thing to do, i would suggest you to define a new typeclass

[Kenny Lau]

or a new structure

[Kenny Lau]

i don’t have a computer right now

[Wenjie Huang]

OK, I'll try it and thank you for your suggestions

[Kenny Lau]

so the pseudocode looks like

structure Norm’ (k) [NormedField k] (E) [Module k E] where
  norm : E -> R
  axioms…

[Kenny Lau]

refer to how NormedSpace does it, but make it a structure instead of class

[Wenjie Huang]

Ok , I'll refer to it

[Kenny Lau]

which book is this?

[Wenjie Huang]

I am trying to formalize many classic theorems in numerical linear algebra, using the textbook

[Eric Wieser]

We already have a similar structure as docs#Seminorm

[Eric Wieser]

docs#AlgebraNorm ?

[Eric Wieser]

That looks like what you want

[Wenjie Huang]

OK, I'll try it

[Kenny Lau]

what is the name of the book?

[Wenjie Huang]

This is a Chinese textbook called Numerical Linear Algebra
image.pnghttps://img9.doubanio.com/view/subject/l/public/s24944214.jpg

[Wenjie Huang]

So is something like this?

import Mathlib

theorem lemma_1
    {n : Type*} [Fintype n] [DecidableEq n]
    (A : Matrix n n ℂ) (p : AlgebraNorm ℂ (Matrix n n ℂ)) :
    (spectralRadius ℂ A).toReal ≤ p A := by
  sorry

[Yiming Fu]

Why don't we have AlgebraNorm.toNormedAlgebra, simliar to docs#RingNorm.toNormedRing.

[Eric Wieser]

That looks like a mistake to me

[Eric Wieser]

I think we should have that, PR welcome

[Jireh Loreaux]

But as someone mentioned in the other thread, these also need the forgetful inheritance versions that replace the topology, uniformity or bornology.

[Eric Wieser]

Or rather, the ones that don't replace it and use an existing instance

[Jireh Loreaux]

indeed, what I mean was: allow the user to replace the default inherited topology with the pre-existing one.

[Kenny Lau]

can we have both a canonical instance but also allow for other compatible norms?

[Kenny Lau]

this is exactly the kind of issues we ran into in local class field theory

[Kenny Lau]

(yes, there are other solutions, but I think I would be happiest with this approach instead)

[Jireh Loreaux]

I'm not sure what you mean. You want a Norm as an instance, but you also want access to other norms? You need type synonyms for the other norms. Or else you need to use something like docs#Seminorm which isn't a class.

[Kenny Lau]

i'm talking about adding onto the existing mathlib structure

[Jireh Loreaux]

Adding what onto the existing structure?

[Kenny Lau]

axiom ℝ : Type

structure Norm (X : Type) : Type where
  toFun : X → ℝ

axiom supNorm (n : Nat) : Norm (Fin n → ℝ)

noncomputable instance {n} : Inhabited (Norm (Fin n → ℝ)) where
  default := supNorm n

class CompleteSpace (X : Type) (norm : Norm X := by exact default) : Prop where
  exists_limit_of_cauchy : 1 + 1 = 2

axiom L2Norm (n : Nat) : Norm (Fin n → ℝ)

instance complete_supNorm (n) : CompleteSpace (Fin n → ℝ) := sorry
instance complete_L2Norm (n) : CompleteSpace (Fin n → ℝ) (L2Norm n) := sorry

#print complete_supNorm
#print complete_L2Norm

[Jireh Loreaux]

I still don't understand what you want to do by looking at this code.

1. CompleteSpace is about uniformities, not norms exactly.
2. In your example, the uniformities induced by these norms are provably equal
3. You can still have type synonyms
4. In fact, we do have the type synonym docs#WithLp (or docs#PiLp, or docs#EuclideanSpace), and moreover, these type synonyms have been constructed with the explicit intent to make the uniformities not just provably equal, but definitionally equal.

[Jireh Loreaux]

So CompleteSpace (EuclideanSpace 𝕜 n) is either already in Mathlib, or else trivial to prove.

[Robert Maxton]

It definitely would be a shame to have to commit to a specific norm; one of the cool/useful/surprising properties of matrix norms is that it almost never matters which one you pick

[Kenny Lau]

@Jireh Loreaux I want to allow other norms on the same type without introducing type synonyms.

[Jireh Loreaux]

But what does it even mean to allow other norms? What do you want to do with them exactly? And why doesn't a type synonym (or a local instance) suffice?

[Jireh Loreaux]

I'm not sure if this would address your desires, but potentially, we could have a predicate on docs#Seminorm called Seminorm.IsCompatible saying that the uniformity induced by a given seminorm is equal to the existing uniformity.

[Jireh Loreaux]

Robert Maxton said:

it almost never matters which one you pick

I beg to differ. I would argue that this is only applicable if you all you care about is properties generically true in Banach algebras.

[Yakov Pechersky]

Possible API:

import Mathlib

open Uniformity

variable {X : Type*}

def PseudoMetricSpace.isEquiv (f g : PseudoMetricSpace X) : Prop :=
  f.toUniformSpace = g.toUniformSpace

lemma PseudoMetricSpace.isEquiv.eq_uniformity {f g : PseudoMetricSpace X}
      (h : f.isEquiv g) :
    𝓤[f.toUniformSpace] = 𝓤[g.toUniformSpace] := sorry

lemma PseudoMetricSpace.isEquiv.eq_topology {f g : PseudoMetricSpace X} (h : f.isEquiv g) :
    f.toUniformSpace.toTopologicalSpace = g.toUniformSpace.toTopologicalSpace := sorry

lemma PseudoMetricSpace.isEquiv.of_normedField {f g : NormedField X} {c C : NNReal}
    (h : ∀ x : X, c * f.norm x ≤ g.norm x ∧ g.norm x ≤ C * f.norm x) :
    f.isEquiv g.toPseudoMetricSpace := sorry

lemma PseudoMetricSpace.isEquiv.of_normedField_rpow {f g : NormedField X} {α : NNReal} (hα : α < 1)
    (h : ∀ x : X, (f.norm x) ^ α.toReal = g.norm x) :
    f.isEquiv g.toPseudoMetricSpace := sorry

[Yakov Pechersky]

A possible application (if I understand correctly): one has an extension L/K of nonarch local fields, and wants to emply docs#spectralNorm_unique_field_norm_ext. It's not obvious that the preexisting norm instance is such that the hypothesis ∀ (x : K), f ((algebraMap K L) x) = ‖x‖ holds true. However, by equivalence of norms over normed fields, there is another norm where that will be true, under some power scaling α. So getting that α allows one to construct the desired topological hom from K to L.

[Bhavik Mehta]

Kenny Lau said:

Jireh Loreaux I want to allow other norms on the same type without introducing type synonyms.

In https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Matrix.html we have three different norms on Matrix (with no type synonyms)

[Eric Wieser]

That file needs some design work; my goal at the time was just to show that we had the machinery to build those instances

[Eric Wieser]

At minimum we should scope each collection of instances to make it easier to enable them all at once

[Eric Wieser]

Type synonyms are a little annoying because matrix notation like transpose is tied to Matrix.transpose and not a notation class.

[Jireh Loreaux]

Definitely they should be scoped instances.

[Jireh Loreaux]

Indeed, I'm familiar with the pain of type synonyms on docs#Matrix (see, for instance, docs#CStarMatrix). @Frédéric Dupuis suggested to me privately the possibility of a MatrixLike type class. At the time I dismissed it thinking there wouldn't be sufficient shared API, but perhaps this was stupid.

[Jireh Loreaux]

But as for @Kenny Lau 's problems, I'm still not sure exactly what they are. I want a concrete example of something he wants to do, but is obstructed, or otherwise unjustifiably hindered, because he can't work with multiple norms simultaneously.

Something that comes to my mind: it's quite inconvenient (without resorting to type synonyms) to say that all norms on a (fixed) finite dimensional space are equivalent. I mean, sure, you can say docs#LinearEquiv.toContinuousLinearEquiv, but that has not much content when you want E = F but possibly different norms and you consider docs#LinearEquiv.refl .

[Kenny Lau]

@Jireh Loreaux it's what Yakov pointed out. In the setting of local fields, there's an arbitrary norm on K and L (which yes, you can solve with attribute [-instance], but that also removes the uniform structure etc.), and you can't prove that L is a normed vector space over K because their norms don't exactly agree

[Eric Wieser]

Jireh Loreaux said:

Definitely they should be scoped instances.

#27855