Unitaries preserve norm

Stream: Is there code for X?

[Alex Meiburg]

import Mathlib
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
theorem unitary_preserves_norm (x : H) (B : unitary (H →L[ℂ] H)) : ‖x‖ = ‖B.1 x‖
  := by sorry

Trying by exact? times out, and Loogle "unitary, Norm" gives no results. But surely the fact that "unitary operators preserve norm" is in there? :P Or is this wrong in some awful subtle way

[Alex Meiburg]

Oops, the Loogle should be Norm.norm, unitary. That gives results, but only norms of operators, not the underlying space

[Jireh Loreaux]

I think we don't have it yet.

[Jireh Loreaux]

We do have docs#CstarRing.norm_of_mem_unitary, but that's not quite strong enough. (Or at least, it still takes some work to prove it.)

[Jireh Loreaux]

You should just prove it directly by going through the inner product.

[Alex Meiburg]

Alright. I guess I just felt like it ... must! be in the mathlib. Maybe it's my bias coming from quantum mechanics, but it feels like probably the second fact about unitary operators that I would want to prove :sweat_smile: (the first being that they form a group) so I thought I must be missing it

[Anatole Dedecker]

I think the reason is that this property doesn’t make sense anymore in the general setting of star-algebras. But we definitely want this so feel free to open a PR!

[Alex Meiburg]

Actually, what I wrote is for bounded operators, but it should be right for any operators on H right?

[Alex Meiburg]

or maybe that's nonsense. My analysis is weak. I guess I think of operators (in quantum mechanics) like X that aren't bounded, but then, the question is what space those actually operate on. Whatever. I'll just leave it with →L[ℂ]

[Alex Meiburg]

theorem unitary_norm_eq (x : H) (B : unitary (H →L[ℂ] H)) : ‖x‖ = ‖B.1 x‖
  := by
    suffices ‖x‖^2 = ‖B.1 x‖^2 by
      apply (sq_eq_sq _ _).mp this
      <;> exact norm_nonneg _
    rw [norm_sq_eq_inner (𝕜 := ℂ) x, norm_sq_eq_inner (𝕜 := ℂ) (B.1 x)]
    rw [← ContinuousLinearMap.adjoint_inner_right]
    congr
    have hbbx : (ContinuousLinearMap.adjoint B.1) (B.1 x) = (star B.1 * B.1) x := by
      rfl
    rw [hbbx, B.property.1, ContinuousLinearMap.one_apply]

This works. I don't like it .. I don't like writing a long equality that's just rfl in order to rw it. Is there a way to say "coerce the goal into this form, assuming that it's defeq"?

[Alex Meiburg]

(deleted)

[Richard Osborn]

change x = (star B.1 * B.1) x is what you want

[Alex Meiburg]

Ahh that's it. Thanks. Also, this might be a better spelling, I'm not sure:

theorem unitary_norm_eq (x : H) (B : H →L[ℂ] H) (hB : B ∈ unitary (_)) : ‖x‖ = ‖B x‖
  := by
    suffices ‖x‖^2 = ‖B x‖^2 by
      apply (sq_eq_sq _ _).mp this
      <;> exact norm_nonneg _
    rw [norm_sq_eq_inner (𝕜 := ℂ) x, norm_sq_eq_inner (𝕜 := ℂ) (B x)]
    rw [← ContinuousLinearMap.adjoint_inner_right]
    congr
    change x = (star B * B) x
    rw [hB.1, ContinuousLinearMap.one_apply]

[Moritz Doll]

Alex Meiburg said:

or maybe that's nonsense. My analysis is weak. I guess I think of operators (in quantum mechanics) like X that aren't bounded, but then, the question is what space those actually operate on. Whatever. I'll just leave it with →L[ℂ]

Unitary operators on Hilbert spaces are bounded.

[Jireh Loreaux]

Richard Osborn said:

change x = (star B.1 * B.1) x is what you want

Almost never do you really want change. If you have it, then you're likely missing a lemma (provable by rfl). What you need here is docs#ContinuousLinearMap.mul_apply and docs#ContinuousLinearMap.star_eq_adjoint

[Alex Meiburg]

rw [← ContinuousLinearMap.mul_apply, ← ContinuousLinearMap.star_eq_adjoint] seems much longer than change x = (star B * B) x :) Why is this preferable? (I trust you that it is, but curious why)

Also, tips on how to find these lemmas? exact? doesn't work because it just gives me rfl as the proof

[Alex Meiburg]

Moritz Doll said:

Unitary operators on Hilbert spaces are bounded.

Of course :) But unitary takes a monoid (not a vector space, which I understand but is slightly off-putting), and I could imagine writing this theorem as unitary (bounded linear operators on H) or as unitary (linear operators on H).

[Alex Meiburg]

Unfortunately, I'm used to these terms being played with very fast and loose, see e.g. the terminology confusion at https://en.wikipedia.org/wiki/Unbounded_operator

[Jireh Loreaux]

change is prone to breakage if things ever get redefined (even to something that is equal). Also, it's not much longer if you're in the ContinuousLinearMap namespace (which it would be, because this lemma should be called ContinuousLinearMap.norm_map_of_mem_unitary, and the LHS and RHS should be switched). Something like this:

import Mathlib

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

theorem ContinuousLinearMap.norm_map_of_mem_unitary (x : H)
    (U : H →L[ℂ] H) (hU : U ∈ unitary (H →L[ℂ] H)) : ‖U x‖ = ‖x‖ := by
  suffices ‖U x‖ ^ 2 = ‖x‖ ^ 2 by
    apply (sq_eq_sq _ _).mp this <;> exact norm_nonneg _
  rw [norm_sq_eq_inner (𝕜 := ℂ) x, norm_sq_eq_inner (𝕜 := ℂ) (U x), ← adjoint_inner_right]
  congr
  congrm($(unitary.star_mul_self_of_mem hU) x)

[Jireh Loreaux]

Also, there's no reason to restrict to ℂ here. This should work fine with {𝕜 : Type*} [IsROrC 𝕜]

[Junyan Xu]

We should define the isomorphism between unitary (H →L[ℂ] H) and H ≃ₗᵢ[ℂ] H (docs#LinearIsometryEquiv.instGroupLinearIsometryEquivIdToNonAssocSemiringIds) ...

[Yaël Dillies]

#10847

[Jireh Loreaux]

Junyan Xu said:

We should define the isomorphism between unitary (H →L[ℂ] H) and H ≃ₗᵢ[ℂ] H (docs#LinearIsometryEquiv.instGroupLinearIsometryEquivIdToNonAssocSemiringIds) ...

I have this now and several related results. I'll PR shortly.

[Jireh Loreaux]

#10858