danabra.mov
+6
-5
README.md
+6
-5
README.md
···
109
109
I am using this repository to host some other minor Lean content unrelated to the text book:
110
110
111
111
- A formalization of physical units
112
-
- Support for systems of units ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/UnitsSystem.lean)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/UnitsSystem.lean))
113
-
- Examples of use ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/UnitsSystemExamples.lean)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/UnitsSystemExamples.lean))
114
-
- The SI system of units ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/SI.lean)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SI.lean))
115
-
- Examples of use ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/SIExamples.lean)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SIExamples.lean))
112
+
- Support for systems of units ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/UnitsSystem.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/UnitsSystem.lean))
113
+
- Examples of use ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/UnitsSystemExamples.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/UnitsSystemExamples.lean))
114
+
- The SI system of units ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/SI.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SI.lean))
115
+
- Examples of use ([Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/SIExamples.html)) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/SIExamples.lean))
116
116
- A formalization of finite choice avoiding Lean's axiom of choice
117
-
- [Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/FiniteChoice.lean) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/FiniteChoice.lean))
117
+
- [Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/FiniteChoice.html) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/FiniteChoice.lean))
118
+
- Some finite probability theory [Documentation](https://teorth.github.io/analysis/docs/Analysis/Misc/Probability.html) ([Lean source](https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/Probability.lean))
118
119
119
120
## Other resources
120
121
+1
analysis/Analysis.lean
+1
analysis/Analysis.lean
+57
-10
analysis/Analysis/Misc/Probability.lean
+57
-10
analysis/Analysis/Misc/Probability.lean
···
1
1
import Mathlib.Tactic
2
-
import Mathlib.Probability.Notation
3
2
4
-
open MeasureTheory ProbabilityTheory
3
+
/-! Some finite probability theory -/
5
4
6
-
structure MeasureTheory.Extension (X Y: Type*) [MeasureSpace X] [MeasureSpace Y] where
7
-
π : X → Y
8
-
extension : MeasurePreserving π
5
+
namespace ProbabilityTheory
9
6
10
-
/-- An embedding, a.k.a. a bundled injective function. -/
11
-
infixr:25 " ↠ " => MeasureTheory.Extension
7
+
class FinitelyAdditive (A:Type*) [BooleanAlgebra A] where
8
+
prob : A → ℝ
9
+
prob_top : prob ⊤ = 1
10
+
prob_nonneg (E:A) : 0 ≤ prob E
11
+
prob_disj_sup {E F:A} (hEF: Disjoint E F) : prob (E ⊔ F) = prob E + prob F
12
12
13
-
instance MeasureTheory.Extension.instFunLike {X Y:Type*} [MeasureSpace X] [MeasureSpace Y] : FunLike (X ↠ Y) X Y where
14
-
coe := π
13
+
namespace FinitelyAdditive
14
+
15
+
instance instFunLike (A:Type*) [BooleanAlgebra A] : FunLike (FinitelyAdditive A) A ℝ where
16
+
coe ℙ := ℙ.prob
15
17
coe_injective' f g h := by { cases f; cases g; congr }
16
18
17
-
theorem MeasureTheory.Extension.measure_preimage {X Y: Type*} [MeasureSpace X] [MeasureSpace Y] (f: X ↠ Y) {E:Set Y} (hE: MeasurableSet E) :ℙ (⇑f ⁻¹' E) = ℙ E := MeasureTheory.MeasurePreserving.measure_preimage f.extension (MeasurableSet.nullMeasurableSet hE)
19
+
variable {A:Type*} [BooleanAlgebra A] (ℙ: FinitelyAdditive A)
20
+
21
+
@[simp]
22
+
theorem top : ℙ ⊤ = 1 := ℙ.prob_top
23
+
24
+
theorem nonneg (E:A) : 0 ≤ ℙ E := ℙ.prob_nonneg E
25
+
26
+
theorem disj_sup {E F:A} (hEF: Disjoint E F) : ℙ (E ⊔ F) = ℙ E + ℙ F := ℙ.prob_disj_sup hEF
27
+
28
+
@[simp]
29
+
theorem bot : ℙ ⊥ = 0 := by
30
+
have : Disjoint (⊥:A) ⊥ := fun ⦃x⦄ a _ ↦ a
31
+
replace := ℙ.disj_sup this
32
+
simpa using this
33
+
34
+
@[simp]
35
+
theorem compl (E:A) : ℙ Eᶜ = 1 - ℙ E := by
36
+
have : Disjoint Eᶜ E := disjoint_compl_left
37
+
replace := ℙ.disj_sup this
38
+
simp at this
39
+
linarith
40
+
41
+
theorem le_one (E:A) : ℙ E ≤ 1 := by
42
+
linarith [ℙ.compl E, ℙ.nonneg Eᶜ]
43
+
44
+
theorem ge_eq_add_diff {E F:A} (hEF: E ≤ F) : ℙ F = ℙ (F \ E) + ℙ E := by
45
+
have : Disjoint (F \ E) E := disjoint_sdiff_self_left
46
+
replace := ℙ.disj_sup this
47
+
rwa [sdiff_sup_cancel hEF] at this
48
+
49
+
theorem mono {E F:A} (hEF: E ≤ F) : ℙ E ≤ ℙ F := by
50
+
linarith [ℙ.nonneg (F \ E), ℙ.ge_eq_add_diff hEF]
51
+
52
+
theorem sup_add_inf (E F:A) : ℙ (E ⊔ F) + ℙ (E ⊓ F) = ℙ E + ℙ F := by
53
+
have h₁ : E ⊓ F ≤ E := inf_le_left; replace h₁ := ℙ.ge_eq_add_diff h₁
54
+
have h₂ : F ≤ E ⊔ F := le_sup_right; replace h₂ := ℙ.ge_eq_add_diff h₂
55
+
simp at h₁ h₂
56
+
linarith
57
+
58
+
theorem sup_le_add (E F:A) : ℙ (E ⊔ F) ≤ ℙ E + ℙ F := by
59
+
linarith [ℙ.sup_add_inf E F, ℙ.nonneg (E ⊓ F)]
60
+
61
+
62
+
63
+
end FinitelyAdditive
64
+
end ProbabilityTheory