linear-algebra-bounded-op

Stream: new members

[Monica Omar]

I am trying to formalise that given $T$ is a bounded operator in a Hilbert space $\mathcal{H}$, then $T=1$ if and only if $\langle\psi,T\psi\rangle=1$ for all $\psi$ such that $\|\psi\|=1$.
Here is what I have got so far,

import analysis.inner_product_space.basic

variables {H 𝕜 : Type*} [is_R_or_C 𝕜]
variables [inner_product_space 𝕜 H]
variables [complete_space H]
variables (T : H →L[𝕜] H)

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

lemma easy_lemma (h : T = 1) : ∀ (ψ : H), ∥ψ∥=1 → ⟪ψ,T ψ⟫ = 1 :=
 λ ψ hψ, by simp [h, inner_self_eq_norm_sq_to_K, hψ]

lemma bounded_op_eq_one_if_norm_is_one (ψ : H) (h : ∥ψ∥=1) (h' : ⟪ψ,T ψ⟫ = 1) : T = 1 :=
 sorry

I am not sure where to go from here. Any help would be appreciated :)

[Ruben Van de Velde]

What's the mathematical proof? Do you know already?

[Monica Omar]

Yeah, you use the polarisation identity to first show $T$ is self-adjoint. Then you take the orthonormal basis to show $T$ is the identity.

[Ruben Van de Velde]

First, note that your statement only assumes that there's a particular psi that had that property, not that all psi have that property

[Ruben Van de Velde]

Some versions of the polarization identity are here: https://leanprover-community.github.io/mathlib_docs/analysis/inner_product_space/basic.html#re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two

[Monica Omar]

Here's what I got so far. Not sure if this is the right direction or not, though. Any advice? @Ruben Van de Velde

import analysis.inner_product_space.basic analysis.complex.basic analysis.normed_space.bounded_linear_maps

variables {H : Type*} [inner_product_space ℂ H]
variables [complete_space H]
variables (T : H →ₗ[ℂ] H)

