2020 09 04 Meeting - math-comp/analysis GitHub Wiki

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
• 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): investigate redundancy between summability.v and isum from measure_wip.v (branch integral_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 use mem
  • TODO(reynald): create a FAQ with an entry on using Boolean operators with Coq's Reals

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