2020 05 07 Meeting - math-comp/analysis GitHub Wiki

quick summary about the branch mathcomp_master_sequence
- we limit ourselves to elementary results and will generalize later
  - elementary but using filters (epsilon-delta reasoning recovered with lemma cvg_normW)
what we put in milestone 0.3
- add https://github.com/math-comp/analysis/pull/196
  - to be merged by tomorrow
  - introduces the notion of locally bounded with notations such as [bound f x | x \in A] or [locally [bounded f x | x in A]]
  - notation for Lipschitz, e.g., k.-lipshitz_A f
  - implementation with the predicate dominated_by (whose generalization beyond normed spaces was discussed)
- add https://github.com/math-comp/analysis/pull/187 on sequences (see above and below)
- add add https://github.com/math-comp/analysis/pull/183
  - no need for Landau notations for most lemmas of this PR
  - Goal for later: Lipschitz continuity
temporary policy for merges
- merge even if results could be generalized but put a TODO in the code and an issue pointing at this TODO
discussion about the introduction of a metric layer (not now)
discussion about the integration of complexes
- already used in https://github.com/math-comp/analysis/pull/192 via real-closed
- TODO: in real-closed, give up on the canonical structures about modules
  - get rid of lmodtype (add it where needed to have a R-valued norm)
  - we should get rid of ^o (Marie to PR a version of mathcomp-analysis that does not use ^o)
  - should come as a fix for the issue https://github.com/math-comp/analysis/issues/156
revive https://github.com/math-comp/analysis/pull/119
- add uniform spaced between topological spaces et pseudometric spaces
- later: change pseudometric with balls to a pseudometric with a distance function
  - a structure with a distance evaluating to +oo might be bothersome
details about https://github.com/math-comp/analysis/pull/187 on sequences
- question about differential of inverse in derive.v
  - differential_Rinv has been updated
  - Cinv_continuous for complex numbers in normedtype.v
- poll about cvg vs. is_cvg (cvg wins)
- reminder about new namings
  - in particular, cvg_normW changed to cvg_distW, in anticipation of the introduction of a notation similar to | - _ |%N for ssrint once distances are introduced
- explain the definition of series
  - notation [normed series u_] that replaces the general term with its norm
- next step: uniform convergence
  - introduction a type of function bounded on a domain?
discussion about metrizable spaces
- metrizable spaces are uniform and lie between uniform and normed spaces
- ref: https://fr.wikipedia.org/wiki/Espace_vectoriel_topologique
You've been warned: don't use exact, done or by in Hint Extern, prefer solve[...]