analysis

analysis copied to clipboard

Missing canonical declaration in topology.v?

2

See [this line](https://github.com/math-comp/analysis/blob/3edd010fa7b101f449c6f364e0dfacb51b546496/theories/cauchyetoile.v#L196), for topological zmodtype.

amahboubi

Add closed sets to topological mixin

3

This issue was opened at the end of a discussion (at least with @CohenCyril) where we felt the need for an inclusion of closed sets as a field of the...

drouhling

I think there should be spec lemma for `bigO` to avoid these patterns: `have /bigOFP [_/posnumP[c1] kOg] := bigOP [bigO of k]`

CohenCyril

In `derive.v`, we should formalize the theorem that derive + continuous partial derivatives implies differentiability

mkerjean

Fix 'the_* landau notation to improve readability

1

- Make the notation f = g +o_e stable (e.g. by putting a definition) https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L199 - Remove the "'the" tag which makes things unreadable https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L135 ...

CohenCyril

want to use just `fct_ringType` from topology.v

1

There is a `ringType` decaration for function types in topology.v, which I have recently found useful for some projects (namely affeldt-aist/infotheo and ieva-itu/robustmean) with no topology. Unfortunately, importing topology conflicts...

t6s

WIP: eudoxus reals

4

Because it's fun.

strub

Banach fixed point theorem

3

##### Motivation for this change A generally useful result that doesn't require any machinery beyond geometric series. The proof is not too long, thankfully. 1. There is some nasty geometric...

zstone1

Separate Normed Module's ring and norm types

5

Long story short, I want to work with modules over the complex numbers, but have the norms live in the real numbers. Things like `infs` and `sups` are defined only...

zstone1

replacing strict inequality by a large one in locally_Rbar

5

CohenCyril