Toeplitz-Hausdorff

Stream: mathlib4

[George Granberry]

Hey everyone, I've been working on formalizing the Toeplitz-Hausdorff theorem for my first Lean formalization. I'm just about done and have to some time to do some complimentary work. Does anyone have any requests/suggestions? Also I'd love some feedback on my proof if anyone is interested

[Filippo A. E. Nuccio]

Do you have a repository where we can have a look at your code?

[George Granberry]

Sure, here it is
https://github.com/ggranberry/ToeplitzHausdorff

[Filippo A. E. Nuccio]

Thanks, and congratulations for your work! Have you considered using docs#Convex ? It has the advantage of having a lot of API (= basic results that make your life easier) built around it. In general, when you introduce a notion it is useful to build this kind of things, and very often "basic" notions are already in Mathlib. Also, we try to prove things in the greatest possible generality and Toplitz-Hausdorff is true for more general operators than linear ones in finite dim's spaces, see for instance here

[Filippo A. E. Nuccio]

Concerning feedback on your work, we're more than welcome to provide this but it would be easier for us if you open a pull request following the instructions here in the section "Making a Pull Request"

[George Granberry]

That would be great! And thanks for all the suggestions. This is my first time using Lean so I've been kind of stumbling along with this project. I'll open up a PR

[George Granberry]

Ok i've got a fork/branch. Where in mathlib would you recommend putting my proof?

[Johan Commelin]

Does you branch live in your fork? Or in the upstream repo?

[Johan Commelin]

Do you already have push access to github.com/leanprover-community/mathlib4 ?

[George Granberry]

It currently lives in my own fork. I figured I'd get all the perms for the upstream repo later

[Johan Commelin]

If you want to make a PR, it's best if you do it from an upstream branch (for crazy CI reasons, sorry)

[Johan Commelin]

Could you please add your github handle to your zulip account?

[George Granberry]

Oh I don't mind at all.

[George Granberry]

Done.
And here is my github in case you don't want to go look at my profile
https://github.com/ggranberry

[Johan Commelin]

Voila: https://github.com/leanprover-community/mathlib4/invitations

[George Granberry]

https://github.com/leanprover-community/mathlib4/pull/22925/files

[Filippo A. E. Nuccio]

Great! I'll be happy to give a look at your file soon (=starting from Tue, I am terribly busy these coming 3 days).

[Kevin Buzzard]

Fortunately the CI machines are already happy to do some initial reviewing :-)

[George Granberry]

Haha, yeah the CI machines are definitely unhappy. I'm still working on some of these subproofs so no hurry

[George Granberry]

One thing I've been stuck on if any passer-bys have an idea:

I have this bit in my formula: inner x₁ x₂

@inner ℝ (EuclideanSpace ℂ n) InnerProductSpace.toInner x₁ x₂ : ℝ

and I've been trying to rewrite it (with no luck) using

EuclideanSpace.inner_eq_star_dotProduct

EuclideanSpace.inner_eq_star_dotProduct.{u_1, u_3} {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι]
  (x y : EuclideanSpace 𝕜 ι) : inner x y = (WithLp.equiv 2 (ι → 𝕜)) y ⬝ᵥ star ((WithLp.equiv 2 (ι → 𝕜)) x)

but not getting a match on it. Any ideas on a fix/alternative? I can link my proof state if needed.

so for example I would like to rewrite inner x y like this:

import Mathlib.LinearAlgebra.Matrix.PosDef


open Complex Matrix

variable {n : Type*} [Fintype n] [DecidableEq n]

lemma inner_eq_star_dotProduct (x y : EuclideanSpace ℂ n) : inner x y = star x ⬝ᵥ y := by
  simp [EuclideanSpace.inner_eq_star_dotProduct]

But this doesn't seem to be the case.

[Kevin Buzzard]

People will find it much easier to read your posts if you follow the instructions in #backticks and they'll find it much easier to answer them if you also check out #mwe (also note that you can edit posts, you don't have to repost)

[Kevin Buzzard]

In short, I'm far more likely to be able to fix your error if I can reproduce it locally especially if that involves just clicking on the link on code enclosed within backticks

[George Granberry]

For further context I'm stuck on two holes in my proof where I commented "stuck here" in exp2 and conv_eq

