Commit e0a24e7f authored by SuperDuckDuck's avatar SuperDuckDuck

added vitali theorem (coin toss version)

parent ec870dd0
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 ❚
import calc http://mathhub.info/MitM/smglom/calculus ❚ // for seqeuences and intervals ❚
import mes http://mathhub.info/MitM/smglom/measures ❚
// theory Vitali : base:?Logic =
include sets:?AllSets ❙
......@@ -10,14 +11,3 @@ import seqs http://mathhub.info/MitM/smglom/calculus ❚
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/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) ❙
\ 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