Summability of g ∘ f

Stream: Is there code for X?

[Michael Stoll]

Do we have something like the following?

import Mathlib

lemma summable_comp_of_summable_and_differentiableAt {f : ℕ → ℂ} {g : ℂ → ℂ}
    (hf : Summable fun x ↦ ‖f x‖) (hg : DifferentiableAt ℂ g 0) (h : g 0 = 0) :
    Summable (g ∘ f) := sorry

(or possibly in a more general version)
I can't find anything. So this is perhaps a nice challenge for our topologists :smile:
EDIT: added missing condition g 0 = 0.

[Junyan Xu]

Do you not need g 0 = 0?

[Patrick Massot]

Like Junyan, I have a counter-example.

[Junyan Xu]

The general assumption should be g(y) = O(y) as y->0, right

[Yury G. Kudryashov]

And we have docs#summable_of_isBigO_nat'

[Yury G. Kudryashov]

You can apply it to (hg : g =O[nhds 0] id).comp_tendsto (hf : Summable f).tendsto_atTop_zero

[Michael Stoll]

Junyan Xu said:

Do you not need g 0 = 0?

Yes, of course. I realized that after going to bed (it was late, and I was tired...). But I figured that whoever would attempt to prove it would realize that, too. I'm editing my first message to include it.

[Michael Stoll]

OK, thanks. What I have now is this.

open Topology in
lemma isBigO_id_of_differentiableAt {g : ℂ → ℂ} (hg : DifferentiableAt ℂ g 0) (hg₀ : g 0 = 0) :
    g =O[𝓝 0] id := by
  simp only [← hasDerivAt_deriv_iff, hasDerivAt_iff_isLittleO, hg₀, sub_zero, smul_eq_mul] at hg
  have H := Asymptotics.IsBigO.const_smul_left
    (Asymptotics.isBigO_refl (fun z : ℂ ↦ z) (𝓝 0)) <| deriv g 0
  convert Asymptotics.IsBigO.add_isLittleO H hg using 1
  simp only [Pi.smul_apply, smul_eq_mul, mul_comm (deriv _ _), add_sub_cancel'_right]

lemma summable_comp_of_summable_and_differentiableAt {f : ℕ → ℂ} {g : ℂ → ℂ}
    (hf : Summable f) (hg : DifferentiableAt ℂ g 0) (hg₀ : g 0 = 0) :
    Summable (g ∘ f) :=
  summable_of_isBigO_nat' hf <|
    (isBigO_id_of_differentiableAt hg hg₀).comp_tendsto hf.tendsto_atTop_zero

Is there a neater way to prove the first lemma? I'm just feeling around my way through this part of Mathlib...

[Yury G. Kudryashov]

#8352

[Yury G. Kudryashov]

I'm going to add IsBigO.comp_summable in another PR.

[Yury G. Kudryashov]

#8359