Iterated_fderiv lemmas

Stream: maths

[Moritz Doll]

For the Schwartz functions, I have to PR some calculations for iterated_fderivs (for example calculate the iterated_fderiv of a sum). I don't need the full generality, but this is obviously not the mathlib style. So I generalized to the following

lemma iterated_fderiv_within_add {n : ℕ} {f g : E → F} {s : set E} (hs : is_open s)
  (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
  ∀ (x : E) (hx : x ∈ s),
  iterated_fderiv_within 𝕜 n (λ y, f y + g y) s x =
  iterated_fderiv_within 𝕜 n f s x + iterated_fderiv_within 𝕜 n g s x :=
begin
  sorry,
end

but what I actually need is

lemma iterated_fderiv_add_apply {n : ℕ} {f g : E → F} {x : E} (hf : cont_diff 𝕜 n f)
  (hg : cont_diff 𝕜 n g):
  iterated_fderiv 𝕜 n (λ x, f x + g x) x = iterated_fderiv 𝕜 n f x + iterated_fderiv 𝕜 n g x :=
begin
  sorry,
end

Now the questions: is the first one sufficiently general? and do you want to have more 'trivial' lemmas in-between?
@Yury G. Kudryashov @Sebastien Gouezel

[Damiano Testa]

Mostly out of curiosity: can you replace the λ with f + g?

[Moritz Doll]

yes, that should be possible. At some point there were coercions there, this is why I had the λ

[Anatole Dedecker]

I have the proof

[Anatole Dedecker]

I have the proof

[Anatole Dedecker]

I’ll do it as soon as I get home

[Anatole Dedecker]

I needed the same things for distributions but I didn’t PR it

[Anatole Dedecker]

I have the proof

[Anatole Dedecker]

I needed the same things for distributions but I didn’t PR it

[Anatole Dedecker]

Whoops the subway mixed my messages

[Moritz Doll]

Shouldn't you only need differentiability for $C_c^\infty$? I need these because I actually have to estimate the derivative and for that reason I need only add, neg, and const_smul, but not sub.

[Moritz Doll]

I am curious to see your proofs as they are probably way better than mine (they are in #15850 if you are interested)

[Anatole Dedecker]

Here are my proofs (not guaranteed to work with current mathlib, but I can fix this) :

lemma iterated_fderiv_add {𝕜 E F : Type*} [nondiscrete_normed_field 𝕜]
  [normed_group E] [normed_group F] [normed_space 𝕜 E] [normed_space 𝕜 F]
  {nf ng : with_top ℕ} {i : ℕ} {f g : E → F} (hf : cont_diff 𝕜 nf f)
  (hg : cont_diff 𝕜 ng g) (hif : (i : with_top ℕ) ≤ nf)
  (hig : (i : with_top ℕ) ≤ ng) :
iterated_fderiv 𝕜 i (f + g) = (iterated_fderiv 𝕜 i f) + (iterated_fderiv 𝕜 i g) :=
begin
  induction i with i hi,
  { ext x, simp },
  { ext x h,
    have hif' : (i : with_top ℕ) < nf :=
      lt_of_lt_of_le (with_top.coe_lt_coe.mpr $ nat.lt_succ_self _) hif,
    have hig' : (i : with_top ℕ) < ng :=
      lt_of_lt_of_le (with_top.coe_lt_coe.mpr $ nat.lt_succ_self _) hig,
    have hdf : differentiable 𝕜 (iterated_fderiv 𝕜 i f) :=
      (cont_diff_iff_continuous_differentiable.mp hf).2 i hif',
    have hdg : differentiable 𝕜 (iterated_fderiv 𝕜 i g) :=
      (cont_diff_iff_continuous_differentiable.mp hg).2 i hig',
    calc iterated_fderiv 𝕜 (i+1) (f + g) x h
        = fderiv 𝕜 (iterated_fderiv 𝕜 i (f + g)) x (h 0) (fin.tail h) : rfl
    ... = fderiv 𝕜 (iterated_fderiv 𝕜 i f + iterated_fderiv 𝕜 i g) x (h 0) (fin.tail h) :
            by rw hi hif'.le hig'.le
    ... = (fderiv 𝕜 (iterated_fderiv 𝕜 i f) + fderiv 𝕜 (iterated_fderiv 𝕜 i g))
              x (h 0) (fin.tail h) :
            by rw [pi.add_def, fderiv_add hdf.differentiable_at hdg.differentiable_at]; refl
    ... = (iterated_fderiv 𝕜 (i+1) f + iterated_fderiv 𝕜 (i+1) g) x h : rfl }
end

lemma iterated_fderiv_smul {𝕜 E F : Type*} [nondiscrete_normed_field 𝕜]
  [normed_group E] [normed_group F] [normed_space 𝕜 E] [normed_space 𝕜 F]
  {nf : with_top ℕ} {i : ℕ} {a : 𝕜} {f : E → F} (hf : cont_diff 𝕜 nf f)
  (hif : (i : with_top ℕ) ≤ nf) :
iterated_fderiv 𝕜 i (a • f) = a • (iterated_fderiv 𝕜 i f) :=
begin
  induction i with i hi,
  { ext, simp },
  { ext x h,
    have hif' : (i : with_top ℕ) < nf :=
      lt_of_lt_of_le (with_top.coe_lt_coe.mpr $ nat.lt_succ_self _) hif,
    have hdf : differentiable 𝕜 (iterated_fderiv 𝕜 i f) :=
      (cont_diff_iff_continuous_differentiable.mp hf).2 i hif',
    calc iterated_fderiv 𝕜 (i+1) (a • f) x h
        = fderiv 𝕜 (iterated_fderiv 𝕜 i (a • f)) x (h 0) (fin.tail h) : rfl
    ... = fderiv 𝕜 (a • iterated_fderiv 𝕜 i f) x (h 0) (fin.tail h) :
            by rw hi hif'.le
    ... = (a • fderiv 𝕜 (iterated_fderiv 𝕜 i f)) x (h 0) (fin.tail h) :
            by rw [pi.smul_def, fderiv_const_smul hdf.differentiable_at]; refl
    ... = (a • iterated_fderiv 𝕜 (i+1) f) x h : rfl }
end

[Anatole Dedecker]

As you can see I have it only for iterated_fderiv, so that should definitely be generalized, but I also take care of the case where n is infinite (edit: this is stupid, I should read the statement I wrote before writing)

[Anatole Dedecker]

I think our proofs are fundamentally the same, and it is a shame that we have to do all this work, but at least mines are a bit structured (I actually thought it was much worse)

[Anatole Dedecker]

(Oh and sorry for the delay, I wasn't stuck in the subway, I just had to prepare some things because I'm flying back to France tomorrow)

[Anatole Dedecker]

Oh and what do you think about the (i : with_top ℕ) ≤ nf setup so that we don't have to use docs#cont_diff.of_le ? It was convenient in my case but I guess it would be more annoying in general, right ?

[Anatole Dedecker]

I've just opened #15902 with the core proofs adapted to the more general setup. I probably won't have a lot of time to finish the PR tomorrow, so feel free to add all the variants and take over the PR if you'd like it merged quickly

[Anatole Dedecker]

Moritz Doll said:

Shouldn't you only need differentiability for $C_c^\infty$? I need these because I actually have to estimate the derivative and for that reason I need only add, neg, and const_smul, but not sub.

Yes you don't need it to define the space. But the topology is defined by pulling back the topology on bounded continuous maps along each iterated_fderiv and then take the infimum, so you definitely want linearity to get a bunch of properties for free (TVS, locally convex, family of seminorms, ...)

[Moritz Doll]

Anatole Dedecker said:

I've just opened #15902 with the core proofs adapted to the more general setup. I probably won't have a lot of time to finish the PR tomorrow, so feel free to add all the variants and take over the PR if you'd like it merged quickly

Thanks, I've generalized the scalar multiplication and added the lemmas for iterated_fderiv.

[Moritz Doll]

Anatole Dedecker said:

Oh and what do you think about the (i : with_top ℕ) ≤ nf setup so that we don't have to use docs#cont_diff.of_le ? It was convenient in my case but I guess it would be more annoying in general, right ?

I don't have strong feelings about that. I might be very slightly in favor of having the strict condition (with i, not nf), because it saves you from using eq.le in some places.

[Moritz Doll]

Have a save flight.