lemma bounded_op_eq_one_if_norm_is_one (ψ : H) (h : ∥ψ∥=1) (h' : ⟪ψ,T ψ⟫_ℂ = 1) : T ψ = id ψ :=
 begin
   have t1 : ∥ψ∥^2  = 1 := by simp [h],
   have t2 : ⟪ψ,ψ⟫_ℂ = 1 := by { simp [inner_self_eq_norm_sq_to_K ψ],finish, },
   have : ⟪ψ,ψ⟫_ℂ - ⟪ψ,T ψ⟫_ℂ = 0 := by simp [h', t2],
   rw ← inner_sub_right at this,
   have t3 : ψ ≠ 0 := λ c, by simp [c, norm_zero] at h;contradiction,
   have :=
    calc ⟪T ψ - ψ,T ψ - ψ⟫_ℂ = ⟪T ψ,T ψ⟫_ℂ - 1 : by simp [inner_sub_right, inner_sub_left, inner_sub_left, h', t2, ← inner_conj_sym (T ψ) ψ, h']
                       ... = ⟪T ψ,T ψ⟫_ℂ - ⟪T ψ,ψ⟫_ℂ : by simp [← inner_conj_sym (T ψ) ψ, h']
                       ... = ⟪T ψ,T ψ - ψ⟫_ℂ : by rw inner_sub_right
                       ... = ⟪ψ,ψ - T ψ⟫_ℂ : sorry
                       ... = 0 : by assumption,
  have := (inner_self_eq_zero).mp this,
  have : T ψ = ψ := by { apply sub_eq_zero.mp,assumption, },
  simp,assumption,
 end

[Yaël Dillies]

Your statement is still wrong. Consider a shear in a direction orthogonal to psi. The correct statement is by quantifying over all psi both in the hypothesis and the conclusion.

[Yaël Dillies]

Regarding your sorry, what I just said is precisely what makes it wrong.

[Monica Omar]

Would the statement just be this then?

 lemma bounded_op_eq_one_if_norm_is_one (h : ∀ ψ,∥ψ∥=1 → ⟪ψ,T ψ⟫_ℂ = 1) : T = 1 :=

[Ruben Van de Velde]

Yeah, this could be a better start:

lemma bounded_op_eq_one_if_norm_is_one (h : ∀ (ψ : H), ∥ψ∥ = 1 → ⟪ψ, T ψ⟫_ℂ = 1) :
  T = 1 :=
begin
  ext ψ,
  simp only [linear_map.one_apply],
  have : inner_product_space.is_self_adjoint T,
  { sorry },
  sorry,
end

[Monica Omar]

How do you go about proving that?

[Ruben Van de Velde]

I don't know, that's what you said the proof was :)

[Ruben Van de Velde]

I managed a proof starting with

  rw [←sub_eq_zero, ←inner_map_self_eq_zero],

but perhaps that's cheating

[Monica Omar]

Oh, yeah. That does work:

lemma bounded_op_eq_one_if_norm_is_one (h : ∀ ψ : H,∥ψ∥=1) (h' : ∀ ψ : H, ⟪ψ,T ψ⟫_ℂ = 1) : T = 1 :=
 begin
   rw [←sub_eq_zero, ←inner_map_self_eq_zero],
   intro ψ,
   have t12 :=
    calc ⟪ψ,ψ⟫_ℂ = ∥ψ∥^2 : by simp [inner_self_eq_norm_sq_to_K]
             ... = 1 : by simp [h ψ],
   simp [inner_sub_left],
   rw [← inner_conj_sym,h' ψ,t12],
   simp,
end

[Kevin Buzzard]

Nice!

[Kevin Buzzard]

Wait -- does this say "assume the false statement that everything in H has norm 1" though? I have not used this stuff before but it might be good to get the statement straight. I think Ruben's version looks ok but I am a bit suspicious of Monica's.

[Ruben Van de Velde]

Oh, that explains why your version is quite a bit shorter than mine :)

[Monica Omar]

Oh, wait. Yeah, I was using my old statement.

[Monica Omar]

Ruben Van de Velde said:

Oh, that explains why your version is quite a bit shorter than mine :)

How did you go about proving it with your statement, then?

[Ruben Van de Velde]

This is the structure I ended up with - you might try to finish it from here

lemma bounded_op_eq_one_if_norm_is_one (h : ∀ (ψ : H), ∥ψ∥ = 1 → ⟪ψ, T ψ⟫_ℂ = 1) :
  T = 1 :=
begin
  rw [←sub_eq_zero, ←inner_map_self_eq_zero],
  intro ψ,
  obtain rfl|hψ := eq_or_ne ψ 0,
  { sorry },
  obtain ⟨φ, n, hφ, rfl⟩ : ∃ φ (r : ℝ), ∥φ∥ = 1 ∧ ψ = (r : ℂ) • φ,
  { sorry },
  suffices : ⟪(T - 1) φ, φ⟫_ℂ = 0,
  { sorry },
  sorry,
end

[Monica Omar]

@Ruben Van de Velde I tried with your structure, but I'm stuck here

lemma bounded_op_eq_one_if_norm_is_one (h : ∀ (ψ : H), ∥ψ∥ = 1 → ⟪ψ, T ψ⟫_ℂ = 1) :
  T = 1 :=
begin
  rw [←sub_eq_zero, ←inner_map_self_eq_zero],
  intro ψ,
  obtain rfl|hψ := eq_or_ne ψ 0,
  { simp },
  obtain ⟨φ, n, hφ, rfl⟩ : ∃ φ (r : ℝ), ∥φ∥ = 1 ∧ ψ = (r : ℂ) • φ,
  {
    use ψ,
    use 1,
    refine ⟨_,by finish⟩,
    sorry,
     },
  suffices : ⟪(T - 1) φ, φ⟫_ℂ = 0,
  {
    rw [inner_smul_right],
    have t2 : conj ↑n * ⟪(T-1) φ,φ⟫_ℂ = conj ↑n * 0 := by rw this,
    rw ← inner_smul_left at t2,
    have t3 : ⟪↑n • (T-1) φ,φ⟫_ℂ = ⟪(T-1) (↑n • φ),φ⟫_ℂ := sorry,
    rw [← t3,t2],
    norm_num,
     },
  simp [inner_sub_left],
  rw [inner_self_eq_norm_sq_to_K, hφ, ←inner_conj_sym (T φ) φ, h φ hφ],
  norm_num,
end

[Kevin Buzzard]

    have t3 : ⟪↑n • (T-1) φ,φ⟫_ℂ = ⟪(T-1) (↑n • φ),φ⟫_ℂ,
    { rw linear_map.map_smul, },

[Kevin Buzzard]

The only reason the terms on either side of the = are different is that you are taking a scalar multiplication (smul) out of an application (map) of a linear map. Now you can guess the name of the lemma which gets you home.