Commit fcc516d1 by SuperDuckDuck

parent 7a49c6b8
 namespace http://mathhub.info/MitM/smglom/arithmetics ❚ import base http://mathhub.info/MitM/Foundation ❚ // used as a return type in for the indicator function in indicatorFunction.mmt❚ theory ZeroOne : base:?Logic = include ?NaturalNumbers ❙ zeroOne : type ❘= ⟨ ℕ | [x] ⊦ x ≐ 1 ∨ x ≐ 0⟩ ❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import ar http://mathhub.info/MitM/smglom/arithmetics ❚ theory NullSets : base:?Logic = include ?Measure ❙ isNullSet : {m : measureSpace} set (m.universe) ⟶ bool ❘// slow! = [m , s] (s ∈ m.sigma_algebra.coll) ∧ (((m.measure.measure) (elem (m.sigma_algebra.coll) s)) ≐ 0)❙ allNullSets : {m : measureSpace} collection (m.universe) ❘// slow!= [m] ⟪ (m.sigma_algebra.coll) | ([s] (((m.measure.measure) (elem (m.sigma_algebra.coll) s)) ≐ 0))⟫ ❙ ❚ theory AlmostEverywhere : base:?Logic = include ?NullSets ❙ almostEverywhere : {m : measureSpace} ((m.universe) ⟶ bool) ⟶ bool ❘ = [m,P] ∃ [n] n ∈ (allNullSets m) ∧ (∀[x] x ∈ (fullset (m.universe) \ n) ⇒ P x)❘# AE 1 2❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/measures ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚ import exr http://mathhub.info/MitM/smglom/arithmetics ❚ import seq http://cds.omdoc.org/urtheories ❚ import desc http://mathhub.info/MitM/smglom/DescriptionOperators❚ theory LebesgueMeasure : base:?Logic = include ?Measure ❙ ❚ \ No newline at end of file
 ... ... @@ -47,9 +47,10 @@ theory Measure : base:?Logic = measurableSpace = {'universe : type , sigma_algebra : sigmaAlgebra universe '} ❙ // toMeasurableSpace : measureSpace ⟶ measurableSpace ❘ = [ms] ['universe := ms.universe , sigma_algebra := ms.sigma_algebra'] ❙ // toMeasureSpace : {ms: measurableSpace} measure (ms.universe) (ms.sigma_algebra) ⟶ measureSpace // very slow! toMeasureSpace : {ms: measurableSpace} measure (ms.universe) (ms.sigma_algebra) ⟶ measureSpace ❘// = [ms, m] ['universe := ms.universe , sigma_algebra := ms.sigma_algebra , measure := m'] ❙ isFiniteMeasure : measureSpace ⟶ bool ❘// slow! = [ms] (ms.measure.measure) (elem (ms.sigma_algebra.coll) (fullset (ms.universe))) < ∞❙ ❚ ... ...
 namespace http://mathhub.info/MitM/smglom/probability ❚ import base http://mathhub.info/MitM/Foundation ❚ import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚ // import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚ theory ProbabilityMeasure : base:?Logic = include measures?Measure ❙ ... ... @@ -22,6 +22,9 @@ theory ProbabilityMeasure : base:?Logic = theory ProbabilitySpaceTheorems : base:?Logic = include ?ProbabilityMeasure ❙ include measures?LebesgueIntegral ❙ include measures?Measurable ❙ include measures?LebesgueMeasurable ❙ theory probabilitySpaceTheorems_theory : base:?Logic > PS : probabilitySpace ❘ = ... ... @@ -29,17 +32,18 @@ theory ProbabilitySpaceTheorems : base:?Logic = omega = (PS.universe) ❘ # Ω ❙ probability : (typeof (set (PS.universe)) (PS.sigma_algebra.coll)) ⟶ ℝ ❘ // slow! = (PS.measure.measure) ❙ events : collection (PS.universe) ❘ // sometimes slow! = (PS.sigma_algebra.coll) ❙ currentMeasurespace : measureSpace ❘ # mspace ❙ // eventsSigmaAlgebra = (PS.sigma_algebra) ❙ // probabilityMeasure : measure Ω (eventsSigmaAlgebra) ❙ expectation : quasiIntegrableFunction mspace ⟶ ℝ ❙ variance : lebesgueIntegrableFunction mspace ⟶ ℝ ❙ // expectation : Ω ⟶ ⊦ quasiIntegrable ⟶ ℝ ❙ // variance : Ω ⟶ ℝ ❙ isRandomVariable : {A : type} ((PS.universe) ⟶ A) ⟶ sigmaAlgebra A ⟶ bool ❙ // slow ! randomVariable : {A : type} Σ t : (((PS.universe) ⟶ A) × sigmaAlgebra A) . ⊦ isRandomVariable A (πl t) (πr t) ❙ isRandomVariable : {A : type} ((PS.universe) ⟶ A) ⟶ sigmaAlgebra A ⟶ bool ❘ ❙ randomVariable : {A : type} Σ t : (((PS.universe) ⟶ A) × sigmaAlgebra A) . ⊦ isRandomVariable A (πl t) (πr t) ❙ isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ bool ❙ realValuedRandomVariable = Σ f: ((PS.universe) ⟶ ℝ) . ⊦ isRealValuedRandomVariable f ❙ isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ bool ❘= [f] ❙ realValuedRandomVariable = Σ f: ((PS.universe) ⟶ ℝ) . ⊦ isRealValuedRandomVariable f ❘# ℝRv ❙ // theorems ❙ ... ... @@ -48,5 +52,14 @@ theory ProbabilitySpaceTheorems : base:?Logic = lemma_probabilityGe1Eq1 : {x : set Ω} ⊦ 1 ≤ probability x ⟶ ⊦ probability x ≐ 1 ❙ ❚ ❚ theory bla : base:?Logic = ❚
 namespace http://mathhub.info/MitM/smglom/probability ❚ import base http://mathhub.info/MitM/Foundation ❚ import sets http://mathhub.info/MitM/smglom/typedsets ❚ import seqs http://mathhub.info/MitM/smglom/calculus ❚ // theory Vitali : base:?Logic = include sets:?AllSets ❙ include seqs:?Sequences ❙ vitaliSet : set ℕ❙ ❚ theory VitaliCoinToss : base:?Logic = include sets:?TypedSets ❙ include seqs:?Sequences ❙ include base:?DescriptionOperator ❙ vitaliSet : set (sequence ℕ) ❘= ⟪ (fullset (ℕ ⟶ ℕ)) | ([f] ∀[i] f i ≐ 0 ∨ f i ≐ 1) ⟫ ❙ flipOneZero : ℕ ⟶ ℕ ❘= [n] (if (n ≐ 1) then 0 else (if (n ≐ 0) then (1 : ℕ) else n))❙ flipAt : (sequence ℕ) ⟶ ℕ ⟶ (sequence ℕ) ❘= [oldSeq, n] [i : ℕ] (if (i ≐ n) then (flipOneZero (oldSeq i)) else (oldSeq i)) ❙ // vitaliTheorem : ⊦ (¬ (∃[P] )) ❙ ❚ \ No newline at end of file
 namespace http://mathhub.info/MitM/smglom/typedsets ❚ import base http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory IndicatorFunction : base:?Logic = include ?AllSets ❙ include arith:?NaturalNumbers ❙ indicatorFunction : {A : type} set A ⟶ A ⟶ ℕ ❘= [A,s,a] if (a ∈ s) then (1 : ℕ) else 0 ❘ ❙ ❚ \ 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!