2022 09 22 Meeting  mathcomp/analysis Wiki
Participants: Affeldt, Cohen, Roux, Stone

port to HB #698
 in
topology.v
: find a way to port
Definition product_topologicalType
 does not seem to require any special technique, should be a standard approach, i.e.,
define a symbol
product_...
which is aType
that is endowed with a canonical structure, etc.  TODO: Reynald to investigate in October
 does not seem to require any special technique, should be a standard approach, i.e.,
define a symbol
 non forgetful inheritance warning at line 3840
 is it related to the fact that the uniform topology does not depend on the topology of the domain?
 maybe no
 actually, this should be an error
isSource
was never intended to be a structure, it was a technical artifact rule of thumb: ignore the warning and leave an issue?
 TODO: Cyril to investigate
 is it related to the fact that the uniform topology does not depend on the topology of the domain?
Section RestrictedUniformTopology.
: might be connect to the non forgetful inheritance warninguniform_limit_continuous
and another one: ...
 find a way to port
 in
normedtype.v
: depends on product topology
 in

split packages classical #600 (this seems mostly ready, just waiting to happen)
 should be top priority
 we have added the split in nix and this should indeed be done first, the opam sync is easier
 PR not yet reviewed
 What do you do when the version is too low for the classical package to exist?
 it becomes a dummy package that does nothing (trick borrowed from MathComp)
 Cyril: would have wanted an error to be thrown. do not see where this is done in MathComp
 https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coqmodules/mathcomp/default.nix#L112
 it's a dummy package at the top not the bottom, it does introduce an extra dependency, it does not change the preexisting hierarchy
 this PR is orthogonal to the one HB but it might have a big impact
 TODO: merge what we have ASAP and try to improve later

PRs:
 https://github.com/mathcomp/analysis/pull/747
 easy one
 NB: no unfold before an intro
 https://github.com/mathcomp/analysis/pull/748
 more interesting
 problem with
R
and\bar R
: we want both theories for integral inR
and in\bar R
 go to Bochner integral and integral on R would be Bochner1?
 using a different notation would also make sense
Rintegral
is transitory and only exist because we do not have Bochner notation in ring_scope following the pattern for
` ... 
 notation in ring_scope following the pattern for
 Bochner needs a notion of dual space
 definition via a canonical embedding into a dual space
 we were waiting for HB to do that
 https://github.com/mathcomp/analysis/pull/737
 report a curiousness about a need to a structure whereas the mixin only is needed
 see isse #750
 Cyril:
 generalize [0,1] in
IsPath
 definition of path is not the right one
 composition of paths is not associative
 define path as a quotient up to remapping
 generalize [0,1] in
 use
generic_quotient
withsame_path_component
to define the equivalence relation
 reparametrization is an equivalence relation

 use that to build the canonical surjection

 define paths as point in the range of that space

 TODO: redefine paths
 Cyril: some proofs might shrink
 report a curiousness about a need to a structure whereas the mixin only is needed
 https://github.com/mathcomp/analysis/pull/674
 uniform space respected uniform and weak topology
 Cyril to review?
 https://github.com/mathcomp/analysis/pull/627
 not worth merging now
 https://github.com/mathcomp/analysis/pull/747