Skip to content

Commit

Permalink
fix (#86)
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist authored Mar 31, 2024
1 parent 9c27a45 commit 64c94c7
Show file tree
Hide file tree
Showing 41 changed files with 2,431 additions and 2,431 deletions.
2 changes: 1 addition & 1 deletion analysis/htmldoc_1_1_0/mathcomp.analysis.Rstruct.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ <h2>Files</h2>
<h1 class="title">Module mathcomp.analysis.Rstruct</h1>
<br/>
<div class="ssrdoc md">
# Compatibility with the real numbers of Coq
# Compatibility with the real numbers of Coq
</div>
<br/>
<span class="vernacular">Require</span> <span class="vernacular">Import</span> <span class="id"><a href="https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Reals.Rdefinitions.html">Rdefinitions</a></span> <span class="id"><a href="https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Reals.Raxioms.html">Raxioms</a></span> <span class="id"><a href="https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Reals.RIneq.html">RIneq</a></span> <span class="id"><a href="https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Reals.Rbasic_fun.html">Rbasic_fun</a></span> <span class="id"><a href="https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.ZArith.Zwf.html">Zwf</a></span>.<br/>
Expand Down
84 changes: 42 additions & 42 deletions analysis/htmldoc_1_1_0/mathcomp.analysis.cantor.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,31 +93,31 @@ <h1 class="title">Module mathcomp.analysis.cantor</h1>
<span class="vernacular">From</span> <span class="id">HB</span> <span class="vernacular">Require</span> <span class="vernacular">Import</span> <span class="id"><a href="NOTFOUND the module url for HB.structures">structures</a></span>.<br/>
<br/>
<div class="ssrdoc md">
# The Cantor Space and Applications

This file develops the theory of the Cantor space, that is bool^nat with
the product topology. The two main theorems proved here are
homeomorphism_cantor_like, and cantor_surj, a.k.a. Alexandroff-Hausdorff.

```
cantor_space == the Cantor space, with its canonical metric
cantor_like T == perfect + compact + hausdroff + zero dimensional
tree_of T == builds a topological tree with levels (T n)
```

The overall goal of the next few sections is to prove that
Every compact metric space `T` is the image of the Cantor space.
The overall proof will build two continuous functions
Cantor space -&gt; a bespoke tree for `T` -&gt; `T`

The proof is in 4 parts:
- Part 1: Some generic machinery about continuous functions from trees.
- Part 2: All cantor-like spaces are homeomorphic to the Cantor space.
(an application of part 1)
- Part 3: Finitely branching trees are Cantor-like.
- Part 4: Every compact metric space has a finitely branching tree with
a continuous surjection. (a second application of part 1)

# The Cantor Space and Applications
This file develops the theory of the Cantor space, that is bool^nat with
the product topology. The two main theorems proved here are
homeomorphism_cantor_like, and cantor_surj, a.k.a. Alexandroff-Hausdorff.
```
cantor_space == the Cantor space, with its canonical metric
cantor_like T == perfect + compact + hausdroff + zero dimensional
tree_of T == builds a topological tree with levels (T n)
```
The overall goal of the next few sections is to prove that
Every compact metric space `T` is the image of the Cantor space.
The overall proof will build two continuous functions
Cantor space -&gt; a bespoke tree for `T` -&gt; `T`
The proof is in 4 parts:
- Part 1: Some generic machinery about continuous functions from trees.
- Part 2: All cantor-like spaces are homeomorphic to the Cantor space.
(an application of part 1)
- Part 3: Finitely branching trees are Cantor-like.
- Part 4: Every compact metric space has a finitely branching tree with
a continuous surjection. (a second application of part 1)
</div>
<br/>
<span class="gallina-kwd">Set</span> <span class="vernacular">Implicit</span> <span class="vernacular">Arguments</span>.<br/>
Expand Down Expand Up @@ -179,18 +179,18 @@ <h1 class="title">Module mathcomp.analysis.cantor</h1>
Qed.</div>
<br/>
<div class="ssrdoc md">
## Part 1

A tree here has countable levels, and nodes of type `K n` on the nth
level.
Each level is in the 'discrete' topology, so the nodes are independent.
The goal is to build a map from branches to X.
1. Each level of the tree corresponds to an approximation of `X`.
2. Each level refines the previous approximation.
3. Then each branch has a corresponding Cauchy filter.
4. The overall function from branches to X is a continuous surjection.
5. With an extra disjointness condition, this is also an injection

## Part 1
A tree here has countable levels, and nodes of type `K n` on the nth
level.
Each level is in the 'discrete' topology, so the nodes are independent.
The goal is to build a map from branches to X.
1. Each level of the tree corresponds to an approximation of `X`.
2. Each level refines the previous approximation.
3. Then each branch has a corresponding Cauchy filter.
4. The overall function from branches to X is a continuous surjection.
5. With an extra disjointness condition, this is also an injection
</div>
<span class="vernacular">Section</span> <span id="topological_trees" class="id"><a name="topological_trees" class="">topological_trees</a></span>.<br/>
<span class="vernacular">Context</span> <span class="id">{K</span> <span class="id">:</span> <span class="id"><a href="https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Init.Datatypes.html#nat">nat</a></span> <span class="id"><a href="https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x">-&gt;</a></span> <span class="id"><a href="mathcomp.analysis.topology.html#Topological.Exports.topologicalType">topologicalType}</a></span> <span class="id">{X</span> <span class="id">:</span> <span class="id"><a href="mathcomp.analysis.topology.html#Topological.Exports.topologicalType">topologicalType}</a></span><br/>
Expand Down Expand Up @@ -358,9 +358,9 @@ <h1 class="title">Module mathcomp.analysis.cantor</h1>
<span class="vernacular">End</span> <span class="id"><a href="mathcomp.analysis.cantor.html#topological_trees">topological_trees</a></span>.<br/>
<br/>
<div class="ssrdoc md">
## Part 2
We can use `tree_map_props` to build a homeomorphism from the
cantor_space to a Cantor-like space T.
## Part 2
We can use `tree_map_props` to build a homeomorphism from the
cantor_space to a Cantor-like space T.
</div>
<br/>
<span class="vernacular">Section</span> <span id="TreeStructure" class="id"><a name="TreeStructure" class="">TreeStructure</a></span>.<br/>
Expand Down Expand Up @@ -473,7 +473,7 @@ <h1 class="title">Module mathcomp.analysis.cantor</h1>
<span class="vernacular">End</span> <span class="id"><a href="mathcomp.analysis.cantor.html#TreeStructure">TreeStructure</a></span>.<br/>
<br/>
<div class="ssrdoc md">
## Part 3: Finitely branching trees are Cantor-like
## Part 3: Finitely branching trees are Cantor-like
</div>
<span class="vernacular">Section</span> <span id="FinitelyBranchingTrees" class="id"><a name="FinitelyBranchingTrees" class="">FinitelyBranchingTrees</a></span>.<br/>
<span class="vernacular">Context</span> <span class="id">{R</span> <span class="id">:</span> <span class="id"><a href="mathcomp.analysis.reals.html#Real.Exports.realType">realType}</a></span>.<br/>
Expand Down Expand Up @@ -505,7 +505,7 @@ <h1 class="title">Module mathcomp.analysis.cantor</h1>
<span class="vernacular">Local</span> <span class="vernacular">Notation</span> <span id="a3311973e1adc86e2f5588d86eb0b54d" class="id"><a name="a3311973e1adc86e2f5588d86eb0b54d" class="">&quot;A ^-1&quot;</a></span> <span class="id">:=</span> (<span class="id"><a href="mathcomp.classical.classical_sets.html#075f2dd209aa707f1415a58a026b96d9">[set</a></span> <span id="xy:104" class="id"><a name="xy:104" class="">xy</a></span> <span class="id"><a href="mathcomp.classical.classical_sets.html#075f2dd209aa707f1415a58a026b96d9">|</a></span> <span class="id">A</span> (<span class="id"><a href="mathcomp.analysis.cantor.html#xy:104">xy</a></span>.<span class="id">2,</span> <span class="id"><a href="mathcomp.analysis.cantor.html#xy:104">xy</a></span>.<span class="id">1</span>)<span class="id"><a href="mathcomp.classical.classical_sets.html#075f2dd209aa707f1415a58a026b96d9">]</a></span>) <span class="id">:</span> <span class="id">classical_set_scope</span>.<br/>
<br/>
<div class="ssrdoc md">
## Part 4: Building a finitely branching tree to cover `T`
## Part 4: Building a finitely branching tree to cover `T`
</div>
<span class="vernacular">Section</span> <span id="alexandroff_hausdorff" class="id"><a name="alexandroff_hausdorff" class="">alexandroff_hausdorff</a></span>.<br/>
<span class="vernacular">Context</span> <span class="id">{R</span> <span class="id">:</span> <span class="id"><a href="mathcomp.analysis.reals.html#Real.Exports.realType">realType}</a></span> <span class="id">{T</span> <span class="id">:</span> <span class="id"><a href="mathcomp.analysis.topology.html#PseudoMetric.Exports.pseudoMetricType">pseudoMetricType</a></span> <span class="id"><a href="mathcomp.analysis.cantor.html#R:105">R}</a></span>.<br/>
Expand Down
104 changes: 52 additions & 52 deletions analysis/htmldoc_1_1_0/mathcomp.analysis.charge.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,58 +94,58 @@ <h1 class="title">Module mathcomp.analysis.charge</h1>
<span class="vernacular">Require</span> <span class="vernacular">Import</span> <span class="id"><a href="mathcomp.analysis.esum.html">esum</a></span> <span class="id"><a href="mathcomp.analysis.measure.html">measure</a></span> <span class="id"><a href="mathcomp.analysis.realfun.html">realfun</a></span> <span class="id"><a href="mathcomp.analysis.lebesgue_measure.html">lebesgue_measure</a></span> <span class="id"><a href="mathcomp.analysis.lebesgue_integral.html">lebesgue_integral</a></span>.<br/>
<br/>
<div class="ssrdoc md">
# Charges

NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.

This file contains a formalization of charges (a.k.a. signed measures) and
their theory (Hahn decomposition theorem, etc.).

## Structures for functions on classes of sets
```
{additive_charge set T -&gt; \bar R} == notation for additive charges where
T is a semiring of sets and R is a
numFieldType
The HB class is AdditiveCharge.
{charge set T -&gt; \bar R} == type of charges over T a semiring of sets
where R is a numFieldType
The HB class is Charge.
isCharge == factory corresponding to the "textbook
definition" of charges
```

## Instances of mathematical structures
```
measure_of_charge nu nu0 == measure corresponding to the charge nu, nu0
is a proof that nu is non-negative
crestr nu mD == restriction of the charge nu to the domain D
where mD is a proof that D is measurable
crestr0 nu mD == csrestr nu mD that returns 0 for
non-measurable sets
czero == zero charge
cscale r nu == charge nu scaled by a factor r : R
charge_add n1 n2 == the charge corresponding to the sum of
charges n1 and n2
charge_of_finite_measure mu == charge corresponding to a finite measure mu
```

## Theory
```
nu.-positive_set P == P is a positive set with nu a charge
nu.-negative_set N == N is a negative set with nu a charge
hahn_decomposition nu P N == the full set can be decomposed in P and N,
a positive set and a negative set for the
charge nu
jordan_pos nu nuPN == the charge obtained by restricting the charge
nu to the positive set P of the Hahn
decomposition nuPN: hahn_decomposition nu P N
jordan_neg nu nuPN == the charge obtained by restricting the charge
nu to the positive set N of the Hahn
decomposition nuPN: hahn_decomposition nu P N
'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu
(the scope is charge_scope)
```

# Charges
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
This file contains a formalization of charges (a.k.a. signed measures) and
their theory (Hahn decomposition theorem, etc.).
## Structures for functions on classes of sets
```
{additive_charge set T -&gt; \bar R} == notation for additive charges where
T is a semiring of sets and R is a
numFieldType
The HB class is AdditiveCharge.
{charge set T -&gt; \bar R} == type of charges over T a semiring of sets
where R is a numFieldType
The HB class is Charge.
isCharge == factory corresponding to the "textbook
definition" of charges
```
## Instances of mathematical structures
```
measure_of_charge nu nu0 == measure corresponding to the charge nu, nu0
is a proof that nu is non-negative
crestr nu mD == restriction of the charge nu to the domain D
where mD is a proof that D is measurable
crestr0 nu mD == csrestr nu mD that returns 0 for
non-measurable sets
czero == zero charge
cscale r nu == charge nu scaled by a factor r : R
charge_add n1 n2 == the charge corresponding to the sum of
charges n1 and n2
charge_of_finite_measure mu == charge corresponding to a finite measure mu
```
## Theory
```
nu.-positive_set P == P is a positive set with nu a charge
nu.-negative_set N == N is a negative set with nu a charge
hahn_decomposition nu P N == the full set can be decomposed in P and N,
a positive set and a negative set for the
charge nu
jordan_pos nu nuPN == the charge obtained by restricting the charge
nu to the positive set P of the Hahn
decomposition nuPN: hahn_decomposition nu P N
jordan_neg nu nuPN == the charge obtained by restricting the charge
nu to the positive set N of the Hahn
decomposition nuPN: hahn_decomposition nu P N
'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu
(the scope is charge_scope)
```
</div>
<br/>
<span class="vernacular">Reserved</span> <span class="vernacular">Notation</span> <span class="id">&quot;{ 'additive_charge' 'set' T '-&gt;' '\bar' R }&quot;</span><br/>
Expand Down
Loading

0 comments on commit 64c94c7

Please sign in to comment.