Commit 745c560c by Sven Wille

probability and finsequences and inductively defined natural numbers

parent 6fdfc850
 namespace http://mathhub.info/MitM/smglom/Probability ❚ import base http://mathhub.info/MitM/Foundation ❚ import ts http://mathhub.info/MitM/smglom/typedsets ❚ // import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚ theory ProbabilityMeasure : base:?Logic = ... ... @@ -20,37 +21,52 @@ theory ProbabilityMeasure : base:?Logic = theory ProbabilitySpaceTheorems : base:?Logic = theory ProbabilityTheoryDefinitions : base:?Logic = include ?ProbabilityMeasure ❙ include calculus?LebesgueIntegral ❙ include measures?Measurable ❙ include measures?LebesgueMeasurable ❙ include measures?BorelMeasurable ❙ include ts:?Functions ❙ include ts:?FiniteCardinality ❙ theory probabilitySpaceTheorems_theory : base:?Logic > PS : probabilitySpace ❘ = theory BasicDefinitions : base:?Logic > PS : probabilitySpace ❘ = 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) ❙ // eventsSigmaAlgebra = (PS.sigma_algebra) ❙ // probabilityMeasure : measure Ω (eventsSigmaAlgebra) ❙ // expectation : Ω ⟶ ⊦ quasiIntegrable ⟶ ℝ ❙ // variance : Ω ⟶ ℝ ❙ 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 ❘// = [f] ❙ realValuedRandomVariable = ⟨ f: ((PS.universe) ⟶ ℝ) | ⊦ isRealValuedRandomVariable f ⟩ ❘# ℝRv ❙ eventsSigmaAlgebra = (PS.sigma_algebra) ❙ probabilityMeasure : measure Ω (eventsSigmaAlgebra) ❘ = PS.measure ❙ ❚ theory RandomVariables : base:?Logic > PS : probabilitySpace ❘ = include ?ProbabilityTheoryDefinitions/BasicDefinitions (PS) ❙ isRandomVariable : {ms : measurableSpace} ((PS.universe) ⟶ (ms.universe)) ⟶ bool ❘= [ms,X] measurable eventsSigmaAlgebra (ms.sigma_algebra) X ❙ randomVariable : measurableSpace ⟶ type ❘= [MS] ⟨ t : ((PS.universe) ⟶ (MS.universe)) | ⊦ isRandomVariable MS t ⟩ ❙ ❚ theory RealValuedRandomVariable : base:?Logic > PS : probabilitySpace ❘ = include ?ProbabilityTheoryDefinitions/RandomVariables (PS) ❙ // isRealValuedRandomVariable : ((PS.universe) ⟶ ℝ) ⟶ prop ❘ = [f] realBorelMeasurable (PS.universe) eventsSigmaAlgebra f❙ // realValuedRandomVariable = ⟨ f: ((PS.universe) ⟶ ℝ) | ⊦ isRealValuedRandomVariable f ⟩ ❘# ℝRv ❙ // bla : {A : type} randomVarixable A ⟶ set A❘ = [A,X] im X (fullset (PS.universe))❙ // isDiscreteRandomVariable : {A : type} randomVariable A ⟶ bool ❘ = [X] finite (image X (fullset (PS.universe))) ❙ // discreteRandomVariable ❙ // isDiscreteRealValuedRandomVariable ❙ ❚ // sw: this one has redundancy in it since the proof that X is quasiitegrable over PS and the borel measure space of ℝ covers that it is a realvalued random variable. I left it in (the constraint that X has to be a realValuedRandomVariable) since it makes it more clear what the expectation is ❙ // expectation : { X : realValuedRandomVariable } {XisLmes : ⊦ lebesgueMeasurableLeq (PS.sigma_algebra) X} ⊦ quasiIntegrable PS X XisLmes ⟶ ℝ ❘= [X,h,h0]lebesgueIntegral PS X h h0❙ // variance : ❙ // theorems ❙ // lemma_probabilityLe1 : ⊦ ∀[x : set Ω] probability x ≤ 1 ❙ lemma_omegaNotEmpty : ⊦ fullset Ω ≠ ∅ ❙ // lemma_omegaNotEmpty : ⊦ fullset Ω ≠ ∅ ❙ // lemma_probabilityGe1Eq1 : {x : set Ω} ⊦ 1 ≤ probability x ⟶ ⊦ probability x ≐ 1 ❙ ❚ ... ...
 namespace http://mathhub.info/MitM/smglom/arithmetics ❚ import base http://mathhub.info/MitM/Foundation ❚ import lfxwt http://gl.mathhub.info/MMT/LFX/WTypes ❚ theory NaturalNumbers : base:?Logic = include base:?NatLiterals ❙ ... ... @@ -85,6 +86,31 @@ theory NaturalArithmetics : base:?Logic = /T convert explicitely a natural number into an "between" ❙ //this function is needed in context wehere a natural number "n" is needed as both natural number and between ❙ // added by sw ❙ // doesn't work correctly and actually shouldn't be necessary❙ // natToBetween : {from : ℕ}{to : ℕ} {v : ℕ } ⊦ from ≤ v ∧ v ≤ to ⟶ between from to ❘= [v,h] v❙ ❚ theory InductiveNaturalNumbers : lfxwt:?Inductive = induct Nats ()❘ = Natt : type ❙ Zero : Natt ❙ Succ : Natt ⟶ Natt ❙ ❚ def Natid () ❘ = recc : Natt ⟶ Natt ❙ Zero = Zero ❙ Succ = [m : Natt] Succ (recc m)❙ ❚ ❚ theory NatConversions : lfxwt:?Inductive = // include ?InductiveNaturalNumbers❙ // include ?NaturalNumbers ❙ // natlitToNat : ℕ ⟶ Nat❙ bla = prop ❙ ❚
 ... ... @@ -3,18 +3,46 @@ namespace http://mathhub.info/MitM/smglom ❚ import base http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ import lfxwt http://gl.mathhub.info/MMT/LFX/WTypes ❚ import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚ import top http://gl.mathhub.info/MMT/LFX ❚ theory FinSequences : base:?Logic = include arith:?NaturalArithmetics ❙ // below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n⟩ ❙ /T finite sequences ❙ finiteSequence : ℕ ⟶ type ⟶ type ❘= [n , A] between 1 n ⟶ A ❘# finSeq 1 2 ❙ finiteSequence : ℕ ⟶ type ⟶ type ❘= [n , A] betweenOneAnd n ⟶ A ❘# finSeq 1 2 ❙ // disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] ∀ [h : ⊦ x < n] ∀ [h0 : ⊦ y < n] y ≐ x ∨ fs x h ≠ fs y h0❙ ❚ theory blaaa : lfxwt:?Inductive = induct Nats ()❘ = Nat : type ❘ # ℕ ❙ Zero : ℕ ❘ # O ❙ Succ : ℕ ⟶ ℕ ❘ # S 1 ❙ ❚ bla : ℕ ❘ = 1 ❙ ❚ theory FinSeqProps : base:?Logic = include arith:?RealArithmetics ❙ include ?FinSequences ❙ /T A disjoint ❙ prop_disjointFinSeq : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] y ≐ x ∨ fs x ≠ fs y ❘# disjoint 3❙ asceindingLoop ❙ // ascendingfn : {n : ℕ} finSeq n ℝ ⟶ bool ❘ = [n,sq] ascending ❘# ascending 2 ❙ ❚ theory FinSeqSum : base:?Logic = ... ... @@ -22,6 +50,7 @@ theory FinSeqSum : base:?Logic = include arith:?RealArithmetics ❙ include arith:?NaturalArithmetics ❙ // sw: old version of finSeqSumRec. I leave it here in case I need it in the future ❙ // this one does the actual recusive summation and is called by finSeqSum ❙ // finSeqSumRec : {n : ℕ} {m : ℕ } ⊦ `arith:?NaturalArithmetics?lessthan m n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 2 3 4❙ // finSeqSumRecB : {n : ℕ} {sq : finSeq n ℝ} {h : ⊦ `arith:?NaturalArithmetics?lessthan 0 n} ⊦ finSeqSumRec n 0 h sq ≐ 0 ❙ ... ... @@ -29,14 +58,15 @@ theory FinSeqSum : base:?Logic = ⊦ finSeqSumR ( `arith:?NaturalNumbers?succ m) h sq ≐ sq (`arith:?NaturalNumbers?succ m) h + finSeqSumR m (lt_pred_lt h) sq❙ finSeqSumRec : {n : ℕ} betweenOneAnd n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 2 3 4❙ finSeqSumRec : {n : ℕ} betweenOneAnd n ⟶ finSeq n ℝ ⟶ ℝ ❘# finSeqSumR 1 2 3❙ finSeqSumRecB : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSumRec n 1 sq ≐ sq 1 ❙ // finSeqSumRecS : {n : ℕ} {m : ℕ} {sq : finSeq n ℝ} {h : ⊦ `arith:?NaturalNumbers?succ m < n} ⊦ finSeqSumR ( `arith:?NaturalNumbers?succ m) h sq ≐ sq (`arith:?NaturalNumbers?succ m) h + finSeqSumR m (lt_pred_lt h) sq❙ finSeqSum : {n : ℕ} finSeq n ℝ ⟶ ℝ❙ finSeqSumZero : {sq} ⊦ finSeqSum 0 sq ≐ 0 ❙ finSeqSumFn : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSum n sq ≐ finSeqSumRec n n sq❙ finSeqSumRecS : {n : ℕ} {m : betweenOneAnd n} {sq : finSeq n ℝ} ⊦ finSeqSumR n ( `arith:?NaturalNumbers?succ m) sq ≐ sq (`arith:?NaturalNumbers?succ m) + finSeqSumR n m sq❙ finSeqSum : {n : ℕ} finSeq n ℝ ⟶ ℝ❙ // the function implementation currently doesn't type check (between n < Nat) ❙ // finSeqSumZero : {sq} ⊦ finSeqSum 0 sq ≐ 0 ❙ // finSeqSumFn : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSum n sq ≐ finSeqSumRec n n sq❙ ❚ \ No newline at end of file
 ... ... @@ -42,7 +42,7 @@ theory Measure : base:?Logic = measureSpace = {' universe : type , sigma_algebra : sigmaAlgebra universe , rmeasure : measure universe sigma_algebra measure : measure universe sigma_algebra '}❙ measurableSpace = {'universe : type , sigma_algebra : sigmaAlgebra universe '} ❙ ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment