partial derivatives

Stream: maths

[Kenny Lau]

namespace mv_polynomial

variables {σ : Type u} [decidable_eq σ]
variables {α : Type v} [comm_semiring α] [decidable_eq α]
variables (i j : σ) (p q : mv_polynomial σ α) (r : α)

def partial_deriv : mv_polynomial σ α :=
-- p.sum $ λ v r, C r * (add_monoid.smul (v i) (X i ^ (v i - 1)) * v.prod (λ j n, if i = j then 1 else (mv_polynomial.X j)^n))
p.sum $ λ v r, finsupp.single (v.sum $ λ j n, finsupp.single j (if i = j then n-1 else n)) (add_monoid.smul (v i) r)

-- #exit
theorem partial_deriv_add : (p + q).partial_deriv i = p.partial_deriv i + q.partial_deriv i :=
finsupp.sum_add_index (λ v, by rw [add_monoid.smul_zero, finsupp.single_zero]; refl) $
λ v a1 a2, by rw [add_monoid.smul_add, finsupp.single_add]

theorem partial_deriv_zero : (0 : mv_polynomial σ α).partial_deriv i = 0 :=
finsupp.sum_zero_index

theorem partial_deriv_C : (C r).partial_deriv i = 0 :=
(finsupp.sum_single_index $ by rw [add_monoid.smul_zero, finsupp.single_zero]; refl).trans $
by rw [finsupp.zero_apply, add_monoid.zero_smul, finsupp.single_zero]; refl

theorem partial_deriv_X : (X i : mv_polynomial σ α).partial_deriv j = if i = j then 1 else 0 :=
begin
  rw [partial_deriv, X, monomial, finsupp.sum_single_index, finsupp.sum_single_index, nat.sub_self, finsupp.single_apply],
  { split_ifs with hji hij hij,
    { rw [add_monoid.one_smul, finsupp.single_zero], refl },
    { exact absurd hji.symm hij },
    { exact absurd hij.symm hji },
    { rw [add_monoid.zero_smul, finsupp.single_zero], refl } },
  { split_ifs with hji,
    { rw [nat.zero_sub, finsupp.single_zero] },
    { rw finsupp.single_zero } },
  { rw [add_monoid.smul_zero, finsupp.single_zero], refl }
end

theorem partial_deriv_one : (1 : mv_polynomial σ α).partial_deriv i = 0 :=
by rw [← C_1, partial_deriv_C]

instance : semimodule α (mv_polynomial σ α) := finsupp.to_semimodule _ _

theorem C_mul'' : C r * p = r • p :=
begin
  refine finsupp.induction p _ _,
  { exact (mul_zero _).trans (smul_zero _).symm },
  { intros v s f hfv hs ih,
    rw [mul_add, smul_add, ih],
    rw [C, monomial, finsupp.mul_def, finsupp.sum_single_index, finsupp.sum_single_index, zero_add],
    rw [finsupp.smul_single, smul_eq_mul],
    { rw [mul_zero, finsupp.single_zero] },
    { rw [finsupp.sum_single_index]; rw [zero_mul, finsupp.single_zero] } }
end

