Skip to content

Commit

Permalink
test a few files
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Dec 8, 2023
1 parent 9119ba1 commit 77c5cc1
Show file tree
Hide file tree
Showing 5 changed files with 93 additions and 25 deletions.
26 changes: 17 additions & 9 deletions theories/landau.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
Require Import ereal reals signed topology normedtype prodnormedzmodule.

(******************************************************************************)
(* BACHMANN-LANDAU NOTATIONS : BIG AND LITTLE O *)
(******************************************************************************)
(******************************************************************************)
(***markdown*******************************************************************)
(* # Bachmann-Landau notations : big and little o *)
(* *)
(* F is a filter, K is an absRingType and V W X Y Z are normed spaces over K *)
(* alternatively, K can be equal to the reals R (from the standard library *)
(* for now) *)
Expand All @@ -33,6 +32,7 @@ Require Import ereal reals signed topology normedtype prodnormedzmodule.
(* using filter reasoning. *)
(* *)
(* Parsable notations: *)
(* ``` *)
(* [bigO of f] == recovers the canonical structure of big-o of f *)
(* expands to itself *)
(* f =O_F h == f is a bigO of h near F, *)
Expand All @@ -56,29 +56,37 @@ Require Import ereal reals signed topology normedtype prodnormedzmodule.
(* 'O == pattern to match a bigO with a generic F *)
(* f x =O_(x \near F) e x == alternative way of stating f =O_F e (provably *)
(* equal using the lemma eqOEx *)
(* ``` *)
(* *)
(* Printing only notations: *)
(* ``` *)
(* {O_F f} == the type of functions that are a bigO of f near F *)
(* 'a_O_F f == an existential bigO, must come from (apply: eqOE) *)
(* 'O_F f == a generic bigO, with a function you should not rely on, *)
(* but there is no way you can use eqOE on it. *)
(* ``` *)
(* *)
(* The former works exactly the same by with littleo instead of bigO. *)
(* *)
(* Asymptotic equivalence: *)
(* ``` *)
(* f ~_ F g == function f is asymptotically equivalent to *)
(* function g for filter F, i.e., f = g +o_ F g *)
(* f ~~_ F g == f == g +o_ F g (i.e., as a boolean relation) *)
(* ``` *)
(* --> asymptotic equivalence proved to be an equivalence relation *)
(* *)
(* Big-Omega and big-Theta notations on the model of bigO and littleo: *)
(* {Omega_F f} == the type of functions that are a big Omega of f near F *)
(* [bigOmega of f] == recovers the canonical structure of big-Omega of f *)
(* [Omega_F e of f] == returns a function with a bigOmega canonical structure *)
(* provably equal to f if f is indeed a bigOmega of e *)
(* or e otherwise *)
(* ``` *)
(* {Omega_F f} == the type of functions that are a big Omega of f *)
(* near F *)
(* [bigOmega of f] == recovers the canonical structure of big-Omega of f *)
(* [Omega_F e of f] == returns a function with a bigOmega canonical *)
(* structure provably equal to f if f is indeed a *)
(* bigOmega of e or e otherwise *)
(* f \is 'Omega_F(e) == f : T -> V is a bigOmega of e : T -> W near F *)
(* f =Omega_F h == f : T -> V is a bigOmega of h : T -> V near F *)
(* ``` *)
(* --> lemmas: relation with big-O, transitivity, product of functions, etc. *)
(* *)
(* Similar notations available for big-Theta. *)
Expand Down
45 changes: 34 additions & 11 deletions theories/measure.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ From mathcomp Require Import cardinality fsbigop .
Require Import reals ereal signed topology normedtype sequences esum numfun.
From HB Require Import structures.

(******************************************************************************)
(* Measure Theory *)
(***markdown*******************************************************************)
(* # Measure Theory *)
(* *)
(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. *)
(* *)
Expand All @@ -18,7 +18,8 @@ From HB Require Import structures.
(* - Daniel Li, Intégration et applications, 2016 *)
(* - Achim Klenke, Probability Theory 2nd edition, 2014 *)
(* *)
(* * Mathematical structures *)
(* ## Mathematical structures *)
(* ``` *)
(* semiRingOfSetsType d == the type of semirings of sets *)
(* The carrier is a set of sets A_i such that *)
(* "measurable A_i" holds. *)
Expand All @@ -33,8 +34,10 @@ From HB Require Import structures.
(* The HB class is AlgebraOfsets. *)
(* measurableType == the type of sigma-algebras *)
(* The HB class is Measurable. *)
(* ``` *)
(* *)
(* * Instances of mathematical structures *)
(* ## Instances of mathematical structures *)
(* ``` *)
(* discrete_measurable_unit == the measurableType corresponding to *)
(* [set: set unit] *)
(* discrete_measurable_bool == the measurableType corresponding to *)
Expand All @@ -57,10 +60,13 @@ From HB Require Import structures.
(* salgebraType G == the measurableType corresponding to <<s G >> *)
(* This is an HB alias. *)
(* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *)
(* ``` *)
(* *)
(* ## Structures for functions on classes of sets *)
(* *)
(* * Structures for functions on classes of sets *)
(* (There are a few details about mixins/factories to highlight *)
(* implementations peculiarities.) *)
(* ``` *)
(* {content set T -> \bar R} == type of contents *)
(* T is expected to be a semiring of sets and R a *)
(* numFieldType. *)
Expand Down Expand Up @@ -113,8 +119,10 @@ From HB Require Import structures.
(* of elements of type T : Type where R is *)
(* expected to be a numFieldType *)
(* The HB class is OuterMeasure. *)
(* ``` *)
(* *)
(* * Instances of measures *)
(* ## Instances of measures *)
(* ``` *)
(* pushforward mf m == pushforward/image measure of m by f, where mf is a *)
(* proof that f is measurable *)
(* \d_a == Dirac measure *)
Expand All @@ -140,8 +148,10 @@ From HB Require Import structures.
(* countable union *)
(* trivIset_closed G == the set of sets G is closed under pairwise-disjoint *)
(* countable union *)
(* ``` *)
(* *)
(* * Hierarchy of s-finite, sigma-finite, finite measures: *)
(* ## Hierarchy of s-finite, sigma-finite, finite measures: *)
(* ``` *)
(* sfinite_measure == predicate for s-finite measure functions *)
(* Measure_isSFinite_subdef == mixin for s-finite measures *)
(* SFiniteMeasure == structure of s-finite measures *)
Expand Down Expand Up @@ -195,14 +205,20 @@ From HB Require Import structures.
(* measure_is_complete mu == the measure mu is complete *)
(* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu, *)
(* declared as an instance of the type of filters *)
(* ``` *)
(* *)
(* # Measure Extension Theorem *)
(* *)
(* * From a premeasure to an outer measure (Measure Extension Theorem part 1) *)
(* From a premeasure to an outer measure (Measure Extension Theorem part 1): *)
(* ``` *)
(* measurable_cover X == the set of sequences F such that *)
(* - forall k, F k is measurable *)
(* - X `<=` \bigcup_k (F k) *)
(* mu^* == extension of the measure mu over a semiring of *)
(* sets (it is an outer measure) *)
(* * From an outer measure to a measure (Measure Extension Theorem part 2): *)
(* ``` *)
(* From an outer measure to a measure (Measure Extension Theorem part 2): *)
(* ``` *)
(* mu.-caratheodory == the set of Caratheodory measurable sets for the *)
(* outer measure mu, i.e., sets A such that *)
(* forall B, mu A = mu (A `&` B) + mu (A `&` ~` B) *)
Expand All @@ -213,23 +229,30 @@ From HB Require Import structures.
(* measure. *)
(* Remark: sets that are negligible for *)
(* this measure are Caratheodory measurable. *)
(* * Measure Extension Theorem: *)
(* ``` *)
(* Measure Extension Theorem: *)
(* ``` *)
(* measure_extension mu == extension of the content mu over a semiring of *)
(* sets to a measure over the generated sigma algebra *)
(* (requires a proof of sigma-sub-additivity) *)
(* ``` *)
(* *)
(* * Product of measurable spaces: *)
(* Product of measurable spaces: *)
(* ``` *)
(* preimage_classes f1 f2 == sigma-algebra generated by the union of the *)
(* preimages by f1 and the preimages by f2 with *)
(* f1 : T -> T1 and f : T -> T2, T1 and T2 being *)
(* measurableType's *)
(* (d1, d2).-prod.-measurable A == A is measurable for the sigma-algebra *)
(* generated from T1 x T2, with T1 and T2 *)
(* measurableType's with resp. display d1 and d2 *)
(* ``` *)
(* *)
(* ``` *)
(* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1 *)
(* ess_sup f == essential supremum of the function f : T -> R where T is a *)
(* measurableType and R is a realType *)
(* ``` *)
(* *)
(******************************************************************************)

Expand Down
8 changes: 6 additions & 2 deletions theories/reals.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,24 +5,27 @@
(* Copyright (c) - 2016--2018 - Polytechnique *)
(* -------------------------------------------------------------------- *)

(******************************************************************************)
(* An axiomatization of real numbers *)
(***markdown*******************************************************************)
(* # An axiomatization of real numbers *)
(* *)
(* This file provides a classical axiomatization of real numbers as a *)
(* discrete real archimedean field with in particular a theory of floor and *)
(* ceil. *)
(* *)
(* ``` *)
(* realType == type of real numbers *)
(* sup A == where A : set R with R : realType, the supremum of A when *)
(* it exists, 0 otherwise *)
(* inf A := - sup (- A) *)
(* ``` *)
(* *)
(* The mixin corresponding to realType extends an archiFieldType with two *)
(* properties: *)
(* - when sup A exists, it is an upper bound of A (lemma sup_upper_bound) *)
(* - when sup A exists, there exists an element x in A such that *)
(* sup A - eps < x for any 0 < eps (lemma sup_adherent) *)
(* *)
(* ``` *)
(* Rint == the set of real numbers that can be written as z%:~R, *)
(* i.e., as an integer *)
(* Rtoint r == r when r is an integer, 0 otherwise *)
Expand All @@ -32,6 +35,7 @@
(* range1 x := [set y |x <= y < x + 1] *)
(* Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x) *)
(* ceil x := - floor (- x) *)
(* ``` *)
(* *)
(******************************************************************************)

Expand Down
Loading

0 comments on commit 77c5cc1

Please sign in to comment.