fderiv and mv_polynomial

Stream: new members

[rtertr (Sonia)]

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]

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

[Moritz Doll]

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

[rtertr (Sonia)]

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]

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]

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

[rtertr (Sonia)]

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]

The D is allowed to depend on x, but not on i.

[rtertr (Sonia)]

oh, I thought D had to be a constant? :)

[Moritz Doll]

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]

Constants are overrated and usually depend on something :big_smile: