Stream: new members

Topic: Smooth multiplication

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?

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

Yakov Pechersky (Jul 30 2020 at 19:39):

Does times_cont_diff_top help?

Yakov Pechersky (Jul 30 2020 at 19:44):

With something like

/-- The product of two C^nfunctions 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


Yakov Pechersky (Jul 30 2020 at 19:45):

but one would need to show has_scalar F F

Yakov Pechersky (Jul 30 2020 at 19:45):

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

Yakov Pechersky (Jul 30 2020 at 19:46):

Or you might require a field structure on F

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!

Yakov Pechersky (Jul 30 2020 at 19:56):

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

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!

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!

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...

Heather Macbeth (Jul 30 2020 at 20:12):

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

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