theorem partial_deriv_smul : (r • p).partial_deriv i = r • p.partial_deriv i :=
begin
  rw [partial_deriv, finsupp.sum_smul_index', partial_deriv, ← C_mul'', finsupp.mul_sum], refine finset.sum_congr rfl _,
  { intros v hv, dsimp only, rw [add_monoid.smul_eq_mul, add_monoid.smul_eq_mul, mul_left_comm, ← smul_eq_mul, ← finsupp.smul_single, C_mul''] },
  { intros v, rw [add_monoid.smul_zero, finsupp.single_zero], refl }
end

theorem partial_deriv_mul : (p * q).partial_deriv i = p * q.partial_deriv i + q * p.partial_deriv i :=
begin
  have : ∀ v w : σ →₀ ℕ, w i ≠ 0 → finsupp.sum (v + w) (λ (j : σ) (n : ℕ), finsupp.single j (ite (i = j) (n - 1) n)) =
    v + finsupp.sum w (λ (j : σ) (n : ℕ), finsupp.single j (ite (i = j) (n - 1) n)),
  { intros v w hw, ext j,
    rw [finsupp.sum_apply, finsupp.add_apply, finsupp.sum_apply, finsupp.sum, finset.sum_eq_single j, finsupp.sum, finset.sum_eq_single j],
    { rw [finsupp.single_apply, finsupp.single_apply, if_pos rfl, if_pos rfl], split_ifs with hij,
      { subst hij, rw [finsupp.add_apply, nat.add_sub_assoc], exact nat.one_le_of_lt (nat.pos_of_ne_zero hw) },
      { refl } },
    { intros k hk hkj, rw [finsupp.single_apply, if_neg hkj] },
    { intros hjw, rw [finsupp.single_apply, if_pos rfl], split_ifs; rw [finsupp.not_mem_support_iff.1 hjw] },
    { intros k hk hkj, rw [finsupp.single_apply, if_neg hkj] },
    { intros hjw, rw [finsupp.single_apply, if_pos rfl], split_ifs; rw [finsupp.not_mem_support_iff.1 hjw] } },
  refine finsupp.induction p _ (λ v r p hpv hr ihp, _),
  { erw zero_mul, rw zero_add, erw partial_deriv_zero, rw mul_zero },
  rw [add_mul, partial_deriv_add], refine eq.trans (congr_arg _ ihp) _,
  rw [add_mul, partial_deriv_add, mul_add, add_comm₄], congr' 1,
  refine finsupp.induction q _ (λ w s q hqw hs ihq, _),
  { erw mul_zero, rw zero_add, erw zero_mul, rw partial_deriv_zero },
  rw [mul_add, partial_deriv_add], refine eq.trans (congr_arg _ ihq) _,
  rw [add_mul, partial_deriv_add, mul_add, add_comm₄], congr' 1,
  rw [finsupp.single_mul_single, finsupp.single_eq_smul_one v r, finsupp.single_eq_smul_one w s, finsupp.single_eq_smul_one (v+w) (r*s)],
  rw [partial_deriv_smul, partial_deriv_smul, partial_deriv_smul, ← C_mul'', ← C_mul'', ← C_mul'', ← C_mul'', ← C_mul''],
  rw [mul_comm₄, ← C_mul, mul_comm₄, ← C_mul, mul_comm s r, ← mul_add], congr' 1,
  rw [partial_deriv, finsupp.sum_single_index], swap, { rw [add_monoid.smul_zero, finsupp.single_zero], refl },
  rw [partial_deriv, finsupp.sum_single_index], swap, { rw [add_monoid.smul_zero, finsupp.single_zero], refl },
  rw [partial_deriv, finsupp.sum_single_index], swap, { rw [add_monoid.smul_zero, finsupp.single_zero], refl },
  rw [finsupp.add_apply, finsupp.single_mul_single, finsupp.single_mul_single, one_mul, one_mul],
  by_cases hv : v i = 0,
  { rw [hv, zero_add, add_monoid.zero_smul, finsupp.single_zero], erw add_zero,
    by_cases hw : w i = 0,
    { rw [hw, add_monoid.zero_smul, finsupp.single_zero, finsupp.single_zero] },
    { rw [this v w hw] } },
  by_cases hw : w i = 0,
  { rw [hw, add_monoid.zero_smul, finsupp.single_zero, add_zero], erw zero_add, rw [add_comm v w, this w v hv] },
  rw [add_monoid.add_smul, finsupp.single_add, add_comm], congr' 1,
  { rw this v w hw }, { rw [add_comm v w, this w v hv] }
end

theorem vars_add : (p + q).vars ⊆ p.vars ∪ q.vars :=
λ i, by unfold vars; simp only [finset.mem_union, multiset.mem_to_finset]; exact
λ hi, multiset.mem_add.1 (multiset.subset_of_le
  (le_trans (degrees_add p q) $ lattice.sup_le (multiset.le_add_right _ _) (multiset.le_add_left _ _)) hi)

theorem vars_mul : (p * q).vars ⊆ p.vars ∪ q.vars :=
λ i, by unfold vars; simp only [finset.mem_union, multiset.mem_to_finset]; exact
λ hi, multiset.mem_add.1 (multiset.subset_of_le (degrees_mul p q) hi)

theorem vars_X_subset : vars (X i : mv_polynomial σ α) ⊆ {i} :=
λ j hj, multiset.subset_of_le (degrees_X i) $ multiset.mem_to_finset.1 hj

theorem of_not_mem_vars (h : i ∉ p.vars) (v : σ →₀ ℕ) (hv : v ∈ p.support) : v i = 0 :=
finsupp.not_mem_support_iff.1 $ λ hiv, h $
have h1 : v.to_multiset ≤ p.degrees := finset.le_sup hv,
have h2 : _ ≤ v.to_multiset := finset.single_le_sum (λ _ _, multiset.zero_le _) hiv,
multiset.mem_to_finset.2 $ multiset.subset_of_le h1 $ multiset.subset_of_le h2 $
by rw ← nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero $ finsupp.mem_support_iff.1 hiv); exact
multiset.mem_cons_self _ _

