Smooth multiplication

Stream: new members

[Nicolò Cavalleri]

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]

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]

Does times_cont_diff_top help?

[Yakov Pechersky]

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

[Yakov Pechersky]

but one would need to show has_scalar F F

[Yakov Pechersky]

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

[Yakov Pechersky]

Or you might require a field structure on F

[Nicolò Cavalleri]

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

[Yakov Pechersky]

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

[Sebastien Gouezel]

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]

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]

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]

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

[Nicolò Cavalleri]

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