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❙ 
❚