namespace http://mathhub.info/MitM/core/measures 

import base http://mathhub.info/MitM/Foundation 
import ts http://mathhub.info/MitM/core/typedsets 
import top http://mathhub.info/MitM/core/topology 
import arith http://mathhub.info/MitM/core/arithmetics 

theory SetAlgebra : base:?Logic = 
  include collections?Properties 
  include ☞base:?InformalProofs 

  prop_isSetAlgebra : {G : type} collection G ⟶ prop 
    = [G,C] prop_fullInColl C ∧ prop_closedUnderComplements C ∧ prop_finiteIntersection C 
	  # isSetAlgebra 2 
	  
	theory setAlgebra_theory : base:?Logic > X : type ❘ =
		include typedsets?SetCollection/setColl_theory (X) 
		axiom_full : ⊦ prop_fullInColl coll 
		axiom_finiteIntersection : ⊦ prop_finiteIntersection coll 
		axiom_complements : ⊦ prop_closedUnderComplements coll 
		lemma_finiteUnion : ⊦ prop_finiteUnion coll  = sketch "by de Morgan" 
		lemma_empty : ⊦ prop_emptyInColl coll  = sketch "$∅$ is the complement of $X$"  
	
	setAlgebra = [X : type] Mod ☞?SetAlgebra/setAlgebra_theory X 

    
theory SigmaAlgebra : base:?Logic = 
	include ☞collections?Properties 
	include ☞base:?InformalProofs 
	include ?SetAlgebra 
	
  prop_isSigmaAlgebra : {G : type} collection G ⟶ prop  
	  = [G,C] isSetAlgebra C ∧ prop_intersectionInColl C 
	  # isSigmaAlgebra 2 
	  
	theory sigmaAlgebra_theory : base:?Logic > X : type ❘ =
		include typedsets?SetCollection/setColl_theory (X) 
		
		axiom_intersection : ⊦ prop_intersectionInColl coll 
		lemma_union : ⊦ prop_unionInColl coll  = sketch "by de Morgan" 
		implicit structure setalgebra : ?SetAlgebra/setAlgebra_theory =
			coll = coll 
			axiom_finiteIntersection = sketch "special case of $axiom_intersection$" 
			lemma_finiteUnion = sketch "special case of $lemma_union$" 
		
	
	
	sigmaAlgebra = [X : type] Mod ☞?SigmaAlgebra/sigmaAlgebra_theory X 


theory Measurable : base:?Logic =
  include ☞ts:?Functions 
  include ?SigmaAlgebra 
  
	measurable : {A : type, B : type}{X : sigmaAlgebra A, Y : sigmaAlgebra B} (A ⟶ B) ⟶ prop 
	 = [A,B][X,Y,F] ∀[S] S ∈ (Y.coll) ⇒ (preim F S) ∈ (X.coll) 
	 # measurable 3 4 5 
	 

 
 
theory LebesgueMeasurable : base:?Logic =
	include ?Measurable 
	include ☞arith:?RealArithmetics 

  lebesgueMeasurableLeq : {A : type, s : sigmaAlgebra A} (A ⟶ ℝ) ⟶ bool 
  = [A,s,f] ∀[x : ℝ] ⟪ fullset A | ([i : A] (f i) ≤ x) ⟫ ∈ (s.coll) # lebesgueMeasurableLeq 2 3
  lebesgueMeasurableLt : {A : type, s : sigmaAlgebra A} (A ⟶ ℝ) ⟶ bool 
  = [A,s,f] ∀[x : ℝ] ⟪ fullset A | ([i : A] (f i) < x) ⟫ ∈ (s.coll) # lebesgueMeasurableLt 2 3
  lebesgueMeasurableGeq : {A : type, s : sigmaAlgebra A} (A ⟶ ℝ) ⟶ bool 
  = [A,s,f] ∀[x : ℝ] ⟪ fullset A | ([i : A] (f i) ≥ x) ⟫ ∈ (s.coll) # lebesgueMeasurableGeq 2 3
  lebesgueMeasurableGt : {A : type, s : sigmaAlgebra A} (A ⟶ ℝ) ⟶ bool 
  = [A,s,f] ∀[x : ℝ] ⟪ fullset A | ([i : A] (f i) > x) ⟫ ∈ (s.coll) # lebesgueMeasurableGt 2 3 


// MiKo: would like a view from topological spaces into Sigma Algebras that makes continuous functions measurable. ❚
// I don't understand - in general, sigma algebras aren't topologies... ❚
/T The BorelSigmaAlgebra is the smallest SigmaAlgebra that contains the collection of open sets. ❚
theory BorelSigmaAlgebra : base:?Logic = 
  include ☞ts:?LeastMost 
  include ?SigmaAlgebra 
  include topology?OpenSetTopology 
  
  borelsigmacoll : {A : type} collection A ⟶ collection A  = [A,C] least ([D] isSigmaAlgebra D ∧ (C ⊑ D)) (subset (set A))  # borelsigma 2
 //  axiom_closedundercomplements : {t : topologicalSpace} ⊦ prop_closedUnderComplements (borelsigma (topologyOf t)) ❙
 // axiom_closedunderintersections : {t : topologicalSpace} ⊦  prop_intersectionInColl (borelsigma (topologyOf t)) ❙
  borelSigma : {t : topologicalSpace} sigmaAlgebra (t.universe)  
    // = [t] ['
	  	  coll := borelsigma (topologyOf t) ,
	  	  axiom_full := (t.axiom_full) ,
	  	  axiom_intersection := axiom_closedunderintersections ,
	  	  axiom_complements := axiom_closedundercomplements
	'] 


theory BorelMeasurable : base:?Logic =
	include ?Measurable 
	include ?BorelSigmaAlgebra 
	include ☞top:?RealTopology 
	
	borelMeasurable : {A : type, t : topologicalSpace} sigmaAlgebra A ⟶ (A ⟶ t.universe) ⟶ prop   = [A,t,s,f] measurable s (borelSigma t) f 
	# borelMeasurable 1 2 3 4 
	
	realBorelMeasurable : {A : type} sigmaAlgebra A ⟶ (A ⟶ ℝ) ⟶ prop = [A,s,f] measurable s (borelSigma realTopologicalSpace) f
	
	lemma_realBorelMeasurableIsMeasurable