Hello, I have the following definition for "n times differentiable functions":

```
Fixpoint CPow (m: nat): set (U -> V) :=
match m with
| 0 => [set f: U -> V | continuous f]
| S m' => [set f | exists f' : U -> U -> V,
(forall x, is_diff x f (fun v => f' v x)) /\
(forall v, CPow m' (f' v))]
end.
```

Problem is, sometimes it unfolds in an ugly way (that is, it includes fixpoint) where I cannot fold `CPow`

back.

For example, I get

```
Cg : forall v : U,
(fix CPow (m : nat) : set (U -> R) :=
match m with
| 0%N => [set f | continuous f]
| m'.+1 =>
[set f | (exists f' : U -> U -> R,
(forall x : U, is_diff x f (f'^~ x)) /\
(forall v0 : U, CPow m' (f' v0)))]
end) m (g' v)
```

How can I prevent this?

Possibly related: In this case,

I have `f: fct_ringType U (numFieldNormedType.normedMod_ringType R)`

instead of conventional `f: U -> R`

.

Also as an alternative, is it possible to have idiomatic inductive proposition in ssreflect? How do I go with that?

Thanks in advance!

Can I cross-post this over #math-comp users ? It seems like traffic is relatively low here, and this could be reformulated into general question on inductive types & ssreflect.

please don't cross post in the Zulip.

Then, can I delete this one and post it over there?

it looks like your post asks about definitions to specific to MathComp Analysis. This means it belongs here, and we work actively to move topics to the most relevant stream.

so if you delete this post and ask the same elsewhere, I think it's obvious what will happen

It will not be the same form, as I will focus on how to use inductive definition in ssreflect.

feel free to ask new general MathComp questions in the math-comp users stream. But I suggest you don't use Analysis-specific code there.

Actually, it should be distinct enough for another thread. I have several definitions which would benefit from using inductive proposition, which should be fairly independent. Will not use analysis-specific code, including ones from `classical_sets`

.

abab9579 said:

Hello, I have the following definition for "n times differentiable functions":

`Fixpoint CPow (m: nat): set (U -> V) := match m with | 0 => [set f: U -> V | continuous f] | S m' => [set f | exists f' : U -> U -> V, (forall x, is_diff x f (fun v => f' v x)) /\ (forall v, CPow m' (f' v))] end.`

Hi! From a non technical (related to inductives) point of view, I wouldn't define this inductively, I would go for something like:

```
Definition CPow (m : nat) : set (U -> V) :=
[set f |continuous ('d^(n.+1) f) /\ forall n, n < m -> forall x, differentiable ('d^`(n) f) x].
```

for a suitable notion of $n^th$ Fréchet derivative `d^`

(n) f` (that is currently missing from the library) that you are leaving implicit in your recursion...

Thank you! I do not know how it would work, though. I would need to define tensors or multilinear functions, and then `continuous`

should work when image is a multilinear function space.

I'd love to see more linear algebra. We have several function space topologies available already, so I have some hole for this approach. What issues are you anticipating?

Just that I am somewhat daunted on this, as I am still a novice in coq & I expect tensors are quite a chore to implement.

~~By the way, would function space topologies work well in this case?~~ Just looked up frechet differential again, it is well-defined for bounded linear space.

Construction of tensor product on general vectorspace require quotient types. How can I do that?

Also, is there a reason why linear type is not given instances for zmodtype?

What do you call linear type precisely? (in which file is it defined for instance)

`{linear U -> V}`

, originally defined from `ssralg`

. Is it because defining instance in another module is intrusive?

Looks like `opp_fun`

(notation`\- f`

for `fun x => - (f x)`

) was added only recently so I guess nobody though about it but we could probably declare a zmodType on functions, with `\+`

(`add_fun`

) as additions and `\-`

(`opp_fun`

) as opposite. This would allow to use `addrA`

to rewrite `f \+ g\+ h`

into `f \+ (g \+ h)`

for instance, not sure if super useful. Note that linear is already stable by `\+`

and `\-`

(c.f., `add_fun_additive`

and `opp_fun_additive`

)

I see. Was curious as I am having problems with defining Lmodule structure for subtype of linear.

About quotient, maybe have a look at https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/generic_quotient.v and https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ring_quotient.v

I'm not sure what a zmodType structure on linear would mean. linear is itself a structure, rather than a type (like int, rat,...) to be equiped with structures.

Maybe you mean the subtype of functions that are linear?

I am defining a type which is subtype of `{linear U -> V}`

, that is, type of functions which is linear and have additional conditions.

For instance, bounded linear operators.

Then, indeed having a zmodtype on functions would make sense for you. You could then derive a subzmodtype on your subtype of functions that are linear + additional condition.

Do you want help to define the zmodType on functions? Anyway if you do it we would certainly welcome a pull request to add it to MathComp.

By now, I added zmodtype and lmodtype on `{linear U -> V}`

and derived these for subtypes as well. Was asking since I was afraid it might not be idiomatic. (Felt like I might be introducing inconsistent orphan instances)

I'd indeed be curious to have a quick look at your code if you don't mind.

(but the principle seems quite reasonable)

I am not good at programming so I ended up with this.

