Defining an inner product to use Cauchy-Schwarz

Stream: new members

[Gregory Wickham]

I'd like to define a semi-inner product (positive semidefinite sesquilinear form) so that I can use the Cauchy-Schwarz inequality, but I can't figure out how to construct an inner product/inner product space in a way that lets me do that.

I was able to define my inner product function to have type A →ₗ⋆[ℂ] A →ₗ[ℂ] ℂ, so that it is conjugate-linear in the first term and linear in the second, which I thought would be what I needed based on what I saw about CStarModules, hoping to maybe use CStarModule.norm_inner_le.

But, I couldn't figure out how to make that work, so I tried defining a PreInnerProductSpace, but I still couldn't figure out how that would allow me to use inner_mul_inner_self_le.

I think I faced the same problem with both approaches, which was that I couldn't figure out how to ensure that inner was the function I defined. Specifically, when I try to use InnerProductSpace.Core.inner_mul_inner_self_le, it seems like it can't figure out that it's a complex inner product, which implies it is not referring to the inner product I defined.

Can somebody help me figure out how to use the Cauchy-Schwarz inequality on the semi-inner product I defined?

Here is my code so far:

import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Algebra.Order.Module.PositiveLinearMap
import Mathlib.Analysis.InnerProductSpace.Defs

variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [PartialOrder ℂ]
variable (f : A →ₚ[ℂ] ℂ)
variable (p q : A)

def myInner := fun (f : A →ₚ[ℂ] ℂ) (b : A) (a : A) => f (star b * a)
#check (myInner f : A → A → ℂ) -- A → A → ℂ
#check (myInner f : A → A → ℂ) p -- A → ℂ
-- parameter a should be linear
def myInnerHelper (f : A →ₚ[ℂ] ℂ) (a : A) : LinearMap (RingHom.id ℂ) A ℂ where
  toFun := (myInner f : A → A → ℂ) a -- A → ℂ
  map_add' := by
    intro x y
    dsimp [myInner]
    rw [mul_add]
    exact map_add f (star a * x) (star a * y)
  map_smul' := by
    intro m x
    dsimp [myInner, RingHom.id]
    simp
#check (myInnerHelper f) p -- A →ₗ[ℂ] ℂ
-- paramter b should be conjugate linear
def mySesquiLinear (f : A →ₚ[ℂ] ℂ) : LinearMap (starRingEnd ℂ) A (A →ₗ[ℂ] ℂ) where
  toFun := (myInnerHelper f)
  map_add' := by
    intro x y
    ext a
    dsimp [myInnerHelper, myInner]
    rw [star_add, add_mul]
    exact map_add f (star x * a) (star y * a)
  map_smul' := by
    intro m x
    ext a
    simp [myInnerHelper, myInner]
#check mySesquiLinear f -- A →ₗ⋆[ℂ] A →ₗ[ℂ] ℂ

instance myInnerProductSpace : PreInnerProductSpace.Core ℂ A where
  inner := (myInner f : A → A → ℂ)
  re_inner_nonneg := sorry
  conj_inner_symm := sorry
  add_left := sorry
  smul_left := sorry

#check InnerProductSpace.Core.inner_mul_inner_self_le p q -- has type:
-- ‖inner ?m.8 p q‖ * ‖inner ?m.8 q p‖
-- ≤ RCLike.re (inner ?m.8 p p) * RCLike.re (inner ?m.8 q q)

[Kenny Lau]

how is Lean supposed to guess what f is?

[Gregory Wickham]

f is just an arbitrary positive linear functional. I won't need to evaluate it. Ideally, I would just like to be able to dsimp inner ℂ b a to f (star b * a)

[Kenny Lau]

@Gregory Wickham yes, but i'm saying that when you write inner, there is no way that Lean can figure out what f is

[Kenny Lau]

i.e. you have a bad instance

[Gregory Wickham]

