2020 05 07 Meeting

• 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[...]