```
Section LinearZmod.
Context {R: ringType} (U V: lmodType R).
Implicit Types (u v : {linear U -> V}).
Definition linear_zero : {linear U -> V} := [linear of 0].
Definition linear_neg u := [linear of 0 \- u].
Definition linear_add u v := [linear of u \+ v].
Lemma linear_eq u v : (u: U -> V) = v -> u = v.
Proof. case: u v => [u +] [v +] /= Eq.
rewrite -{}Eq=> Hu Hu'. by have ->: Hu = Hu'.
Qed.
Lemma linear_assoc : associative linear_add.
Proof. move=> u v w. apply/linear_eq.
case: u v w => [u _] [v _] [w _] /=. apply/addrA.
Qed.
Lemma linear_comm : commutative linear_add.
Proof. move=> u v. apply/linear_eq.
case: u v => [u _] [v _] /=. apply/addrC.
Qed.
Lemma linear_add0r : left_id linear_zero linear_add.
Proof. move=> u. apply/linear_eq.
case: u => [u _] /=. apply/add0r.
Qed.
Lemma linear_addNr: left_inverse linear_zero linear_neg linear_add.
Proof. move=> u. apply/linear_eq.
case: u => [u _] /=. have ->: 0 \- u = \- u by apply/sub0r. apply/addNr.
Qed.
Definition linear_zmodMixin := ZmodMixin linear_assoc linear_comm linear_add0r linear_addNr.
Canonical linear_zmodType := ZmodType {linear U -> V} linear_zmodMixin.
End LinearZmod.
Section LinearLmod.
Context {R: comRingType} (U V: lmodType R).
Implicit Types (u v : {linear U -> V}).
Fact scale_linear (c: R) u : linear (c \*: u).
Proof. move=> b s t /=. rewrite linearP !scalerDr !scalerA.
by rewrite mulrC.
Qed.
Definition linear_scale (c: R) u := Linear (scale_linear c u).
Lemma linear_scalerA a b v : linear_scale a (linear_scale b v) = linear_scale (a * b) v.
Proof. apply/linear_eq. case: v=> [v _] /=. apply/scalerA.
Qed.
Lemma linear_scale1r : left_id 1 linear_scale.
Proof. move=> v. apply/linear_eq.
case: v=> [v _] /=. apply/scale1r.
Qed.
Lemma linear_scalerDr : right_distributive linear_scale +%R.
Proof. move=> c u v. apply/linear_eq.
case: u v=> [u _] [v _] /=. apply/scalerDr.
Qed.
Lemma linear_scalerDl v : {morph linear_scale^~ v: a b / a + b}.
Proof. move=> a b. apply/linear_eq.
case: v=> [v _] /=. apply/scalerDl.
Qed.
Definition linear_lmodMixin := LmodMixin linear_scalerA linear_scale1r linear_scalerDr linear_scalerDl.
Canonical linear_lmodType := LmodType R {linear U -> V} linear_lmodMixin.
End LinearLmod.
```

This code seems perfectly reasonable to me. Note that this would IMHO be a nice addition to mathcomp-analysis (not to mathcomp proper because it is a classical result), not sure in which file it should go though. @Reynald Affeldt or @Cyril Cohen any idea?

So I tried the definition through Frechet derivative - it did not require any tensors, it does seem to work out.

However, it did not suit my specific usecase: also working on functions `U -> R`

.

In detail, I need to use multiplication to describe derivation. Using frechet derivative makes proving relevant facts quite hard.

(E.g. product rule becomes ` 'd^() (f * g) x = f x *: 'd^() g x + g x *: 'd^() f x `

, then I need to deal with scales, which complicates stuffs)

If I'm understanding the setting correctly, does the ' *: ' unfold to the normal ' * ' on 'R'? It's not ideal, but some lemmas to support rewrites may help. A separate product rule on R that uses the more idiomatic '*' would be nice either way.

On the opposite extreme, I'm eager to define Banach algebras in HB, which should improve the ergonomics of this kind of multiplication a bit.

Differentiation of function `U -> V`

gives `U -> { bounded U -> V }`

.

For multiplication with `V := R`

, for `f : U -> R`

and `g : U -> R`

we have e.g. `df : U -> { bounded U -> R }`

so it has to be `d(f * g) x = (f x) *: (dg x) + (g x) *: (df x)`

. This cannot be changed.

To get induction step going, you need differentiation of such `*:`

. I am worried it might explode on order.

Hmm, how would banach space improve ergonomics of this multiplication? I am a bit lost.

Ah, I see. I'm looking at the `deriveM`

lemma, where a `rewrite /GRing.scale /=`

helps. What context is this coming up in? I'm mostly curious about what kind of deratives you need.

The Banach algebra point is that this formulation of product rule basically cheats. It _only_ works for R, and exploits scalar multiplication in a weird way. Ideally you'd write `d (f * g) x = df * g + f * dg`

, for some sensible notion of *. Apparently there's a better generalization regarding bilinear forms, so maybe I should do some more homework before I try to generalize this...

I just need to prove that multiplication of smooth functions is smooth. This is crucial for expressing product rule for derivations. (Ideally I should define germs and work on it, but that would take more effort. Still, that also needs multiplication)

So, I need to deal with "infinitely differentiable" on multiplication here.

I do not think Banach algebra would help with this. Inevitably, even if we do not restrict `R`

to be `realType`

, we still have `d(f * g) x = f x *: dg x + g x *: df x`

. Here, `dg x : { bounded U -> R }`

while `f x : R`

- the types just do not match. No kinds of multiplication would amend this difference.

I think this is just a quirk coming from frechet differentiation.

Wow, tensor product of normed spaces are finicky to deal with..

Last updated: Feb 05 2023 at 13:02 UTC