Zulip Chat Archive
Stream: new members
Topic: Uniqueness of (global) minimum
Aron Erben (May 12 2022 at 14:52):
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 (May 12 2022 at 15:37):
I'm guessing I could do something with positive semi-definiteness to prove convexity here?
Yaël Dillies (May 12 2022 at 15:45):
Are you following a reference?
Aron Erben (May 12 2022 at 15:50):
@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 (May 12 2022 at 15:53):
Nono, that's what I meant. What function exactly are you trying to prove the convexity of?
Yaël Dillies (May 12 2022 at 15:53):
I assume you know about docs#convex_on, already?
Aron Erben (May 12 2022 at 19:01):
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 (May 12 2022 at 19:02):
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 (May 12 2022 at 19:07):
We have docs#matrix.topological_ring. Does your file import file#topology/instances/matrix ?
Aron Erben (May 12 2022 at 20:03):
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 (May 12 2022 at 20:05):
Ah, I just found docs#topological_ring.to_topological_add_group, that might be it
Alex J. Best (May 12 2022 at 20:06):
Typeclass instance search should be filling in that sort of gap for you in most cases though
Kevin Buzzard (May 12 2022 at 20:07):
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 (May 12 2022 at 20:07):
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 (May 12 2022 at 20:16):
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 (May 12 2022 at 20:17):
But I'm wondering whether really we're missing imports here or something?
Kevin Buzzard (May 12 2022 at 20:26):
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 (May 12 2022 at 20:27):
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 (May 12 2022 at 20:30):
I added all these instances quite recently, I'm a bit surprised you're seeing this weirdness
Eric Wieser (May 12 2022 at 20:31):
Do we not have docs#matrix.topological_add_group?
Eric Wieser (May 12 2022 at 20:31):
I guess I assumed it would unfold matrix
for me, but that was silly
Eric Wieser (May 12 2022 at 20:32):
We should add it next to docs#matrix.has_continuous_add
Eric Wieser (May 12 2022 at 20:32):
... which we should also add, next to docs#matrix.has_continuous_smul
Kevin Buzzard (May 12 2022 at 21:15):
import topology.metric_space.algebra
was the import I was missing -- needed for has_bounded_smul.has_continuous_smul
.
Eric Wieser (May 12 2022 at 21:21):
It's not obvious to me why you need that instance
Eric Wieser (May 12 2022 at 21:22):
I would expect it to be found via docs#has_continuous_mul.to_has_continuous_smul
Eric Wieser (May 12 2022 at 21:23):
Oh come on, do we really have none of these?
Eric Wieser (May 12 2022 at 21:24):
Phew, just a bad name
docs#has_continuous_mul.has_continuous_smul
Kevin Buzzard (May 12 2022 at 22:29):
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 (May 17 2022 at 08:13):
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 (May 17 2022 at 08:14):
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 (May 17 2022 at 11:31):
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 (May 17 2022 at 11:52):
Is f
injective?
Yaël Dillies (May 17 2022 at 11:53):
Your assumptions can easily prove f β₁tilde = f β₁caron
.
Aron Erben (May 17 2022 at 12:01):
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 (May 17 2022 at 12:04):
f β₁tilde ≤ f β₁caron
and f β₁caron ≤ f β₁tilde
by your assumptions.
Yaël Dillies (May 17 2022 at 12:04):
If hf : injective f
and h : f β₁tilde = f β₁caron
, then hf h : β₁tilde = β₁caron
.
Aron Erben (May 17 2022 at 12:06):
Yaël Dillies said:
f β₁tilde ≤ f β₁caron
andf β₁caron≤ f β₁tilde
by your assumptions.
Oh yea, I was tunnel-visioning pretty hard... :face_palm:
Alex J. Best (May 17 2022 at 12:07):
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 (May 17 2022 at 12:11):
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 (May 17 2022 at 12:19):
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 (May 17 2022 at 12:20):
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 (May 17 2022 at 12:21):
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 (May 17 2022 at 12:21):
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 (May 17 2022 at 12:24):
(As there is a docs#pi.topological_add_group)
Alex J. Best (May 17 2022 at 12:42):
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 (May 17 2022 at 12:54):
Cool, I get it now, thanks :) I'll gladly try my hand at adding them to mathlib!
Aron Erben (May 17 2022 at 13:36):
Yaël Dillies said:
If
hf : injective f
andh : f β₁tilde = f β₁caron
, thenhf 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.
Last updated: Dec 20 2023 at 11:08 UTC