Zulip Chat Archive
Stream: Lean for the curious mathematician 2020
Topic: Friday afternoon
Johan Commelin (Jul 17 2020 at 10:57):
The next talk is starting in 4 minutes!
Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900
Meeting ID: 954 0208 5900
Password: 333537
Johan Commelin (Jul 17 2020 at 11:03):
Talk is starting!
Yury G. Kudryashov (Jul 17 2020 at 12:14):
I should've stated more explicitly that the exercise about iterated_deriv 7 is not supposed to be solved today.
Mario Carneiro (Jul 17 2020 at 12:47):
is there a proof that \lam f, f i is a continuous linear map somewhere?
Johan Commelin (Jul 17 2020 at 12:47):
continuous_pi_apply or something?
Mario Carneiro (Jul 17 2020 at 12:48):
I would guess the name proj instead of apply because the second argument is fixed rather than the first
Sebastien Gouezel (Jul 17 2020 at 12:49):
continuous_apply?
Mario Carneiro (Jul 17 2020 at 12:55):
that covers the continuous part, and linear_map.proj is the linear part
Yury G. Kudryashov (Jul 17 2020 at 13:05):
We also have is_bounded_bilinear_map_apply.
Yury G. Kudryashov (Jul 17 2020 at 13:05):
Sorry, it's about a different apply
Yury G. Kudryashov (Jul 17 2020 at 13:07):
Another missing lemma: derivative of ∏ i, f i.
Sebastien Gouezel (Jul 17 2020 at 13:08):
More generally, derivatives of continuous multilinear maps are missing I think.
Johan Commelin (Jul 17 2020 at 13:28):
The next talks starts in a couple of minutes!
Last updated: Dec 20 2023 at 11:08 UTC