math-comp/analysis

Issues

• useless type constraint

  #1357 opened a month ago by affeldt-aist
  0

• Use instance of realType once we get one

  #1355 opened a month ago by proux01
  0

• depency of `altreals` on `topology` and `ereal` not needed

  #1352 opened a month ago by affeldt-aist
  0

• Near message error

  #1320 opened 2 months ago by mkerjean
  2

• shouldn't this equivalence with suffixed with `P`?

  #1345 opened a month ago by affeldt-aist
  0

• duplicate line

  #1343 opened a month ago by affeldt-aist
  0

• `\oo` should be documented in `filter.v`

  #1342 opened a month ago by affeldt-aist
  1

• move `Require Import` to top of the file

  #1334 opened a month ago by affeldt-aist
  0

• Splitting normedmodtype.v

  #1339 opened a month ago by mkerjean
  0

• `setD_closed` and `setDI_closed`

  #1225 opened 6 months ago by affeldt-aist
  0

• generalize definitions introduced with Banach-Steinhaus PR

  #1310 opened 2 months ago by affeldt-aist
  0

• finitely-supported probability measure

  #1227 opened 6 months ago by affeldt-aist
  0

• variant of `measurable_fun_eqr`

  #1319 opened 2 months ago by affeldt-aist
  0

• split `lebesgue_measure.v`

  #1315 opened 2 months ago by affeldt-aist
  0

• add this lemma to `classical_orders.v` when dropping support for MathComp < 2.3

  #1336 opened a month ago by affeldt-aist
  0

• Broken in Coq CI

  #1333 opened a month ago by SkySkimmer
  6

• `maxeMr`: can be generalized to large inequality

  #1329 opened a month ago by affeldt-aist
  1

• Adding the infinite versions of lemmas such as `cvg_at_rightP` in `realfun.v`

  #1261 opened 2 months ago by Yosuke-Ito-345
  0

• status of the file `summability.v`

  #1284 opened 2 months ago by affeldt-aist
  2

• location of the definition of `expR`

  #1219 opened 2 months ago by affeldt-aist
  0

• missing lemma about `indic`

  #1317 opened 2 months ago by affeldt-aist
  0

• Should we make `not_near_at_rightP` an equivalence?

  #1273 opened 4 months ago by Yosuke-Ito-345
  2

• wrong documentation

  #1313 opened 2 months ago by affeldt-aist
  0

• unused `Reserved Notations` in `topology.v`?

  #1305 opened 2 months ago by affeldt-aist
  0

• numeric local notations not needed anymore

  #1308 opened 2 months ago by affeldt-aist
  0

• should be moved to the classical subdir

  #1307 opened 2 months ago by affeldt-aist
  0

• unneeded local notation

  #1309 opened 2 months ago by affeldt-aist
  0

• documentation of `\;` needs fixing

  #1301 opened 3 months ago by affeldt-aist
  0

• generalize `ge0_integral_closed_ball`

  #1299 opened 3 months ago by affeldt-aist
  0

• domain of function parameter can be genralized

  #1297 opened 3 months ago by affeldt-aist
  0

• duplicate use of `entourage_refl`?

  #1296 opened 3 months ago by affeldt-aist
  0

• `opp_ ...`, `... _opp` -> `oppr_ ...`, `... _ oppr`?

  #1292 opened 3 months ago by IshiguroYoshihiro
  0

• typo in `measure.v`

  #1277 opened 3 months ago by affeldt-aist
  1

• `to_set` -> `xsection`

  #1248 opened 3 months ago by affeldt-aist
  0

• `inf_lb` should be `inf_lbound`?

  #1258 opened 3 months ago by IshiguroYoshihiro
  3

• duplicate section

  #1270 opened 3 months ago by affeldt-aist
  0

• explicit dependency wrt Coq 8.20

  #1274 opened 3 months ago by affeldt-aist
  0

• Introducing cumulative distribution function to `Probability.v`

  #1260 opened 4 months ago by Yosuke-Ito-345
  0

• topology.(at_point, principal_filter) are the same

  #1268 opened 4 months ago by t6s
  0

• shouldn't `set_mem` actually be `mem_set`?

  #1269 opened 4 months ago by affeldt-aist
  0

• useless instantiation?

  #1253 opened 4 months ago by affeldt-aist
  0

• Missing subspace lemma on balls

  #1231 opened 5 months ago by CohenCyril
  1

• update using MathComp 1.17.0 naming convention

  #1241 opened 5 months ago by affeldt-aist
  0

• `inf_lower_bound` and `inf_lb`

  #1226 opened 5 months ago by affeldt-aist
  0

• typo in `functions.v`'s doc

  #1236 opened 5 months ago by affeldt-aist
  0

• dead code in `realfun.v`

  #1237 opened 5 months ago by affeldt-aist
  0

• rename the `misc` subdir to `showcase`

  #1233 opened 5 months ago by affeldt-aist
  1

• small generalization of Markov's lemma

  #1232 opened 5 months ago by affeldt-aist
  1

• naming

  #1229 opened 5 months ago by affeldt-aist
  1

• Countable product of measurable spaces

  #1214 opened 7 months ago by t6s
  0