Why does it need to know what fis (beyond knowing that it's a positive linear functional)? And how can I fix that?

[Eric Wieser]

Maybe it helps to realize that myInnerProductSpace is defined for all possible f; hover over if and you'll see it's a function from f

[Gregory Wickham]

So then when I write myInnerProductSpace f, it has type PreInnerProductSpace.Core ℂ A, which I think is what I want. So then I think my question is how do I use inner_mul_inner_self_le so that it knows that the inner I'm referring to is specifically (myInnerProductSpace f).inner.

Because if I try to #check InnerProductSpace.Core.inner_mul_inner_self_le p q, it says failed to synthesize PreInnerProductSpace.Core ?m.8. How can I tell it to synthesize myInnerProductSpace f when it looks like it can't take that as an explicit parameter?

[Kenny Lau]

it's a bad instance, you shouldn't use it

[Gregory Wickham]

Can you explain how I can tell it's a "bad instance"? I'm still pretty new to Lean.

And then how do I construct an inner product whose definition depends on some fixed linear functional? Because this isn't the only time I'll need to do that.

[Eric Wieser]

This works:

example :=
  let := myInnerProductSpace f (A := A)
  InnerProductSpace.Core.inner_mul_inner_self_le (𝕜 := ℂ) p q

[Eric Wieser]

To refine what Kenny said, it's a bad instance, so you should make it an abbrev instead

[Eric Wieser]

Note that Lean also doesn't know in your original whether it's looking for a real or complex inner product

[Eric Wieser]

For what it's worth, you can drop most of your code by using

noncomputable def mySesquilinear (f : A →ₚ[ℂ] ℂ) : A →ₗ⋆[ℂ] A →ₗ[ℂ] ℂ :=
  (LinearMap.mul ℂ A).comp (starLinearEquiv ℂ (A := A) : A →ₗ⋆[ℂ] A) |>.compr₂ₛₗ f

@[simp]
theorem mySesquilinear_apply (f : A →ₚ[ℂ] ℂ) (x y : A) : mySesquilinear f x y = f (star x * y) := rfl

(the noncomputable is a bug, fixed by #29608 and #29609)

[Kenny Lau]

Gregory Wickham said:

how I can tell it's a "bad instance"?

because it depends on some f that cannot be inferred (i.e. Lean has no way of guessing the f)

[Kenny Lau]

Gregory Wickham said:

how do I construct an inner product whose definition depends on some fixed linear functional

you either locally make it an instance like eric suggested (where "locally" really means you need to do it in every statement and every proof),
or you can define a type synonym WithFunctional A f of A so that f is baked into the type

[Kenny Lau]

that means, def WithFunctional (A : ..) (f : ..) := A

[Kenny Lau]

and then make instance : InnerProductSpace (WithFunctional A f)

[Eric Wieser]

Kenny, my reading of the problem was that this was a temporary instance just to get a Cauchy-Schwarz result

[Eric Wieser]

So while what you describe is true for instances you plan to use across multiple theorems, it seem overkill here

[Kevin Buzzard]

Gregory Wickham said:

Can you explain how I can tell it's a "bad instance"? I'm still pretty new to Lean.

For what it's worth, I had to read #tpil three times and do several Lean projects before I got the hang of instances (a.k.a. the square bracket system). Behind the scenes there is a computer program filling in all of the theorems of the form "a field is an additive abelian group" (which you need every time you e.g. use that $a+b=b+a$ for a field) and this program works in a certain way, which you pick up over time. The key thing to understand is that this program cannot do everything which is obvious to a human, it can only do what it's been programmed to do, there are certain facts that it can use and other facts that it can't use. What Kenny means is that the program that's dealing with all the square bracket stuff doesn't have access to f, but this is not at all obvious, this only becomes obvious when you have a feeling for how the program does what it does.

[Gregory Wickham]

Eric Wieser said:

This works:

example :=
  let := myInnerProductSpace f (A := A)
  InnerProductSpace.Core.inner_mul_inner_self_le (𝕜 := ℂ) p q

How does this force the theorem to identify the correct InnerProductSpace? Is the point that it puts a PreInnerProductSpace into the context so that the theorem can infer it? Is there no more specific way to make sure it identifies the correct PreInnerProductSpace, like if there might be more than one in the context?

It seems like I can use that method to get a specific statement of the theorem into the context, like here:

example (a b : A) : norm (f (star b * a)) ^2 ≤ f (star b * b) * f (star a * a) := by
  let mip := myInnerProductSpace f (A := A)
  have cs := InnerProductSpace.Core.inner_mul_inner_self_le (𝕜 := ℂ) a b
  sorry

but then I can't seem to simp, dsimp, or rw inner to the definition I gave it when defining myInnerProductSpace. Is there any way to still simplify to the specific, definition of inner for a particular space?

[Jireh Loreaux]

So presumably you are trying to do GNS, right? You'll want to make a type synonym as Kenny suggested.

[Gregory Wickham]

Yes, I'm trying to do GNS. What is a type synonym and how does it help here? Is there somewhere I can read about how those work? Because I cannot figure out how I'm supposed to use that.

[Gregory Wickham]

Specifically because a definition like this:
Kenny Lau said:

that means, def WithFunctional (A : ..) (f : ..) := A

would seem to erase information when passed to some constructor. I could understand maybe defining a new type/structure that contains a functional alongside a C*-algebra and maybe just separately referring to its components as necessary, but the approach you're suggesting seems very different from that.

[Jireh Loreaux]

No, that's exactly what this is doing. Now for every C⋆-algebra A and every functional f, we have a new type WithFunctional A f which is a copy of A, except this new type doesn't have an instances on it. So we can equip it with new ones (e.g., a new norm).

[Jireh Loreaux]

This is important because having an InnerProductSpace means that you must have a norm that agrees with the inner product. You can't do this on A itself (because it already has a norm), but you can do it on the type WithFunctional A f.

[Jireh Loreaux]

(when I say "can't", I mean, technically you can but you will make Lean, and consequently yourself, misrable by doing so)

[Jireh Loreaux]

You can see, for example, how docs#WithLp defines a type synonym for a new type but equips it with the Lp norm. For example, ℝ × ℝ has the max norm in Lean, but WithLp p (ℝ × ℝ) has the p-norm.

[Jireh Loreaux]

If we tried to put the p-norm on ℝ × ℝ directly, then Lean would never be able to know which norm to choose for ‖x‖ for x : ℝ × ℝ (because there's no reference to p; this is what Kenny said above when he mentioned your instance was a "bad instance"). But if you have x : WithLp p (ℝ × ℝ), then Lean knows that ‖x‖ is p-norm (because p is encoded in the type, and we've equipped this type with the p-norm).

[Jireh Loreaux]

I think @Monica Omar may be working on GNS though.

[Gregory Wickham]

So is this:

def WithFunctional (A : Type*) [CStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) := A

variable [CStarAlgebra (WithFunctional A f)] [PartialOrder (WithFunctional A f)]

instance myInnerProductSpace : PreInnerProductSpace.Core ℂ (WithFunctional A f) where
  inner := sorry
  re_inner_nonneg := sorry
  conj_inner_symm := sorry
  add_left := sorry
  smul_left := sorry

the right set up to start using this "type synonym"? Because then the next thing I have to do is re-work my inner product function to have type WithFunctional A f → WithFunctional A f → ℂ, but when I try do that, I'm told "synthesized type class instance is not definitionally equal to expression inferred by typing rules".

I'll also try to look the examples you've shared to see if I can figure it out.

[Jireh Loreaux]

No, your variable line means "put an arbitrary C⋆-algebra and partial order instance on this type".

[Jireh Loreaux]

You don't want WithFunction A f to have a C⋆-algebra instance at all, ever, because it's going to be the space for the representation. So, you'll need to set up some basic things, like construct an equivalence (trivial) between A and WithFunctional A f, and then use this to pull back the vector space structure from A to WithFunctional A f. And after that you can construct your instance.

[Gregory Wickham]

I did my best to adapt the code you referenced to this situation, but it seems like I ended up exactly where I started. I still can't seem to make an instance of PreInnerProductSpace.Core, and even my definition of my inner product is quesitonable. And I definitely can't adapt Eric Wieser's definition for the inner product function.

Am I even remotely on the right track? Or do I need to do something else entirely?

This is my code so far:

import Mathlib.Analysis.CStarAlgebra.Classes
import Mathlib.Algebra.Order.Module.PositiveLinearMap
import Mathlib.Analysis.InnerProductSpace.Defs
import Mathlib.Analysis.InnerProductSpace.Basic

variable [PartialOrder ℂ]
variable {A : Type*} [CStarAlgebra A] [PartialOrder A]
variable (f : A →ₚ[ℂ] ℂ)

def WithFunctional (_A : Type*) [CStarAlgebra _A] [PartialOrder _A] (_f : _A →ₚ[ℂ] ℂ) := _A

namespace WithFunctional

/-- The canonical inclusion of `A` into `WithFunctional A f`. -/
def toFunctional : A → WithFunctional A f := id

/-- The canonical inclusion of `WithFunctional A f` into `A`. -/
def ofFunctional : WithFunctional A f → A := id

/-- `WithFunctional.toFunctional` and `WithFunctional.toFunctional` as an equivalence. -/
@[simps]
protected def equiv : WithFunctional A f ≃ A where
  toFun := ofFunctional f
  invFun := toFunctional f
  left_inv _ := rfl
  right_inv _ := rfl

instance instAddCommGroup [AddCommGroup A] : AddCommGroup (WithFunctional A f) := ‹AddCommGroup A›
instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring A] :
  NonUnitalNonAssocSemiring (WithFunctional A f) := ‹NonUnitalNonAssocSemiring A›
instance instModule [Semiring ℂ] [AddCommGroup A] [Module ℂ A] :
  Module ℂ (WithFunctional A f) := ‹Module ℂ (WithFunctional A f)›

/-
-- Some other properties I could specify:
instance instStarAddMonoid [StarAddMonoid A] : StarAddMonoid (WithFunctional A f) :=
 ‹StarAddMonoid A›
instance instAddCommMonoid [AddCommMonoid (StarAddMonoid A)] :
  AddCommMonoid (StarAddMonoid (WithFunctional A f)) :=
 ‹AddCommMonoid (StarAddMonoid A)›
 variable [PartialOrder (WithFunctional A f)]
instance instStarAddMonoidFunctional [StarAddMonoid (A →ₗ⋆[ℂ] A)] :
  StarAddMonoid (WithFunctional A f →ₗ⋆[ℂ] WithFunctional A f) :=
  ‹StarAddMonoid (A →ₗ⋆[ℂ] A)›
-/

def myInner (a b : WithFunctional A f) : ℂ := f (star b * a)
#check myInner f

instance myInnerProductSpace : PreInnerProductSpace.Core ℂ (WithFunctional A f) where
  inner := myInner f
  re_inner_nonneg := sorry
  conj_inner_symm := sorry
  add_left := sorry
  smul_left := sorry

example (a b : WithFunctional A f) : a = a := by
  #check InnerProductSpace.Core.inner_self_nonneg (𝕜 := ℂ) a b -- can't find the instance
  sorry

end WithFunctional

[Monica Omar]

It's not that it can't find the instance, if you look at the error it says that it expected a function...
inner_self_nonneg is a function that takes in {x : F} and outputs 0 ≤ inner _ x x. Changing this to

#check InnerProductSpace.Core.inner_self_nonneg (𝕜 := ℂ) (x := a)

will show you that it's working okay.

[Monica Omar]

Gregory Wickham said:

And I definitely can't adapt Eric Wieser's definition for the inner product function.

I think what Eric was saying is that instead of proving addition and scalar multiplication, you can get them for free by defining it as a bi-semi-linear map:

noncomputable def mySesquilinear (f : A →ₚ[ℂ] ℂ) : A →ₗ⋆[ℂ] A →ₗ[ℂ] ℂ :=
  (LinearMap.mul ℂ A).comp (starLinearEquiv ℂ (A := A) : A →ₗ⋆[ℂ] A) |>.compr₂ₛₗ f

noncomputable instance myInnerProductSpace : PreInnerProductSpace.Core ℂ (WithFunctional A f) where
  inner a b := mySesquilinear f a b
  re_inner_nonneg := sorry
  conj_inner_symm := sorry
  add_left _ _ _ := LinearMap.map_add₂ _ _ _ _
  smul_left _ _ _ := LinearMap.map_smulₛₗ₂ _ _ _ _

[Gregory Wickham]

Thank you for your help! This will also certainly be useful for other steps of GNS. @Monica Omar are you working on GNS too? If so, and if there's any way I could help, I would love to contribute. But also, I'm clearly very new to lean, and so working on it separately would still be an important learning experience for me, and I'll probably keep working on it either way.

[Monica Omar]

I am. And, yeah, sure. There's no better way to learn than by doing. I'll let you know when I get back on working on it :)

[Gregory Wickham]

Sounds good!