-- This module serves as the root of the `ToeplitzHausdorff` library.
-- Import modules here that should be built as part of the library.
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.LinearAlgebra.Matrix.Hermitian
import Mathlib.Analysis.Convex.Basic
import Mathlib.Algebra.Group.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.PosDef

open Complex Matrix

variable {n : Type*} [Fintype n] [DecidableEq n]
variable (A : Matrix n n ℂ)

def numericalRange (A : Matrix n n ℂ) : Set ℂ :=
  { z | ∃ x : EuclideanSpace ℂ n, ‖x‖ = 1 ∧ z = dotProduct (star x) (A.mulVec x) }

def convex_set (S : Set ℂ) : Prop :=
  ∀ (z1 z2: ℂ) (t : ℝ) , (z1 ∈ S) -> (z2 ∈ S) -> (0 <= t) -> (t <= 1) ->
    (1 - t) * z1 + t * z2 ∈ S

open Classical

theorem toeplitz_hausdorff {A : Matrix n n ℂ} (hA : Aᴴ = A):
  -- TODO use Convex rather than convex_set
  convex_set (numericalRange A) :=
  by
    intros z₁ z₂ t hz₁ hz₂ ht₀ ht
    obtain ⟨x₁, hx₁, hz₁'⟩ := hz₁
    obtain ⟨x₂, hx₂, hz₂'⟩ := hz₂

    let v := (1 - t) • x₁ + t • x₂
    by_cases hv : v = 0
    {
      -- skipped for brevity. I've got this part solved
      sorry
    }
    {
      let xₜ := ‖v‖⁻¹ • v
      use xₜ
      have h_norm : ‖‖v‖⁻¹ • v‖ = 1 := by
         simp [norm_smul, hv]
      simp_all

      -- We can go ahead and define the quadratic form of the norm of v to use its properties
      have expand_xt : star xₜ ⬝ᵥA *ᵥxₜ = (star v ⬝ᵥA *ᵥv) / ‖v‖^2 := by
        rw [star_smul, star_trivial, mulVec_smul, dotProduct_smul]
        field_simp [hv]
        ring_nf
        simp

      rw [expand_xt]

      -- Rewrite qudratic form of the numerator using our unit vectors and t
      have exp1 : star v ⬝ᵥ A *ᵥv =
        (1-t)^2 * (star x₁ ⬝ᵥ A *ᵥx₁)
        + t^2 * (star x₂ ⬝ᵥ A *ᵥ x₂)
        + t*(1-t)*(star x₁ ⬝ᵥ A *ᵥ x₂ + star x₂ ⬝ᵥ A *ᵥ x₁) := by
        -- skipped for brevity. I've got this part solved
        sorry

      -- Rewrite qudratic form of the denominator using our unit vectors and t
      have exp2 : ‖v‖^2 = (1-t)^2 + t^2 + 2*t*(1-t)* (star x₁ ⬝ᵥ x₂) := by
        norm_cast
        rw [norm_add_sq_real]
        rw [norm_smul, norm_smul]
        rw [Real.norm_eq_abs, Real.norm_eq_abs]
        rw [hx₁, hx₂]
        rw [inner_smul_left, inner_smul_right]
        rw [starRingEnd_apply, star_trivial]
        rw [_root_.abs_of_nonneg (sub_nonneg.mpr ht), _root_.abs_of_nonneg  ht₀]
        simp
        ring_nf
        sorry
        -- STUCK HERE

      -- using the expansion of the numerator and the denominator,
      -- simplify the quadratic form of the norm of v
      have conv_eq : (star v ⬝ᵥ A *ᵥ v) / ‖v‖^2 =
        (1-t) * (star x₁ ⬝ᵥ A *ᵥ x₁) + t * (star x₂ ⬝ᵥ A *ᵥ x₂) := by

        rw [exp1, exp2]

        have H : (1 - ↑t)^2 + ↑t^2 + 2 * ↑t * (1 - ↑t) * (star x₁ ⬝ᵥ x₂) ≠ 0 := by
          intro h
          simp_all

        field_simp [H]
        sorry
        -- STUCK HERE

      simp [conv_eq]
      linarith
    }

For exp2 I'm struggling to figure out how
∑ x : n, (↑(x₂ x).re * ↑(x₁ x).re + ↑(x₂ x).im * ↑(x₁ x).im)
can be related to star on the two sides of my equation