# Zulip Chat Archive

## Stream: new members

### Topic: fderiv and mv_polynomial

#### rtertr (Sonia) (Apr 01 2023 at 18:44):

Hello everyone,

I am trying to somehow transform `‖fderiv ℝ (λ (y : E'), ↑‖y‖ ^ 2) x‖`

with `variables {E' : Type*} [normed_add_comm_group E'] [inner_product_space ℝ E'] `

into something I can work with. At best, I can transform it into `‖(fderiv ℝ coe (‖x‖ ^ 2)).comp (bit0 (⇑(innerSL ℝ) x))‖`

. Is there a way to transform it into a mv_polynomial, or something else? Or perhaps a way to show it is bounded by some norms dependent on `E' `

? Any ideas would help :)

#### Moritz Doll (Apr 02 2023 at 10:12):

I think it suffices to show that you can bound the derivative by the norm and (deleted nonsense).

#### Moritz Doll (Apr 02 2023 at 10:54):

Am I right in assuming that this is for proving the Schwartz function bound for the Gaussian?

#### rtertr (Sonia) (Apr 02 2023 at 13:32):

Hello again,

Yes, I am indeed still working on that :smiling_face_with_tear:

I guess I could have something like `‖fderiv ℝ (λ (y : E'), ↑‖y‖ ^ 2) x‖ < 1+‖x‖ ^ 2`

:thinking:

#### Moritz Doll (Apr 02 2023 at 13:52):

Having in mind that you want to apply this lemma from Sebastien's PR https://github.com/leanprover-community/mathlib/pull/18643/files#diff-1114505a9ffd6cfe324c241f491820d7cf97abc32c0894ade6b334af9e9ed929R2808

I would recommend on bounding the first derivative by `2 * (1+‖x‖)`

.

#### Moritz Doll (Apr 02 2023 at 14:06):

by the way, this is what we call an #xy problem

#### rtertr (Sonia) (Apr 02 2023 at 14:09):

I tried quite a bit with that lemma, but I concluded that since `∀ i, 1 ≤ i → i ≤ n → ‖iterated_fderiv 𝕜 i f x‖ ≤ D^i`

did not hold for `i=1`

when `f = ‖x‖^2`

then it would not really work.

But since I have `∃ (C : ℝ), ∀ (x : ?m_1), ‖↑‖x‖ ^ k * cexp (-a * ↑‖x‖ ^ 2)‖ ≤ C`

, I can make the proof work as long as I can show `‖fderiv ℝ (λ (y : E'), ↑‖y‖ ^ 2) x‖`

is bounded by some form of `summation a * ‖x‖^k`

, so for me it does not matter how big `k`

or `a`

is :)

#### Moritz Doll (Apr 02 2023 at 14:09):

The `D`

is allowed to depend on `x`

, but not on `i`

.

#### rtertr (Sonia) (Apr 02 2023 at 14:12):

oh, I thought `D`

had to be a constant? :)

#### Moritz Doll (Apr 02 2023 at 14:15):

if you look at the statement, first you have to give the theorem an `x`

and then an `D`

, so if you apply that theorem you choose `D`

according to you choice of `x`

.

#### Moritz Doll (Apr 02 2023 at 14:16):

Constants are overrated and usually depend on something :big_smile:

Last updated: Dec 20 2023 at 11:08 UTC