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 LebesgueIntegral : base:?Logic =
	include ☞ms:?Measure ❙
	include ☞ts:?Functions ❙
	include ☞ts:?SetCollection ❙
	include ?SimpleFunctions ❙
	include ☞ts:?SetSum ❙
	include ☞ts:?SupremumReal ❙
	include ☞ms:?LebesgueMeasurable ❙
	// include arith:?RealArithmetics ❙

  simpleLebesgueIntegral :  {m : measureSpace , s : nonnegativeSimpleFunction  m }  ℝ 
  ❘  = [m , s] setSum  ((im (πl s) (fullset (m.universe))) : set ℝ) 
  (theorem_nonnegativeSimpleFunctionHasFiniteValues m s) (([x] x ⋅ (m.rmeasure.measure) (elem (m.sigma_algebra.coll) (preim (πl s) (single x)))) : ℝ ⟶ ℝ) ❙
	
  upperFunction : {a : type} (a ⟶ ℝ) ⟶ a ⟶ ℝ ❘ =  [a , f , x ] max (f x) 0❙
  
  lowerFunction : {a : type} (a ⟶ ℝ) ⟶ a ⟶ ℝ ❘ =  [a : type, f : a ⟶ ℝ, x : a] max (- f x) 0  ❙
  
  lemma_upperFunctionIsNonNegative : {A : type , f : A ⟶ ℝ} ⊦ prop_nonnegative_function (upperFunction A f) 
  ❘# upperFunctionIsNonNegative 2❙
  
  lemma_lowerFunctionInNonNegative : {A : type , f : A ⟶ ℝ} ⊦ prop_nonnegative_function (lowerFunction A f)  
  ❘# lowerFunctionInNonNegative 2❙
  
 
	positiveLebesgueIntegral : {m : measureSpace, f : (m.universe ⟶ ℝ)} ⊦ lebesgueMeasurableLeq (m.sigma_algebra) f ⟶
	⊦ prop_nonnegative_function f  ⟶ ℝ 
	❘ = [m , f, p1,p2] supR ( im (simpleLebesgueIntegral m) ( ⟪ fullset (nonnegativeSimpleFunction m) | ([ff] (∀[x] ((πl ff) x) ≤ (f x))) ⟫ )) ❙

	
	lemma_lebesgueMeasurableFunctionUpperLebesgueMeasurable : 
	{A : type , s : sigmaAlgebra A, f : A ⟶ ℝ} ⊦ lebesgueMeasurableLeq s f ⟶ ⊦ lebesgueMeasurableLeq s (upperFunction A f)  
	❘ # lebesgueMeasurableFunctionUpperLebesgueMeasurable 2 3 4❙
	
	lemma_lebesgueMeasurableFunctionLowerLebesgueMeasurable : 
	{A : type , s : sigmaAlgebra A, f : A ⟶ ℝ} ⊦ lebesgueMeasurableLeq s f ⟶ ⊦ lebesgueMeasurableLeq s (lowerFunction A f)  
	❘# lebesgueMeasurableFunctionLowerLebesgueMeasurable 2 3 4❙
	
	lebesgueIntegrable : {ms : measureSpace, f : (ms.universe ⟶ ℝ)} ⊦ lebesgueMeasurableLeq (ms.sigma_algebra) f ⟶ bool
	❘ = [ms, f , p] positiveLebesgueIntegral ms (upperFunction (ms.universe) f) 
	(lebesgueMeasurableFunctionUpperLebesgueMeasurable (ms.sigma_algebra) f p) 
	(upperFunctionIsNonNegative f)
	< ∞ ∧ positiveLebesgueIntegral ms (lowerFunction (ms.universe) f) 
	(lebesgueMeasurableFunctionLowerLebesgueMeasurable (ms.sigma_algebra) f p) 
	(lowerFunctionInNonNegative f)
	< ∞ 
	❙

	quasiIntegrable : {ms : measureSpace , f : (ms.universe ⟶ ℝ)} ⊦ lebesgueMeasurableLeq (ms.sigma_algebra) f ⟶ bool 
	❘ = [ms, f , p] positiveLebesgueIntegral ms (upperFunction (ms.universe) f) 
	(lebesgueMeasurableFunctionUpperLebesgueMeasurable (ms.sigma_algebra) f p) 
	(upperFunctionIsNonNegative f)
	< ∞ ∨ positiveLebesgueIntegral ms (lowerFunction (ms.universe) f) 
	(lebesgueMeasurableFunctionLowerLebesgueMeasurable (ms.sigma_algebra) f p) 
	(lowerFunctionInNonNegative f)
	< ∞ 
	❙

	lebesgueIntegral : {m : measureSpace ,f : ((m.universe ⟶ ℝ)) , 
	p1 : ⊦ lebesgueMeasurableLeq (m.sigma_algebra) f}  ⊦  quasiIntegrable m f p1 ⟶ ℝ ❘  
	 = [m,f, p1 , p2] 
	(positiveLebesgueIntegral m (upperFunction (m.universe) f) 
	(lebesgueMeasurableFunctionUpperLebesgueMeasurable (m.sigma_algebra) f p1) 
	(upperFunctionIsNonNegative f) : ℝ) + 
	(- (positiveLebesgueIntegral m (lowerFunction (m.universe) f) 
	(lebesgueMeasurableFunctionLowerLebesgueMeasurable (m.sigma_algebra) f p1) 
	(lowerFunctionInNonNegative f) : ℝ))
	❙
	

❚