namespace http://mathhub.info/MitM/core/measures ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/core/typedsets ❚
import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚
import exr http://mathhub.info/MitM/core/arithmetics ❚
import seq http://cds.omdoc.org/urtheories ❚
import desc http://mathhub.info/MitM/core/DescriptionOperators❚
theory Additive : base:?Logic =
include arithmetics?ExtendedReals ❙
include collections?Properties ❙
prop_additive : {A : type}{F : collection A} (setastype F ⟶ ℝ) ⟶ bool ❘ # prop_Additive 2 3 ❘
// = [A,F,f] ∀[S]∀[T] disjoint X Y ⇒ f(X ∪ Y) ≐ f(X) + f(Y) ❙
// DM: conversion between sets and types needed to work properly ❙
❚
theory SigmaAdditive : base:?Logic =
include ☞ts:?Functions ❙
include ?SigmaAlgebra ❙
include arithmetics?ExtendedReals ❙
include calculus?Series ❙
prop_sigmaAdditive : {A : type}{F : collection A} (setastype F ⟶ ℝ) ⟶ bool ❘ # prop_sigmaAdditive 2 3 ❘
// = [A,F,f] ∀[S : sequence (setastype (F.coll))] pairwiseDisjoint (im S (fullset ℕ)) ⇒ f (elem (F.coll) (UNION (im S (fullset ℕ)))) ≐ SUM ([x : ℕ] f (S x)) ❙
// DM: conversion between sets and types needed to work properly ❙
❚
theory Measure : base:?Logic =
include ?SigmaAdditive ❙
include calculus?Series ❙
include ☞ts:?Functions ❙
theory measure_theory : base:?Logic > X : type , A : sigmaAlgebra X ❘ =
measure : setastype (A.coll) ⟶ ℝ ❘ # μ 1 prec 120 ❙
axiom_nonnegative : ⊦ ∀ [x] μ x ≥ 0 ❙
axiom_emptyiszero : ⊦ μ (elem (A.coll) ∅ ) ≐ 0 ❙
axiom_sigmaadditivity : ⊦ prop_sigmaAdditive (A.coll) measure ❙
❚
measure = [X : type, A : sigmaAlgebra X] Mod ☞?Measure/measure_theory X A ❙
measureSpace = {'
universe : type ,
sigma_algebra : sigmaAlgebra universe ,
rmeasure : measure universe sigma_algebra
'}❙
measurableSpace = {'universe : type , sigma_algebra : sigmaAlgebra universe '} ❙
// very slow! toMeasureSpace : {ms: measurableSpace} measure (ms.universe) (ms.sigma_algebra) ⟶ measureSpace
❘// = [ms, m] ['universe := ms.universe , sigma_algebra := ms.sigma_algebra , measure := m'] ❙
isFiniteMeasure : measureSpace ⟶ bool ❘// slow! = [ms] (ms.measure.measure) (elem (ms.sigma_algebra.coll) (fullset (ms.universe))) < ∞❙
❚
theory PowerSigmaAlgebra : base:?Logic =
include ?Measure ❙
prop_powersetIsSigmaAlgebra : type ⟶ bool ❘= [A] prop_isSigmaAlgebra A (powerset A (fullset A)) ❙
prop_fullInPowerset : {A : type} ⊦ prop_fullInColl (℘ (fullset A)) ❙ // (℘ (fullset A)) ❙
prop_finiteIntersectionPower : {A : type} ⊦ prop_finiteIntersection (℘ (fullset A)) ❙
prop_complementsPower : {A : type} ⊦ prop_closedUnderComplements (℘ (fullset A)) ❙
// lemma_finiteUnion : ⊦ prop_finiteUnion coll ❘ = sketch "by de Morgan" ❙
// lemma_empty : ⊦ prop_emptyInColl coll ❘ = sketch "$∅$ is the complement of $X$" ❙
prop_intersectionInPower : {A : type} ⊦ prop_intersectionInColl (℘ (fullset A)) ❙
powerSigmaAlgebra : {X : type} sigmaAlgebra X
❘ // = [X : type] [' setalgebra/axiom_complements := prop_complementsPower , coll := ℘ (fullset X), axiom_intersection := prop_intersectionInPower
, setalgebra/axiom_full := prop_fullInPowerset '] ❙
❚
theory CountingMeasure : base:?Logic =
include ?PowerSigmaAlgebra ❙
countingMeasureFunction : {X : type, A : sigmaAlgebra X} setastype (A.coll) ⟶ ℝ
❘// slow! = [A, S, s] if s finite then (| s | : ℝ) else ∞❙
countingMeasureFunction_nonnegative : {X : type, A : sigmaAlgebra X } ⊦ ∀ [x] (countingMeasureFunction X A) x ≥ 0❙
// slow! countingMeasure_emptyiszero : {A : type, S : sigmaAlgebra A} ⊦ (countingMeasureFunction A S) (elem (S.coll) ∅) ≐ 0 ❙
countingMeasure_sigmaadditivity : {A : type , S : sigmaAlgebra A} ⊦ prop_sigmaAdditive (S.coll) (countingMeasureFunction A S) ❙
countingMeasure : {X : type, A : sigmaAlgebra X} measure X A ❘ // = [X,A]
['
measure := (countingMeasureFunction X A) , axiom_nonnegative := countingMeasureFunction_nonnegative ,
axiom_emptyiszero := countingMeasure_emptyiszero , axiom_sigmaadditivity := countingMeasure_sigmaadditivity
'] ❙
countingMeasurableSpace : type ⟶ measurableSpace ❘ // slow! = [A] ['universe := A , sigma_algebra := powerSigmaAlgebra A']❙
countingMeasureSpace : type ⟶ measureSpace ❘ // slow! = [A] ['universe := A , sigma_algebra := powerSigmaAlgebra A , measure := countingMeasure A (powerSigmaAlgebra A) '] ❙
❚
theory NullSets : base:?Logic =
include ?Measure ❙
isNullSet : {m : measureSpace} set (m.universe) ⟶ bool ❘// slow! = [m , s] (s ∈ m.sigma_algebra.coll) ∧ (((m.measure.measure)
(elem (m.sigma_algebra.coll) s)) ≐ 0)❙
allNullSets : {m : measureSpace} collection (m.universe) ❘// slow!= [m] ⟪ (m.sigma_algebra.coll) | ([s] (((m.measure.measure)
(elem (m.sigma_algebra.coll) s)) ≐ 0))⟫ ❙
❚
theory AlmostEverywhere : base:?Logic =
include ?NullSets ❙
almostEverywhere : {m : measureSpace} ((m.universe) ⟶ bool) ⟶ bool ❘
= [m,P] ∃ [n] n ∈ (allNullSets m) ∧ (∀[x] x ∈ (fullset (m.universe) \ n) ⇒ P x)❘# AE 1 2❙
❚