Commit 6fdfc850 authored by Sven Wille's avatar Sven Wille

more finsequences

parent 39f3a83b
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:3034.76.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:3754.88.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -27,6 +27,8 @@ dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?a
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_rightUnitalPlus
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_lt_pred_lt
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le
datatypeconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between
datatypeconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd
theory http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics
HasMeta http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
......@@ -350,3 +352,25 @@ DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_l
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lemma_le_pred_le?type http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leq?definition
Declares http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between
constant http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?definition http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?between?definition http://mathhub.info/MitM/Foundation?Logic?and?type
Declares http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd
constant http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?definition http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?betweenOneAnd?definition http://mathhub.info/MitM/Foundation?Logic?and?type
namespace http://mathhub.info/MitM/smglom/Probability ❚
import base http://mathhub.info/MitM/Foundation ❚
// import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚
theory ProbabilityMeasure : base:?Logic =
include measures?Measure ❙
theory probabilityMeasure_theory : base:?Logic > X : type , A : sigmaAlgebra X ❘ =
include measures?Measure/measure_theory (X,A) ❙
axiom_fullsetisone : ⊦ μ (elem (A.coll) (fullset X)) ≐ 1 ❙
probabilityMeasure = [X : type, A : sigmaAlgebra X] Mod `?ProbabilityMeasure/probabilityMeasure_theory X A ❙
probabilitySpace = {'
universe : type ,
sigma_algebra : sigmaAlgebra universe ,
measure : probabilityMeasure universe sigma_algebra
'} ❙
theory ProbabilitySpaceTheorems : base:?Logic =
include ?ProbabilityMeasure ❙
include calculus?LebesgueIntegral ❙
include measures?Measurable ❙
include measures?LebesgueMeasurable ❙
theory probabilitySpaceTheorems_theory : 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 ❙
// theorems ❙
// lemma_probabilityLe1 : ⊦ ∀[x : set Ω] probability x ≤ 1 ❙
lemma_omegaNotEmpty : ⊦ fullset Ω ≠ ∅ ❙
// lemma_probabilityGe1Eq1 : {x : set Ω} ⊦ 1 ≤ probability x ⟶ ⊦ probability x ≐ 1 ❙
namespace http://mathhub.info/MitM/smglom/probability ❚
import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/smglom/typedsets ❚
import calc http://mathhub.info/MitM/smglom/calculus ❚ // for seqeuences and intervals ❚
import mes http://mathhub.info/MitM/smglom/measures ❚
theory VitaliCoinToss : base:?Logic =
// a version of the vitali theorem from Hans-Otto Georgii's "Stochastik" ❙
include sets:?AllSets ❙
include calc:?Sequences ❙
include base:?DescriptionOperator ❙
include calc:?Intervals ❙
include mes:?SigmaAdditive ❙
vitaliSet : set (sequence ℕ) ❘= ⟪ (fullset (ℕ ⟶ ℕ)) | ([f] ∀[i] f i ≐ 0 ∨ f i ≐ 1) ⟫ ❙
vitaliPowerSet : collection (sequence ℕ) ❘= ℘ vitaliSet ❙
flipOneZero : ℕ ⟶ ℕ ❘= [n] (if (n ≐ 1) then 0 else (if (n ≐ 0) then (1 : ℕ) else n))❙
flipAt : ℕ ⟶ (sequence ℕ) ⟶ (sequence ℕ) ❘= [n , oldSeq] [i : ℕ] (if (i ≐ n) then (flipOneZero (oldSeq i)) else (oldSeq i)) ❙
vitaliPowerSetType : type ❘= setastype (vitaliPowerSet)❙
invariancy : (vitaliPowerSetType ⟶ ℝ) ⟶ bool ❘ = [P] ∀[A ] ∀[n : ℕ] A ⊑ vitaliSet ⇒
P (elem vitaliPowerSet A) ≐ P (elem vitaliPowerSet (im (flipAt n) A))❙
vitaliTheorem :
⊦ (¬ (∃[P : vitaliPowerSetType ⟶ ℝ]
(∀[x : vitaliPowerSetType] P x ≤ 1 ∧ 0 ≤ P x) ∧ P (vitaliSet) ≐ 1 ∧ prop_sigmaAdditive vitaliPowerSet P) ∧ invariancy P) ❙
......@@ -85,6 +85,6 @@ 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 ❙
natToBetween : {from : ℕ}{to : ℕ} {v : ℕ } ⊦ from ≤ v ∧ v ≤ to ⟶ between from to ❘= [v,h] v❙
// natToBetween : {from : ℕ}{to : ℕ} {v : ℕ } ⊦ from ≤ v ∧ v ≤ to ⟶ between from to ❘= [v,h] v❙
......@@ -37,6 +37,6 @@ theory FinSeqSum : base:?Logic =
finSeqSum : {n : ℕ} finSeq n ℝ ⟶ ℝ❙
finSeqSumZero : {sq} ⊦ finSeqSum 0 sq ≐ 0 ❙
finSeqSumFn : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSum n sq ≐ finSeqSumRec n n sq❙
finSeqSumFn : {n : ℕ} {sq : finSeq n ℝ} ⊦ finSeqSum n sq ≐ finSeqSumRec n n sq❙
\ 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!
Please register or to comment