Zulip Chat Archive

Stream: maths

Topic: Iterated_fderiv lemmas


Moritz Doll (Aug 06 2022 at 21:24):

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 (Aug 06 2022 at 21:31):

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

Moritz Doll (Aug 06 2022 at 22:10):

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

Anatole Dedecker (Aug 07 2022 at 00:22):

I have the proof

Anatole Dedecker (Aug 07 2022 at 00:22):

I have the proof

Anatole Dedecker (Aug 07 2022 at 00:22):

I’ll do it as soon as I get home

Anatole Dedecker (Aug 07 2022 at 00:22):

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

Anatole Dedecker (Aug 07 2022 at 00:22):

I have the proof

Anatole Dedecker (Aug 07 2022 at 00:22):

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

Anatole Dedecker (Aug 07 2022 at 00:23):

Whoops the subway mixed my messages

Moritz Doll (Aug 07 2022 at 00:40):

Shouldn't you only need differentiability for CcC_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 (Aug 07 2022 at 00:42):

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 (Aug 07 2022 at 03:26):

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 (Aug 07 2022 at 03:27):

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 (Aug 07 2022 at 03:34):

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 (Aug 07 2022 at 03:35):

(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 (Aug 07 2022 at 03:46):

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 (Aug 07 2022 at 04:38):

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 (Aug 07 2022 at 04:40):

Moritz Doll said:

Shouldn't you only need differentiability for CcC_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 (Aug 07 2022 at 09:33):

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 (Aug 07 2022 at 09:42):

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 (Aug 07 2022 at 09:44):

Have a save flight.


Last updated: Dec 20 2023 at 11:08 UTC