-
Notifications
You must be signed in to change notification settings - Fork 43
2020 09 04 Meeting
affeldt-aist edited this page Sep 4, 2020
·
3 revisions
Participants: Marie, Cyril, Kazuhiko, Reynald
- postponed topics:
- about PR 180
- a quick check revealed an exposed match at line 2016
- the sort projection is unfolded to a match of
pseudoMetricNormedZmodule
- TODO: investigate:
type_of_filter
is the culprit?
- about PR 204 (Holomorphy)
- postpone until further input is available
- solution likely to rely on https://github.com/math-comp/real-closed/tree/complex_both_modules
- related work: https://github.com/zstone1/coq-complex
- about PR 180
- TODOs:
- about PR 205
- ideally, we would like to benefit from MathComp PR 546 (even though it should use primitive projections for class records)
- TODO(marie):
- test with Kazuhiko's branch 546
- or test with the snippet of code from https://github.com/math-comp/analysis/pull/205#discussion_r451816256
- about PR 224 (integral sketch)
- TODO(reynald): PR the new lemmas about sequences of extended
reals that are lingering at the top of
measure_wip.v
- TODO(reynald): PR the new lemmas about sequences of extended
reals that are lingering at the top of
- TODO(reynald): investigate redundancy between
summability.v
andisum
frommeasure_wip.v
(branchintegral_sketch_hb
) - TODO(marie): PR Banach-Steinhaus and Baire's theorems (https://github.com/tvignon/StageL3)
- the first goal is to integrate some notions into master (closed balls, fixes for working with floor, etc., density)
- reuse the notion of boundedness from master (instead of defining locally boundedness for linear functions)
- the statement of Baire's theorem can be improved
- TODO(marie): PR Hahn-Banach (https://github.com/math-comp/analysis/pull/179) into master
- TODO(reynald):
measure_wip.v
:set_of_interval
should usemem
- TODO(reynald): create a FAQ with an entry on using Boolean operators with Coq's Reals
- about PR 205
From Coq Require Import Reals.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrnum.
From mathcomp.analysis Require Import
boolp ereal reals posnum landau classical_sets Rstruct Rbar topology prodnormedzmodule normedtype.
Local Open Scope ring_scope.
Check (0 <= 1 :> R). (* (0 : R) <= (1 : R) : bool *)
- other topics:
- a file about cardinality appeared in the branch
integral_sketch_hb
https://github.com/math-comp/analysis/blob/030f36e2095b0e2ae1d7d59fb0c46bdfba42b7e4/theories/cardinality.v- in the future it should be better integrated with MathComp
- on the model of https://github.com/math-comp/analysis/pull/83
- lemmas about finite cardinals should be derived from MathComp (e.g., pigeonhole)
- for the time being, continue developing enough theory for Caratheodory and then PR to better integrate with MathComp
- no conflicting naming (
lte
prefix) with the new interval library
- a file about cardinality appeared in the branch