### more probability and measure theory

parent c8b9cf7e
No preview for this file type
No preview for this file type
No preview for this file type
No preview for this file type
No preview for this file type
No preview for this file type
No preview for this file type
No preview for this file type
No preview for this file type
 ... ... @@ -52,7 +52,7 @@ theory ProbabilityTheoryDefinitions : base:?Logic = theory RealValuedRandomVariables : base:?Logic > PS : probabilitySpace ❘ = include ?ProbabilityTheoryDefinitions/RandomVariables (PS) ❙ include measures?RealBorelMeasurableSpace ❙ include measures?RealBorelMeasurableSpace ❙ isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ prop ❘ = [f] isRandomVariable realBorelMeasurableSpace f❙ realValuedRandomVariable = randomVariable realBorelMeasurableSpace ❙ ... ...
 namespace http://mathhub.info/MitM/smglom/Probability ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import meas http://mathhub.info/MitM/smglom/measures ❚
 ... ... @@ -121,6 +121,6 @@ theory RealVectorspace : base:?Logic = realVec1 : realVec ❘ = asVectorspace realField ❘ # ℝ1 ❙ realVec2 : realVec ❘ // = productspace realField ℝ1 ℝ1 ❘ # ℝ2 ❙ realVec3 : realVec ❘ // = productspace realField ℝ1 ℝ2 ❘ # ℝ3 ❙ // takes forever ❙ // finite_real_vectorspace : pos_lit ⟶ RealVec ❙ finite_real_vectorspace : pos_lit ⟶ realVec ❙ // uncommented and changed by sw : why was this one commented out ❙ ❚
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import top http://mathhub.info/MitM/smglom/topology ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory SigmaOperator : base:?Logic = include ts:?AllSets❙ include ?SigmaAlgebra❙ bigF : {A : type} {Ω : set A} {M : set (set A)} ⊦ M ⊑ ( ℘ Ω) ⟶ set (set (set A)) ❘ = [A , O , M , h ] ⟪ ℘ (℘ O) | ([S : set (set A)] M ⊑ S ∧ isSigmaAlgebra S) ⟫ ❘# bigF 2 3 4 ❙ sigmaOperator : {A : type} {Ω : set A} {M : set (set A)} ⊦ M ⊑ (℘ Ω) ⟶ set (set A) ❘ = [A , O, M , h] INTERSECT (bigF O M h) ❘ # σ 2 3 4 ❙ // alt : generatorSigmaAlgebra ❙ ❚ theory SigmaOperatorTheorems : base:?Logic = include ?SigmaOperator ❙ theorem_sigmaOperator_1 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ M ⊑ σ O M h ❙ theorem_sigmaOperator_2 : {A : type} {O : set A} {O0 : set A} {M : set (set A)} {N : set (set A)} {h : ⊦ M ⊑ ℘ O} {h0 : ⊦ N ⊑ ℘ O0} ⊦ M ⊑ N ⟶ ⊦ σ O M h ⊑ σ O0 N h0❙ theorem_sigmaOperator_3 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ σ O M h ⊑ ℘ O ❙ theorem_sigmaOperator_4 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ σ O (σ O M h) (theorem_sigmaOperator_3 A O M h) ≐ σ O M h ❙ theorem_sigmaOperator_5 ❙ ❚ theory BorelExample : base:?Logic = ❚ theory bla : base:?Logic = ❚
 ... ... @@ -8,7 +8,7 @@ theory Countable : base:?InductiveTypes = include ?AllSets ❙ include natt:?InductiveNaturalNumbers ❙ prop_countableSet : {A : type} set A ⟶ prop ❘= [A,S] ∃ [f : setastype S ⟶ Nat] is_injective f ❘# is_countable 2 ❙ prop_countableSet : {A : type} set A ⟶ prop ❘= [A,S] ∃ [f : setastype S ⟶ INat] is_injective f ❘# is_countable 2 ❙ lemma_finiteSetIsCountable : {A : type} {s : set A} ⊦ s finite ⟶ ⊦ is_countable s ❙ ❚ ... ... @@ -17,7 +17,7 @@ theory CountablyInfinite : base:?InductiveTypes = include ?Countable ❙ include ?Bijective ❙ prop_countablyInfiniteSet : {A : type} set A ⟶ prop ❘= [A,S] ∃ [f : setastype S ⟶ Nat] is_bijective f ❘# is_countablyInfinite 2 ❙ prop_countablyInfiniteSet : {A : type} set A ⟶ prop ❘= [A,S] ∃ [f : setastype S ⟶ INat] is_bijective f ❘# is_countablyInfinite 2 ❙ lemma_countablyInfiniteSetsAreCountable : {A : type} {s : set A} ⊦ is_countablyInfinite s ⟶ ⊦ is_countable s ❙ ❚ ... ...
 ... ... @@ -17,5 +17,5 @@ theory FiniteSets : base:?Logic = theorem_setConsFinite : {A : type, s : set A , a : A} ⊦ s finite ⟶ ⊦ (s <- a) finite❙ theorem_setConsFiniteSplit : {A : type, s : set A , a : A } ⊦ (s <- a) finite ⟶ ⊦ s finite ❘ # setSpFin 2 3 4❙ // error , wenn keine notation dann fehle rin setsum -> bla ❙ theorem_setConsFiniteSplit : {A : type, s : set A , a : A } ⊦ (s <- a) finite ⟶ ⊦ s finite ❘ # setSpFin 2 3 4❙ // error , wenn keine notation dann fehler in setsum -> bla ❙ ❚ \ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!