namespace http://mathhub.info/MitM/core/calculus ❚

import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/core/typedsets ❚
import ms http://mathhub.info/MitM/core/measures ❚

theory SimpleFunctions : base:?Logic = 
	include ☞ms:?Measure ❙
	include ☞ts:?Functions ❙
	include ☞ms:?PowerSigmaAlgebra ❙
	include ☞ms:?BorelMeasurable ❙
//	include top:?RealTopology ❙
	
	
	prop_nonnegative_function : {A : type} (A ⟶ ℝ) ⟶ bool ❘= [A , f] ∀ [x : A] (0 : ℝ) ≤ ((f x) : ℝ) ❘# prop_nonnegative_function 2 ❙ 
	prop_simpleFunction  : {m : measurableSpace } (m.universe ⟶ ℝ) ⟶ bool 
	❘ = [m , f] (im f (fullset (m.universe))) finite ∧ 
	(∀ [x]  x ∈ im f (fullset m.universe) ⇒ preim f (single x)  ∈ (m.sigma_algebra.coll)) ❙
	
	simpleFunction : measurableSpace ⟶ type ❘= [m] Σ f : (m.universe ⟶ ℝ) . ⊦ prop_simpleFunction m f   ❙ 
	nonnegativeSimpleFunction : measurableSpace ⟶ type  ❘= [m] Σ f: (m.universe ⟶ ℝ) . ⊦ prop_simpleFunction m f  ∧ prop_nonnegative_function f ❙ 

	simpleFunctionIsMeasurable : {m1 : measurableSpace  , f : simpleFunction m1} ⊦ measurable (m1.sigma_algebra) (powerSigmaAlgebra ℝ) (πl f) ❙
	simpleFunctionIsBorelMeasurable : { m : measurableSpace , s : simpleFunction m} 
	⊦  realBorelMeasurable (m.universe) (m.sigma_algebra) (πl s) ❙
	
	
	theorem_simpleFunctionHasFiniteValues : {m : measurableSpace, S : simpleFunction m} ⊦ (im (πl S) (fullset (m.universe))) finite ❘# simpleFunctionHasFiniteValues 1 2 ❙
	theorem_nonnegativeSimpleFunctionHasFiniteValues : {m : measurableSpace, S : nonnegativeSimpleFunction m} ⊦ (im (πl S) (fullset (m.universe))) finite ❘# nonnegativeSimpleFunctionHasFiniteValues 1 2 ❙
	
	
❚