Uniqueness of (global) minimum

Stream: new members

[Aron Erben]

Hello, I would like to prove the following (written as #mwe):

import data.matrix.basic
import data.real.basic
import topology.local_extr
import topology.instances.matrix

def is_ols_coefficient
  {u v : ℕ}
  (Y : matrix (fin u) unit ℝ)
  (X : matrix (fin u) (fin v) ℝ)
  (β : matrix (fin v) unit ℝ)
  : Prop
:= is_local_min (λ (β : matrix (fin v) unit ℝ), ((Y - X ⬝ β)ᵀ ⬝ (Y - X ⬝ β)) () ()) β

variables
  {n p₁ : ℕ}
  (Y : matrix (fin n) unit ℝ)
  (X₁tilde : matrix (fin n) (fin p₁) ℝ)
  (β₁tilde : matrix (fin p₁) unit ℝ)
  (β₁caron : matrix (fin p₁) unit ℝ)

  (h₁ : is_ols_coefficient Y X₁tilde β₁tilde)
  (h₂ : is_ols_coefficient Y X₁tilde β₁caron)

include h₁ h₂
theorem t1 : β₁tilde = β₁caron :=
begin
  sorry,
end

In words: β₁tilde and β₁caron are both local minima of the function above, and I would like to show they are the same local minimum, as the function is convex.

How would I go about proving t1? I've tried is_min_on.of_is_local_min_of_convex_univ from analysis.convex.extrema, but matrices don't seem to be instances of topological_add_group, although Pi types are (wouldn't that imply matrices are too?). I would also have to show convexity with this theorem, which I'm also kind of stuck on...

The context for all this is some work on theorems related to linear regression and ordinary least squares (Is there prior work on these topics? I was not able to find relevant discussions on Zulip).

Besides the above question, is this canonical Lean? Are hypotheses supposed to go into a variables section?

Thanks in advance!

[Aron Erben]

I'm guessing I could do something with positive semi-definiteness to prove convexity here?

[Yaël Dillies]

Are you following a reference?

[Aron Erben]

@Yaël Dillies Well, not quite, they are very superficial lecture notes from a coworker that don't go into detail. This proof is pretty much only implied in a paragraph... Maybe I misunderstood your question?

[Yaël Dillies]

Nono, that's what I meant. What function exactly are you trying to prove the convexity of?

[Yaël Dillies]

I assume you know about docs#convex_on, already?

[Aron Erben]

Yaël Dillies said:

Nono, that's what I meant. What function exactly are you trying to prove the convexity of?

Ah I see, if I were to somehow get docs#is_min_on.of_is_local_min_of_convex_univ to work, I would have to proof the convexity of (λ (β : matrix (fin v) unit ℝ), ((Y - X ⬝ β)ᵀ ⬝ (Y - X ⬝ β)) () ()), where Y and X are the matrices given in is_ols_coefficient.

But I'm still stuck at the earlier step, since it's still telling me that

35:13: failed to synthesize type class instance for
...
⊢ topological_add_group (matrix (fin p₁) unit ℝ)

If I have

include h₁ h₂
theorem t1 : β₁tilde = β₁caron :=
begin
  rw is_ols_coefficient at h₁,
  rw is_ols_coefficient at h₂,
  have a := is_min_on.of_is_local_min_of_convex_univ h₁
end

[Aron Erben]

Yaël Dillies said:

I assume you know about docs#convex_on, already?

Yes, this is mentioned in one of the hypotheses for docs#is_min_on.of_is_local_min_of_convex_univ, so I'm trying to get exactly that

[Yaël Dillies]

We have docs#matrix.topological_ring. Does your file import file#topology/instances/matrix ?

[Aron Erben]

Yes I'm importing it in the #mwe. Could I somehow project out the additive topological group from the topological ring to get a topological_add_group instance?

[Aron Erben]

Ah, I just found docs#topological_ring.to_topological_add_group, that might be it

[Alex J. Best]

Typeclass instance search should be filling in that sort of gap for you in most cases though

[Kevin Buzzard]

I just tried your code and it doesn't compile for me; I have complaints about X ⬝ β, Lean doesn't know what the dot is. Edit: aah, open_locale matrix fixes it

[Alex J. Best]

In your case the indexing type for the rows is not the same as for the columns so it won't be a ring it seems

[Kevin Buzzard]

letI : topological_add_group (matrix (fin p₁) unit ℝ) := by delta matrix; apply_instance,

(as the first line of the proof) is a hacky way to get that topological additive group, but it doesn't solve your problems because Lean now complains it doesn't know that the action of R on matrices is continuous.

[Kevin Buzzard]

But I'm wondering whether really we're missing imports here or something?

[Kevin Buzzard]

We're missing imports. With import all the below works without the weird instance at the top.

import data.matrix.basic
import data.real.basic
import topology.local_extr
import topology.instances.matrix
import analysis.convex.extrema
import topology.algebra.mul_action
import topology.instances.real
--import all

instance : has_continuous_smul ℝ ℝ := infer_instance -- with `import all` I don't need this

open_locale matrix

def is_ols_coefficient
  {u v : ℕ}
  (Y : matrix (fin u) unit ℝ)
  (X : matrix (fin u) (fin v) ℝ)
  (β : matrix (fin v) unit ℝ)
  : Prop
:= is_local_min (λ (β : matrix (fin v) unit ℝ), ((Y - X ⬝ β)ᵀ ⬝ (Y - X ⬝ β)) () ()) β

variables
  {n p₁ : ℕ}
  (Y : matrix (fin n) unit ℝ)
  (X₁tilde : matrix (fin n) (fin p₁) ℝ)
  (β₁tilde : matrix (fin p₁) unit ℝ)
  (β₁caron : matrix (fin p₁) unit ℝ)

  (h₁ : is_ols_coefficient Y X₁tilde β₁tilde)
  (h₂ : is_ols_coefficient Y X₁tilde β₁caron)

include h₁ h₂

instance : topological_add_group (matrix (fin p₁) unit ℝ) := by delta matrix; apply_instance

theorem t1 : β₁tilde = β₁caron :=
begin
  letI : topological_add_group (matrix (fin p₁) unit ℝ) := by delta matrix; apply_instance,
  haveI : has_continuous_smul ℝ (matrix (fin p₁) unit ℝ) := by delta matrix; apply_instance,
  have := is_min_on.of_is_local_min_of_convex_univ h₁,
  sorry,
end

[Kevin Buzzard]

To make import all work, run ./scripts/mk_all.sh in the mathlib root directory (or wait for someone else to come along and tell us what the right import is to make it work). I also suspect I'm doing it wrong and these instances should just work; I don't know much about real matrices in Lean.

[Eric Wieser]

I added all these instances quite recently, I'm a bit surprised you're seeing this weirdness

[Eric Wieser]

Do we not have docs#matrix.topological_add_group?

[Eric Wieser]

I guess I assumed it would unfold matrix for me, but that was silly

[Eric Wieser]

We should add it next to docs#matrix.has_continuous_add

[Eric Wieser]

... which we should also add, next to docs#matrix.has_continuous_smul

[Kevin Buzzard]

import topology.metric_space.algebra was the import I was missing -- needed for has_bounded_smul.has_continuous_smul.

[Eric Wieser]

It's not obvious to me why you need that instance

[Eric Wieser]

I would expect it to be found via docs#has_continuous_mul.to_has_continuous_smul

[Eric Wieser]

Oh come on, do we really have none of these?

[Eric Wieser]

Phew, just a bad name
docs#has_continuous_mul.has_continuous_smul

[Kevin Buzzard]

I posted the code above with the import all commented out and the instance just below; comment out the instance and the code stops compiling; add the import I suggest and it works again. Type class inference wanted a surprising instance of the form fin p1 -> continuous_smul R R or some such thing

[Aron Erben]

Thanks for your responses! Sorry for the delayed response on my part.

Kevin Buzzard said:

I just tried your code and it doesn't compile for me; I have complaints about X ⬝ β, Lean doesn't know what the dot is. Edit: aah, open_locale matrix fixes it

Yes, sorry, I sometimes have to redefine operators since for some reason some Unicode characters don't work on my Emacs. So for my MWEs, I remove the redefinitions again, but I forgot that people that don't have this problem have to open that module :grinning_face_with_smiling_eyes:

And thanks a bunch for your code! So the instances are done by unfolding the matrix into the definition with delta and then the apply_instance tactic finds such an instance in the current scope? (Is this what you meant @Alex J. Best? )

[Aron Erben]

Eric Wieser said:

Phew, just a bad name
docs#has_continuous_mul.has_continuous_smul

Can I use this somehow to not have to write out

instance : has_continuous_smul ℝ (matrix (fin p₁) unit ℝ) := by delta matrix; apply_instance

?

I imported topology.algebra.monoid(and omitted the "manual" instance), but it's still telling me

42:13: failed to synthesize type class instance for
...
⊢ has_continuous_smul ℝ (matrix (fin p₁) unit ℝ)

[Aron Erben]

Now I have

theorem t1 : β₁tilde = β₁caron :=
begin
  rw is_ols_coefficient at h₁,
  rw is_ols_coefficient at h₂,
  have a := is_min_on.of_is_local_min_of_convex_univ h₁ _,
  have b := is_min_on.of_is_local_min_of_convex_univ h₂ _,
 -- Uncomment to beta-reduce
  -- dsimp only [] at a,
  -- dsimp only [] at b,
end

With the state

n p₁ : ℕ,
Y : matrix (fin n) unit ℝ,
X₁tilde : matrix (fin n) (fin p₁) ℝ,
β₁tilde β₁caron : matrix (fin p₁) unit ℝ,
h₁ :
  is_local_min (λ (β : matrix (fin p₁) unit ℝ), ((Y - X₁tilde ⬝ β)ᵀ ⬝ (Y - X₁tilde ⬝ β)) () ())
    β₁tilde,
h₂ :
  is_local_min (λ (β : matrix (fin p₁) unit ℝ), ((Y - X₁tilde ⬝ β)ᵀ ⬝ (Y - X₁tilde ⬝ β)) () ())
    β₁caron,
a :
  ∀ (x : matrix (fin p₁) unit ℝ),
    (λ (β : matrix (fin p₁) unit ℝ), ((Y - X₁tilde ⬝ β)ᵀ ⬝ (Y - X₁tilde ⬝ β)) () ()) β₁tilde ≤
      (λ (β : matrix (fin p₁) unit ℝ), ((Y - X₁tilde ⬝ β)ᵀ ⬝ (Y - X₁tilde ⬝ β)) () ()) x,
b :
  ∀ (x : matrix (fin p₁) unit ℝ),
    (λ (β : matrix (fin p₁) unit ℝ), ((Y - X₁tilde ⬝ β)ᵀ ⬝ (Y - X₁tilde ⬝ β)) () ()) β₁caron ≤
      (λ (β : matrix (fin p₁) unit ℝ), ((Y - X₁tilde ⬝ β)ᵀ ⬝ (Y - X₁tilde ⬝ β)) () ()) x
⊢ β₁tilde = β₁caron

So I pretty much want to prove (in pseudo-Lean)

(∀ x, f β₁tilde ≤ f x) → (∀ x, f β₁caron ≤ f x) → β₁tilde = β₁caron

How would I go about proving this now? I've found docs#eq_of_forall_ge_iff, but that's not quite it...

[Yaël Dillies]

Is f injective?

[Yaël Dillies]

Your assumptions can easily prove f β₁tilde = f β₁caron.

[Aron Erben]

Yaël Dillies said:

Is f injective?

Hmmm, I'm not sure about this.

Your assumptions can easily prove f β₁tilde = f β₁caron.

How would I do that? And assuming it is injective, would I proceed with something like docs#set.inj_on.eq_iff?

[Yaël Dillies]

f β₁tilde ≤ f β₁caron and f β₁caron ≤ f β₁tilde by your assumptions.

[Yaël Dillies]

If hf : injective f and h : f β₁tilde = f β₁caron, then hf h : β₁tilde = β₁caron.

[Aron Erben]

Yaël Dillies said:

f β₁tilde ≤ f β₁caron and f β₁caron≤ f β₁tilde by your assumptions.

Oh yea, I was tunnel-visioning pretty hard... :face_palm:

[Alex J. Best]

Yaël Dillies said:

We have docs#matrix.topological_ring. Does your file import file#topology/instances/matrix ?

@Aron Erben I was observing that as you have different types for the rows and columns the matrices arent square and so won't form a ring, and the above quoted instance didn't seem to apply in your setting, something more specifically only additive is needed.

[Aron Erben]

Alex J. Best said:

Aron Erben I was observing that as you have different types for the rows and columns the matrices arent square and so won't form a ring, and the above quoted instance didn't seem to apply in your setting, something more specifically only additive is needed.

I was more referring to
Alex J. Best said:

Typeclass instance search should be filling in that sort of gap for you in most cases though

Specifically if Typeclass instance search meant the apply_instance tactic.

[Alex J. Best]

Oh sorry, right, apply instance is explicitly invoking typeclass search, but if you rewrite with or apply lemmas which have typeclass arguments, e.g. [monoid G]  then typeclass search is also run to get an instance of monoid G from ring G or whatever you have in context that "implies" the thing being searched for

[Alex J. Best]

So docs#topological_ring.to_topological_add_group isn't something that you as a user should have to look up and invoke specifically by name

[Alex J. Best]

Of course if the instance is missing then you can be a bit stuck, as typeclass search won't find it, so it is good to check things exist if Lean isn't filling in step we would expect it to.

[Aron Erben]

Ah I see, and in my case this didn't work because matrix a b c had to be unfolded into a -> b -> c before the lookup could happen (in this case explicitly with the apply_instance tactic)?

[Aron Erben]

(As there is a docs#pi.topological_add_group)

[Alex J. Best]

Yes exactly. But we should add these instances to mathlib for matrix, as Eric said, so future people don't have to unfold matrix to do stuff. Do you want to make a PR adding those instances?

[Aron Erben]

Cool, I get it now, thanks :) I'll gladly try my hand at adding them to mathlib!

[Aron Erben]

Yaël Dillies said:

If hf : injective f and h : f β₁tilde = f β₁caron, then hf h : β₁tilde = β₁caron.

I think I can't assume injectivity here. I think I have to work with global minima here, I'll try a proof by contradiction with convexity, maybe I can get that to work.