Zulip Chat Archive

Stream: new members

Topic: Smooth multiplication


view this post on Zulip Nicolò Cavalleri (Jul 30 2020 at 18:53):

Is it possible that this:

example : times_cont_diff   (λ x :  × , x.1 * x.2) :=
begin
  library_search,
end

is not present in mathlib?

view this post on Zulip Nicolò Cavalleri (Jul 30 2020 at 19:19):

In the description of the file times_cont_diff I find

/-
We also prove that the usual operations (addition, multiplication, difference, composition, and
so on) preserve `C^n` functions.
-/

but I can't really find it anywhere in the file

view this post on Zulip Yakov Pechersky (Jul 30 2020 at 19:39):

Does times_cont_diff_top help?

view this post on Zulip Yakov Pechersky (Jul 30 2020 at 19:44):

With something like

/-- The product of two `C^n`functions is `C^n`. -/
lemma times_cont_diff.smul {n : with_top } {f g : E  F}
  (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) : times_cont_diff 𝕜 n (λx, f x  g x) :=
begin
  have : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
  { apply is_bounded_linear_map.times_cont_diff,
    exact is_bounded_linear_map.smul is_bounded_linear_map.fst is_bounded_linear_map.snd },
  exact this.comp (hf.prod hg)
end

view this post on Zulip Yakov Pechersky (Jul 30 2020 at 19:45):

but one would need to show has_scalar F F

view this post on Zulip Yakov Pechersky (Jul 30 2020 at 19:45):

Which I think would be possible from normed_group F...

view this post on Zulip Yakov Pechersky (Jul 30 2020 at 19:46):

Or you might require a field structure on F

view this post on Zulip Nicolò Cavalleri (Jul 30 2020 at 19:48):

Sorry did you write that lemma or did you find it in the file? I don't see it!

view this post on Zulip Yakov Pechersky (Jul 30 2020 at 19:56):

I wrote that, but it doesn't work yet. It's broken.

view this post on Zulip Sebastien Gouezel (Jul 30 2020 at 19:56):

You have is_bounded_bilinear_map.times_cont_diff. But I think the consequence for products is not there, a big gap in the library!

view this post on Zulip Sebastien Gouezel (Jul 30 2020 at 19:57):

The historical reason is probably that I only wrote at first what is needed for manifolds, and taking products is not really useful for this. But of course it should be added!

view this post on Zulip Yakov Pechersky (Jul 30 2020 at 20:09):

For this, I need to somehow endow normed_group F with the property of normed_ring F, but normed_ring F does not assume normed_group F...

view this post on Zulip Heather Macbeth (Jul 30 2020 at 20:12):

You probably want to do [normed_ring F] [normed_algebra 𝕜 F].

view this post on Zulip Nicolò Cavalleri (Jul 30 2020 at 21:33):

I'll add it to my next PR then! I was just confused cause in the introduction you claimed it was in the file haha


Last updated: May 14 2021 at 07:19 UTC