Looking for help with iteratedFDeriv and Taylor series

Stream: new members

[Stefan Kebekus]

Dear all,

I am trying to prove that iteratedFDeriv commutes with post-composition by continuous linear maps, but I am having severe difficulties understanding and navigating the API surrounding these notions. Any help is greatly appreciated!

Thanks -- Stefan.

variable
  {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]

theorem iteratedFDeriv_const_clm_apply
    {i n : ℕ} {c : F →L[𝕜] G} {x : E} {f : E → F} (hf : ContDiffAt 𝕜 n f x)
    (hi : i ≤ n) {x : E} {u : F}  :
    iteratedFDeriv 𝕜 i (c ∘ f) x = c ∘ (iteratedFDeriv 𝕜 i f x) := by
  sorry

[Sébastien Gouëzel]

Are you looking for docs#ContinuousLinearMap.iteratedFDeriv_comp_left ?

[Stefan Kebekus]

@Sébastien Gouëzel Aww! Shoot. I did not find that theorem, tried to come up with an inductive proof myself and got stuck in a mess.

Now this is embarrassing. Thank you for your help!

[Sébastien Gouëzel]

No problem. Finding theorems in the library is definitely hard, and asking on Zulip is one of the best ways I know!

[Sébastien Gouëzel]

A very good tool to find this kind of theorems is loogle (https://loogle.lean-lang.org/). You can ask it to state all theorems where something matches the form you're looking for, here it would be iteratedFDeriv _ _ (_ ∘ _).

We can even ask on Zulip:

@loogle iteratedFDeriv _ _ (_ ∘ _)

Hopefully among the answers there is the one you are looking for.

[loogle]

:search: iteratedFDeriv_comp, LinearIsometry.norm_iteratedFDeriv_comp_left, and 5 more

[Stefan Kebekus]

Thanks, Sébastien, for the hint. I knew loogle, but I was unaware of this useful syntax.