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