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