Duality principle

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Do we have the duality principle for Hilbert operators in Mathlib? I may be missing it, but I can’t find it under an obvious name. Here is what I mean. Here is what I mean.

Let $V$, $W$ be Hilbert spaces, and let $A : V \to W$ be a bounded linear operator. Then the operator norms of $A$ and its adjoint coincide:

$$\|A\| = \|A^*\|.$$

This is extremely useful in analytic number theory -- in particular, it underlies an entire family of proofs for the large sieve in different forms, to the point that some call it "the principle of the large sieve". For most applications in number theory, the finite-dimensional case suffices, but one doesn't need any assumption of finite-dimensionality in the proof.

Has the duality principle been stated and proved in Lean? The basic language necessary for the task does seem to be there - I'm finding something called "ContinuousLinearMap.norm_def", for instance.

For the sake of convenience, I’m attaching a screenshot from a draft of my book where the lemma is stated and proved, preceded by some definitions, all in a few lines.
image.png

[Aaron Liu]

is it docs#innerSL_apply_norm

[Aaron Liu]

is it docs#ContinuousLinearMap.adjoint

[Aaron Liu]

which is bundled as a star-linear isometry equiv

[Harald Helfgott]

That's the adjoint I mean, yes. The point is that the operator norm of the adjoint of an operator equals the operator norm of the operator itself.

[Aaron Liu]

docs#norm_map

[Aaron Liu]

because the type of ContinuousLinearMap.adjoint is star-linear isometry equiv, and all linear isometries preserve the norm

[Harald Helfgott]

Is norm_map saying that the adjoint operator is an isometry, yes or no?

[Aaron Liu]

no, norm_map says isometries which preserve zero preserve the norm

[Aaron Liu]

ContinuousLinearMap.adjoint is defined as a star-linear isometry equiv

[Aaron Liu]

so in particular it's automatically an isometry which preserves zero

[Harald Helfgott]

Right, then norm_map is not the statement we want. But are you saying that the statement is hidden in a type, because the adjoint map is defined as an isometry?

[Aaron Liu]

yes

[Aaron Liu]

close enough

[Aaron Liu]

if you have some Lean code I can fill in a sorry

[Harald Helfgott]

Ah, interesting. Sounds elegant, but I wish there were a way to highlight this. Wait, is this close enough or do we really have this? Or do you mean that we ought to have a Lean statement saying exactly the same as the Lemma I posted, and that the proof would be a line or so - the Lemma would be a convenient wrapper for something that already exists?

[Aaron Liu]

this probably doesn't deserve its own lemma

[Aaron Liu]

but it sounds like you were having trouble proving it so I offered to help if you have some code

[Aaron Liu]

we do already have this it's a zero line proof

[Harald Helfgott]

I wasn't having trouble proving it (to be sincere: I was about to give a blueprint to Aristotle). I was just surprised that it didn't seem to be there. I do think it deserves to be easily findable by people who know it as "the duality principle". So, sure, a lemma with a zero-line proof and a telling name would be nice.

[Harald Helfgott]

Thanks.

[Aaron Liu]

oh no we're missing instances

[Aaron Liu]

so the proof I have doesn't work

[Harald Helfgott]

But you can give a simple proof (even simpler than what I pasted) given what is there, right? Well, I guess that does mean the statement deserves its own Lemma :)

[Aaron Liu]

well it didn't end up being zero lines I guess

import Mathlib.Analysis.InnerProductSpace.Adjoint

variable {𝕜 E F : Type*} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F]
  [CompleteSpace E] [CompleteSpace F]

lemma ContinuousLinearMap.norm_adjoint (A : E →L[𝕜] F) : ‖A.adjoint‖ = ‖A‖ :=
  -- can't use `_root_.norm_map` here because of missing instances
  SemilinearIsometryClass.norm_map _ A

[Aaron Liu]

the mathematical content of the proof is in docs#ContinuousLinearMap.adjointAux_norm

[Harald Helfgott]

OK - thanks. I think it would be a service to everybody if this were included in Mathlib - I know it's just a wrapper, but it's now more transparent and immediately applicable.

[Edward van de Meent]

fwiw, ContinuousLinearMap.adjoint.norm_map A works as proof too