IshYosh

C1 and lipschitz

3

##### Motivation for this change tentative definition C1 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers ##### Compatibility with...

Sometimes notation `_ @ _ --> _` is broken after `under eq_cvg` or `under eq_fun`. Here is my example. ```coq From HB Require Import structures. From mathcomp Require Import all_ssreflect...

I found some lemmas about `GRing.opp` which is named `opp_ ...` or `... _opp`, not `oppr_ ...` or `... _oppr`. I suppose these may be for distinguish between `GRing.opp` for...

##### Motivation for this change I added an alternative proof of gauss integral and placed it in theories/showcase. This is an experimental approach of improper integral. The difference of proof...

https://github.com/math-comp/analysis/blob/05898dcecc81e696b04dde8883718d54f2109990/theories/normedtype_theory/num_normedtype.v#L2 num_normedtype.v improted HB, but does not use HB.

name: `cvgeMl` -> `cvgeMr`?

3

https://github.com/math-comp/analysis/blob/11915720f13a33adf805e33dbfe17f01076e2460/theories/normedtype.v#L2747 https://github.com/math-comp/analysis/blob/11915720f13a33adf805e33dbfe17f01076e2460/theories/normedtype.v#L3105-L3106 I found a confusion of abbreviation `l` and `r`. I think that `cvgeMl` should be `cvgMr`, but I am not sure. NB(2025/04/21): the renaming of `cvgMr` is still...

##### Motivation for this change Some properties of `exp_coeff`. ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to...

##### Motivation for this change This is experimental generalization of monotone_convergence. - a sequence which is nondecreasing not for all n but over some N. - a sequence which is...

Generalize integration_by_parts

6

##### Motivation for this change Add a part of generalized version of integration by parts for unbound intervals `` `[a, +oo[ ``. This PR is over #1656 and #1662. I...

Lemmas `interval_set1` and `set_itv1` have identical statements. https://github.com/math-comp/analysis/blob/eed79156fac45c0aaa5d37aa047e89dbf4481f9c/classical/set_interval.v#L123 https://github.com/math-comp/analysis/blob/eed79156fac45c0aaa5d37aa047e89dbf4481f9c/classical/set_interval.v#L141