theorem partial_deriv_of_not_mem_vars (h : i ∉ p.vars) : p.partial_deriv i = 0 :=
finset.sum_eq_zero $ λ v hv, by dsimp only; rw [of_not_mem_vars i p h v hv, add_monoid.zero_smul, finsupp.single_zero]; refl

end mv_polynomial

[Kenny Lau]

PR-ready?

[Johan Commelin]

Looks pretty good to me. Maybe C_mul'' can be called C_mul_eq_smul?

[Yury G. Kudryashov]

I've started thinking about a proper way to introduce partial derivatives into mathlib.

[Yury G. Kudryashov]

It's clear how to define pderiv for a function f : (fin n → k) → E

[Yury G. Kudryashov]

But this definition won't work, e.g., for f : k × k → E or f : k → E, and this doesn't sound good for a mathematician.

[Yury G. Kudryashov]

I suggest introducing something like

class has_canonical_basis (k : Type*) [normed_field k] (E : Type*) [normed_group E] [normed_space k E] :=
(σ : Type)
[hfin : fintype σ]
(iso : (σ → k) ≃L[k] E)

[Yury G. Kudryashov]

With instances for σ → k, euclidean_space, E × F (using σ = σE ⊕ σF), k (using σ = unit).

[Yury G. Kudryashov]

@Patrick Massot @Sebastien Gouezel What do you think?

[Johan Commelin]

We have the same problem in the omin repository. We introduced a has_coordinates typeclass.

[Johan Commelin]

@Reid Barton Do you think it is ready for PR?

[Johan Commelin]

(Of course it doesn't assume any normed* stuff. So we'll have to think whether it is good enough, or maybe you need some has_normed_coordinates extending it.

[Yury G. Kudryashov]

Actually, we can just upgrade from linear_equiv to continuous_linear_equiv using finiteness of σ.

[Yury G. Kudryashov]

Could you please post a link to your has_coordinates code?

[Johan Commelin]

https://github.com/rwbarton/lean-omin/blob/master/src/o_minimal/coordinates.lean

[Johan Commelin]

There is also Patrick's has_uncurry class in mathlib, which might be the right solution for your use case

[Yury G. Kudryashov]

No, it will uncurry f : k × k → E to k → k → E, not to (fin 2 → k) → E.

[Yury G. Kudryashov]

Or (unit ⊕ unit → k) → E

[Yury G. Kudryashov]

I would prefer to have any (σ : Type*) [fintype σ] as an index type, not necessarily fin n.

[Yury G. Kudryashov]

Because for E × F it's easier to deal with sum.inl k than some fin magic.

[Yury G. Kudryashov]

And I need coordinates to be linear. So, probably I'll add another typeclass.

[Sebastien Gouezel]

There is still the issue that, on $E \oplus F$, some people call partial derivative the derivative with respect to $E$ (so, it's not a number, it's really a matrix). But it is impossible to get a notion that covers all these variants, so I think your idea is a very nice one to cover one-dimensional partial derivatives.

[Yury G. Kudryashov]

We can mention that ∂f/∂x : E →L[k] G for f : E × F → G can be written as fderiv (λ x, f (x, y)).

[Sebastien Gouezel]

Yes, sure!

[Reid Barton]

In general, the problem is how to replace a given fin.dim. R-vector space with some fixed model R^ι (ι a finite type) or R^n in a conventional way. For some purposes the order of coordinates is irrelevant, and then R^ι is enough, but for other purposes the order really matters and you need R^n. For example, consider row reduction of the matrices that represent linear maps, or classifying subspaces by how they meet the standard flag inside R^n. Likewise in model theory, quantifier elimination works by eliminating one variable at a time, say, the "last" one, and for this it's again better to work with R^(n+1) than with fintypes. (Actually row reduction of matrices is basically a special case of this, I think.)

[Reid Barton]

So, unless we think it makes sense to have both concepts, I think the R^n version is better.

[Reid Barton]

Yury G. Kudryashov said:

Because for E × F it's easier to deal with sum.inl k than some fin magic.

With some version of the "reindexing" concept you can hide the details of exactly how the coordinates of (x, y) : E × F are related to those of x : E and y : F.

[Reid Barton]

The main advantage of a fintype version would be that you can have an instance for ι → R itself whose coordinates are given by the identity and so, in particular, the coordinates for (ι ⊕ ι') → R are related to those for ι → R and ι' → R specifically by composing with sum.inl and sum.inr. In lean-omin this has never come up because we have actually never had a use for specifically ι → R with [fintype ι]. But, you could have an instance which uses choice to pick an ordering on ι and uses it to define coordinates. In that case, there would be no specific relationship between the coordinates for (ι ⊕ ι') → R and ι → R and ι' → R. I claim this doesn't really matter because you can describe the coordinate change as a reindexing, anyways. However, probably a sensible thing to do would be to only have a global instance when ι is an instance of docs#fin_enum and then ensure that ι ⊕ ι' has a sensible fin_enum instance.

[Yury G. Kudryashov]

Is R^ι with a decidable_linear_order on ι any worse than fin n?

[Reid Barton]

Another consideration about the fintype version is that either you introduce a second universe variable, or in the ι → R instance you only handle ι in Type 0.

[Reid Barton]

It is worse because fin n has a bunch of API that is not conveniently available on an arbitrary finite decidable linear order, as well as somewhat better definitional behavior.

[Reid Barton]

(Also, conceptually the point of this whole construction is to reduce some problem/construction from general fin.dim. vector spaces to specific model spaces, so why stop at R^ι when you could go all the way to R^n?)

[Reid Barton]

Once you're working in this setting, the general objects are like (V : Type*) [has_coordinates R V] and the specific objects are like fin n -> R, so there's no longer any special significance to ι → R with [fintype ι].

[Reid Barton]

It only comes up if you have a [fintype ι] that comes from outside, so to speak. And then perhaps it would be better to have [fin_enum ι] which is basically the non-linear analogue of this setup.

[Yury G. Kudryashov]

OK, I'll try fin n. Thank you for the explanation.

[Reid Barton]

I should probably also add that in lean-omin this reindexing stuff is only ever used to prove Props, but you would probably also want to for example say what the partial derivatives of prod.fst : E \x F -> E are, so that might affect the design.

[Yury G. Kudryashov]

I'll just declare an instance on E × F using docs#equiv.sum_fin_sum_equiv.

[Patrick Massot]

@Sebastien Gouezel and @Yury G. Kudryashov what is the current status of partial derivatives and $C^k$ functions? Say for instance I have a $C^1$ function $F : E \times F \to G$. How am I meant to express that $\partial F/\partial e$ is a continuous function?

[Patrick Massot]

And how should I prove this? Is it already somewhere?

[Sebastien Gouezel]

$\partial F / \partial e$ is just the composition of $DF$ with the injection of $E$ in $E \times F$. I don't think we have a special notation for it (unless Yury has introduced something when doing the implicit function theorem, where this kind of thing is used all the time).

[Patrick Massot]

I had a look in the implicit function file, having exactly this idea in mind, but I didn't see anything relevant.

[Patrick Massot]

The continuity issue is related to the trichotomy of has_fderiv fderiv and times_cont_diff which complicates everything.

[Patrick Massot]

And actually I think what I needed when I posted this message was the continuity of $e \mapsto \partial F/\partial x(e, x_0)$ or something like this which makes things even more complicated in Lean (but still obvious on paper).

[Yury G. Kudryashov]

I did not introduce any notation. Probably you need something like docs#continuous_linear_map.compL with docs#continuous_linear_map.inl. To make things worse, you might need to use flip on compL.

Do other proof assistants have automation for things like this? How does it work?

[rtertr (Sonia)]

Hello everyone,
I am wondering how to work around the partial derivatives, since I realized they are not formalized. Under the Schwartz space page #analysis.schwartz_space they say they have defined rapid decay in such a way ‖x‖^k * ‖iterated_fderiv ℝ n f x‖ < C. This approach completely avoids using partial derivatives as well as polynomials.
I am just not sure how to work with x : fin d → ℝ then. As an undergraduate student, I am sure I have enough mathematical background to fully work around partial derivatives in Lean. I have yet to find a way to transform iterated_fderiv into something I can work with. In one dimension, I used that ‖(λ (x : ℝ), eval ↑x p * cexp (-a * ↑x ^ 2)) x‖ ≤ C.
Any help would be greatly appreciated as I am a bit stuck at the moment.
Kind regards,
Sonia

[Sophie Morel]

It probably depends on what you want to do with the partial derivatives. I may misunderstand the question, but I'll have a go.
If f is a function on $\mathbb{R}^k$ and $(e_1,\ldots,e_k)$ is the canonical basis, then iterated_fderiv R n f x will be a n-linear function on $\mathbb{R}^k$, let's call it $F_n(x)$. You can go between it and the partial derivatives by the formula:

$$\frac{\partial^n f}{\partial^{n_1}x_1\ldots\partial^{n_k}x_k}(x)=F_n(x)(e_1,\ldots,e_1,\ldots,e_k,\ldots,e_k),$$

where each basis element $e_i$ is repeated $n_i$ times, at least for f nice enough and if I didn't get confused in my indices. Here I am implicitly assuming that Schwartz's theorem holds, so it doesn't matter in which order I take the partial derivatives; this means that the iterated_fderiv R f n x should be a symmetric multilinear map if f is nice enough (one problem being to give optimal conditions on f for this to hold). I couldn't find that statement in mathlib, except for n=2 (see fderiv_symmetric); technically the case n=2 implies the general case but it might be a pain to prove.

[Patrick Massot]

Sonia, we need a more specific question to give you a more specific answer.

[Kevin Buzzard]

My students have been finding this issue as well. Basically there are vector spaces, and there is $\R^n$. If you work with $\R^n$ then you get concrete vectors (lists of numbers) and matrices and things. If you work with vector spaces then you get abstract vectors $v$ and linear maps. If you choose a basis then there's a dictionary between one language and the other. But mathlib prefers to not choose a basis if it can avoid doing so.

[Jireh Loreaux]

I also prefer to avoid choosing a basis, including when I'm teaching! :smiley:

[Moritz Doll]

I think the answer to the question "how do I prove that something is a Schwartz function" is to hold your breath until Sebastien's PR that gives API for the norms of iterated_fderiv exists.

[Moritz Doll]

You should also not work with fin d → ℝ, but with inner_product_space.

[Kevin Buzzard]

ie don't choose a basis :-)

[Moritz Doll]

yes, I wanted to give the answer to the question what is the correct level of generality.

[Sebastien Gouezel]

If you really want to work on this now, you could start from the branch #18643, in which I prove bounds for the n-th derivative of a composition. But note that this is not in mathlib master yet!

[rtertr (Sonia)]

Hello again everyone,
Thank you so much for your input :D
So to answer Patrick's question about more information: I am working with Stein & Shakarchi's book on Fourier Analysis, and specifically Chapter: The Fourier Transform on ℝ^d. I ideally want to formalize theorem 2.4. image.png
The norm needs to be Euclidean norm. And the derivative is defined as the following image.png thus I need to prove image.png.
Now, I am not sure how the the {n: N} ‖iterated_fderiv ℝ n f x‖ is equivalent to the multi-index β, or if I am misunderstanding this.
I was thinking I could just try to work with my own definition between the connection between iterated_fderiv R n f x and the partial derivative in defined in the book. But I would be nervous to build all of my work on a potentially incorrect definition :)

[rtertr (Sonia)]

Sophie Morel said:

$$\frac{\partial^n f}{\partial^{n_1}x_1\ldots\partial^{n_k}x_k}(x)=F_n(x)(e_1,\ldots,e_1,\ldots,e_k,\ldots,e_k),$$

Looks very similar, except for the norm at

$$partial^ |n| f$$

Sophie Morel said:

fderiv_symmetric

I could not find this in mathlib

[rtertr (Sonia)]

Kevin Buzzard said:

My students have been finding this issue as well.

What do you then tell them? Do they manage to work around it, or do they just not work further on it?
How do you not choose a basis?

[rtertr (Sonia)]

This is a little bit related, I was trying to perhaps switch from R^d to the euclidean norm space, and I was not allowed to apply cont_diff_norm_sq . I haven't tried with inner_product_space, I will try that later, but for now I am unsure why it is upset. Here is a #mwe

import data.nat.choose.sum
import data.complex.exponential
import analysis.normed_space.exponential
import analysis.special_functions.log.basic
import data.polynomial.basic
import data.polynomial.eval
import analysis.schwartz_space
import analysis.normed_space.exponential
import tactic
import topology.basic
import analysis.special_functions.log.base
import analysis.calculus.cont_diff
import analysis.calculus.iterated_deriv
import analysis.special_functions.exp_deriv
import number_theory.dioph
import analysis.complex.real_deriv
import analysis.special_functions.gaussian
import analysis.inner_product_space.calculus

open complex

lemma  complex.cont_diff_coe2  {d:ℕ } {f : ((fin d)→ ℝ)→ ℝ} (hf : cont_diff ℝ   ⊤ (λ (x : (fin d)→ ℝ  ), f x)): cont_diff ℝ ⊤ (λ y,  (f y : ℂ)) :=
begin
  apply cont_diff.comp _ hf,
  show cont_diff ℝ _ complex.of_real_clm,
  exact of_real_clm.cont_diff,
end


lemma  complex.cont_diff_coe2_euclid  {d:ℕ } {f : euclidean_space ℝ (fin d)→ ℝ} (hf : cont_diff ℝ   ⊤ (λ (x : euclidean_space ℝ (fin d)  ), f x)): cont_diff ℝ ⊤ (λ y,  (f y : ℂ)) :=
begin
  apply cont_diff.comp _ hf,
  show cont_diff ℝ _ complex.of_real_clm,
  exact of_real_clm.cont_diff,
end



def gaussian_complex  {d:ℕ } {a:ℂ} (ha:0<a.re): schwartz_map (fin d -> ℝ)   ℂ :=
  { to_fun := λ x : (fin d -> ℝ), complex.exp (-a * ‖x‖^2),
    smooth' :=
    begin
      refine cont_diff.comp _ _,
      apply cont_diff.cexp,
      exact cont_diff_id,
      refine cont_diff.mul _ _,
      exact cont_diff_const,
      norm_cast,
      refine complex.cont_diff_coe2 _,
      convert cont_diff_norm_sq,
    end,
    decay' := sorry,}



def gaussian_complex_euclidean_space  {d:ℕ } {a:ℂ} (ha:0<a.re): schwartz_map (euclidean_space ℝ (fin d))   ℂ :=
  { to_fun := λ x : (euclidean_space ℝ (fin d)), complex.exp (-a * ‖x‖^2),
    smooth' :=
    begin
      refine cont_diff.comp _ _,
      apply cont_diff.cexp,
      exact cont_diff_id,
      refine cont_diff.mul _ _,
      exact cont_diff_const,
      norm_cast,
      refine complex.cont_diff_coe2_euclid _,
      convert cont_diff_norm_sq,
    end,
    decay' := sorry,}

[Moritz Doll]

You would have an easier time if you follow the advise we are giving:

variables {E : Type*} [inner_product_space ℝ E]

lemma  complex.cont_diff_coe2_euclid {f : E → ℝ} (hf : cont_diff ℝ   ⊤ (λ (x : E), f x)): cont_diff ℝ ⊤ (λ y,  (f y : ℂ)) :=
begin
  apply cont_diff.comp _ hf,
  show cont_diff ℝ _ complex.of_real_clm,
  exact of_real_clm.cont_diff,
end

noncomputable
def gaussian_complex_euclidean_space  {a:ℂ} (ha:0<a.re): schwartz_map E ℂ :=
  { to_fun := λ x : E, complex.exp (-a * ‖x‖^2),
    smooth' :=
    begin
      refine cont_diff.comp _ _,
      apply cont_diff.cexp,
      exact cont_diff_id,
      refine cont_diff.mul _ _,
      exact cont_diff_const,
      norm_cast,
      exact complex.cont_diff_coe2_euclid cont_diff_norm_sq,
    end,
    decay' := sorry,}

[Moritz Doll]

fderiv_symmetric

I could not find this in mathlib

https://leanprover-community.github.io/mathlib_docs/analysis/calculus/fderiv_symmetric.html

[Moritz Doll]

If you really want to work on this now, you could start from the branch #18643, in which I prove bounds for the n-th derivative of a composition. But note that this is not in mathlib master yet!

I got too excited and proved the multiplication result for Schwartz functions: #18649

[Moritz Doll]

Composition should be very similar and if @rtertr (Sonia) does not object, then I will prove that as well.

[rtertr (Sonia)]

Hi Moritz, this looks very great! Interesting to see new tactics and way of doing proofs!
Now I have not looked too much at it yet, I will have more time tomorrow.
But when it comes to the bilinear proof, why is it not possible to do it by induction? :D
Also a proof of Composition would be great!
Kind regards, Sonia

[Moritz Doll]

It is certainly possible to prove everything by induction, but it is way more convenient to use general bounds for the iterated derivative. Half a year ago or so I've tried to use an the induction argument by hand and gave up because it is very messy, since iterated derivatives are so annoying to deal with. If you look at Sebastien's PR you will see what I mean.

[Moritz Doll]

After working a bit on the composition, I think it is easier in your case to use the bound on the iterated_fderiv for the composition directly, rather than using some theorem for Schwartz functions. The amount of hoops one has to jump through to get the Gaussian into a sensible composition is probably not worth the effort.

[rtertr (Sonia)]

Hi Moritz,
Was working a bit with updating my Lean.
Now, oddly enough, after updating, I run into issues with the inner_product_space.
Before it worked perfectly, but since I updated Lean, it is now unhappy:

import data.complex.basic
import data.nat.choose.sum
import data.complex.exponential
import analysis.normed_space.exponential
import analysis.special_functions.log.basic
import data.polynomial.basic
import data.polynomial.eval
import analysis.schwartz_space
import analysis.normed_space.exponential
import tactic
import topology.basic
import analysis.special_functions.log.base
import analysis.calculus.cont_diff
import analysis.calculus.iterated_deriv
import analysis.special_functions.exp_deriv
import number_theory.dioph
import analysis.complex.real_deriv
import analysis.special_functions.gaussian
import analysis.inner_product_space.calculus

variables {E : Type*} [inner_product_space ℝ E]

lemma  complex.cont_diff_coe2_euclid {f : E → ℝ} (hf : cont_diff ℝ   ⊤ (λ (x : E), f x)): cont_diff ℝ ⊤ (λ y,  (f y : ℂ)) :=
begin
  apply cont_diff.comp _ hf,
  show cont_diff ℝ _ complex.of_real_clm,
  exact complex.of_real_clm.cont_diff,
end

noncomputable
def gaussian_complex_euclidean_space  {a:ℂ} (ha:0<a.re): schwartz_map E ℂ :=
  { to_fun := λ x : E, complex.exp (-a * ‖x‖^2),
    smooth' :=
    begin
      refine cont_diff.comp _ _,
      apply cont_diff.cexp,
      exact cont_diff_id,
      refine cont_diff.mul _ _,
      exact cont_diff_const,
      norm_cast,
      exact complex.cont_diff_coe2_euclid cont_diff_norm_sq,
    end,
    decay' := sorry,}

[rtertr (Sonia)]

It now says

failed to synthesize type class instance for
E : Type u_1
⊢ normed_add_comm_group E

And if I add that, it asks for [normed_space ℝ E]. And if I add that, it no longer wants to apply

type mismatch at application
  complex.cont_diff_coe2_euclid cont_diff_norm_sq
term
  cont_diff_norm_sq
has type
  ∀ (𝕜 : Type ?) {E : Type ?} [_inst_1 : is_R_or_C 𝕜] [_inst_2 : normed_add_comm_group E]
  [_inst_3 : inner_product_space 𝕜 E] [_inst_6 : normed_space ℝ E] {n : ℕ∞},
    cont_diff ℝ n (λ (x : E), ‖x‖ ^ 2)
but is expected to have type
  cont_diff ℝ ⊤ (λ (x : E), ‖x‖ ^ 2)

[Eric Wieser]

Can you show the version after you "added that"?

[Kevin Buzzard]

Do you understand the current error? Just fix it.

[Kevin Buzzard]

Eric I think the issue now is simply that Sonia hasn't given k explicitly.

[Eric Wieser]

I would not expect adding [normed_space ℝ E] to be necessary

[Eric Wieser]

Or in other words, adding it would almost certainly be a mistake

[rtertr (Sonia)]

Eric Wieser said:

Can you show the version after you "added that"?

Like, I put as a condition on E.

lean
import data.complex.basic
import data.nat.choose.sum
import data.complex.exponential
import analysis.normed_space.exponential
import analysis.special_functions.log.basic
import data.polynomial.basic
import data.polynomial.eval
import analysis.schwartz_space
import analysis.normed_space.exponential
import tactic
import topology.basic
import analysis.special_functions.log.base
import analysis.calculus.cont_diff
import analysis.calculus.iterated_deriv
import analysis.special_functions.exp_deriv
import number_theory.dioph
import analysis.complex.real_deriv
import analysis.special_functions.gaussian
import analysis.inner_product_space.calculus


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

lemma  complex.cont_diff_coe2_euclid {f : E → ℝ} (hf : cont_diff ℝ   ⊤ (λ (x : E), f x)): cont_diff ℝ ⊤ (λ y,  (f y : ℂ)) :=
begin
  apply cont_diff.comp _ hf,
  show cont_diff ℝ _ complex.of_real_clm,
  exact complex.of_real_clm.cont_diff,
end

noncomputable
def gaussian_complex_euclidean_space  {a:ℂ} (ha:0<a.re): schwartz_map E ℂ :=
  { to_fun := λ x : E, complex.exp (-a * ‖x‖^2),
    smooth' :=
    begin
      refine cont_diff.comp _ _,
      apply cont_diff.cexp,
      exact cont_diff_id,
      refine cont_diff.mul _ _,
      exact cont_diff_const,
      norm_cast,
      exact complex.cont_diff_coe2_euclid cont_diff_norm_sq,
    end,
    decay' := sorry,}

[Kevin Buzzard]

docs#inner_product_space

[Kevin Buzzard]

Oh I don't know if the docs are up to date. This is a very recent change.

[Kevin Buzzard]

Have you posted the actual code you're running? inner_product_space shoudln't compile without normed_add_comm_group and in your posting you have them the wrong way around.

[Kevin Buzzard]

import analysis.schwartz_space
import analysis.inner_product_space.calculus

are the only imports you need by the way. Why are you importing all this other stuff?

[rtertr (Sonia)]

Yeah, I tend just to import at the thing I have open on my main file :D but it seems to still give the same issue. If I change the order, I still get the same issue:

lean
type mismatch at application
  complex.cont_diff_coe2_euclid cont_diff_norm_sq
term
  cont_diff_norm_sq
has type
  ∀ (𝕜 : Type ?) {E : Type ?} [_inst_1 : is_R_or_C 𝕜] [_inst_2 : normed_add_comm_group E]
  [_inst_3 : inner_product_space 𝕜 E] [_inst_6 : normed_space ℝ E] {n : ℕ∞},
    cont_diff ℝ n (λ (x : E), ‖x‖ ^ 2)
but is expected to have type
  cont_diff ℝ ⊤ (λ (x : E), ‖x‖ ^ 2)

It is just so odd because it used to work so smoothly :)

[Eric Wieser]

Kevin Buzzard said:

Oh I don't know if the docs are up to date. This is a very recent change.

They are up to date

[Kevin Buzzard]

@rtertr (Sonia) Yes but this is what happens when you upgrade mathlib, things change. It is not backwards compatible, so it's not odd. Read the error messge and fix the error.

[Eric Wieser]

It is just so odd because it used to work so smoothly :)

Mathlib changes quickly, you shouldn't expect code on an old version to work perfectly on a newer version.
However, this particular issue is trivial to fix, the error message is telling you everything you need to know

[rtertr (Sonia)]

Sorry I was gone for a few minutes. I tried to add it the conditions, but I unfortunately can't get it work quite, but I will try to talk with someone about in person this week :D