Skip to content

Commit f67b03e

Browse files
marekpetrikmarekpetrik
committed
Added lint check and fixed lint messages
1 parent 67a9ec3 commit f67b03e

2 files changed

Lines changed: 46 additions & 42 deletions

File tree

β€ŽProbability/Probability/Basic.leanβ€Ž

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ theorem prob_compl_one_minus : β„™[Β¬α΅£B // P] = 1 - β„™[B // P] :=
4646

4747
------------------------------ Expectation ---------------------------
4848

49-
namespace Ex
49+
section Expectation
5050

5151
variable {n : β„•} {P : Findist n}
5252
variable {k : β„•} {X : FinRV n β„š} {B : FinRV n Bool} {L : FinRV n (Fin k)}
@@ -73,10 +73,9 @@ theorem law_total_exp : 𝔼[𝔼[X |α΅£ L // P] // P] = 𝔼[X // P] :=
7373
_ = βˆ‘ i : Fin k, 𝔼[X * (L =α΅’ i) // P] := by apply Fintype.sum_congr; intro i; apply exp_congr; rw[indi_eq_indr]
7474
_ = 𝔼[X // P] := by rw [←exp_decompose]
7575

76+
end Expectation
7677

77-
end Ex
78-
79-
namespace Pr
78+
section Probability
8079

8180
variable {k : β„•} {L : FinRV n (Fin k)}
8281

@@ -91,4 +90,7 @@ theorem law_of_total_probs : β„™[B // P] = βˆ‘ i, β„™[B * (L =α΅£ i) // P] :=
9190
by_cases h1 : L Ο‰ = i
9291
repeat by_cases h2 : B Ο‰; repeat simp [h1, h2, 𝕀, indicator ]
9392

94-
end Pr
93+
94+
end Probability
95+
96+
#lint

β€ŽProbability/Probability/Defs.leanβ€Ž

Lines changed: 39 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -11,32 +11,36 @@ section Findist
1111

1212
variable {n : β„•}
1313

14+
/-- Finite probability distribution -/
1415
structure Findist (n : β„•) : Type where
15-
p : Fin n β†’ β„š
16+
/-- Probaiblity measure -/
17+
p : Fin n β†’ β„š
1618
prob : 1 ⬝α΅₯ p = 1
1719
nneg : 0 ≀ p
1820

21+
1922
namespace Findist
2023

24+
/-- Finite probability distribution -/
2125
abbrev Delta : β„• β†’ Type := Findist
26+
27+
/-- Finite probability distribution -/
2228
abbrev Ξ” : β„• β†’ Type := Delta
2329

2430

31+
/-- Single probability distribution -/
2532
def singleton : Findist 1 :=
2633
{p := ![1],
2734
prob := by simp [Matrix.vecHead],
2835
nneg := by simp [Pi.zero_def, Pi.le_def] }
2936

3037

31-
@[simp]
32-
def length (_ : Findist n) := n
33-
3438
variable {n : β„•}
3539

36-
theorem nonempty (P : Findist n) : P.length > 0 :=
40+
theorem nonempty (P : Findist n) : n > 0 :=
3741
by cases n
3842
Β· have := P.prob; simp_all only [Matrix.dotProduct_of_isEmpty, zero_ne_one]
39-
Β· simp only [length, gt_iff_lt, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true]
43+
Β· simp only [gt_iff_lt, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true]
4044

4145

4246
end Findist
@@ -87,52 +91,50 @@ instance instBoolAdd: Add Bool where add a b := Bool.or a b
8791
instance instBoolZero : Zero Bool where zero := false
8892
instance instBoolOne : One Bool where one := true
8993

90-
@[simp] lemma bool_mul_tt : (true * true : Bool) = true := rfl
91-
@[simp] lemma bool_mul_tf : (true * false : Bool) = false := rfl
92-
@[simp] lemma bool_mul_ft : (false * true : Bool) = false := rfl
93-
@[simp] lemma bool_mul_ff : (false * false : Bool) = false := rfl
94-
9594
variable {A B : Bool}
9695

9796
@[simp] theorem one_eq_true : (1:Bool) = true := rfl
9897
@[simp] theorem zero_eq_false : (0:Bool) = false := rfl
9998
@[simp] theorem bool_sum_or : A + B = Bool.or A B := rfl
10099
@[simp] theorem bool_prod_and : A * B = Bool.and A B := rfl
101100

102-
@[simp]
103-
def not (B : FinRV n Bool) : FinRV n Bool :=
101+
102+
/-- Negates a random variable -/
103+
@[simp] def not (B : FinRV n Bool) : FinRV n Bool :=
104104
fun Ο‰ ↦ (B Ο‰).not
105105

106+
/-- Negates a random variable -/
106107
prefix:40 "Β¬α΅£" => FinRV.not
107108

108-
@[simp]
109-
def eq [DecidableEq ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
109+
/-- Boolean random variable representing an quality condition -/
110+
@[simp] def eq [DecidableEq ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
110111
(fun Ο‰ ↦ decide (Y Ο‰ = y) )
111112

113+
/-- Boolean random variable representing an quality condition -/
112114
infix:50 "=α΅£" => FinRV.eq
113115

114-
/-- indicator version of equality -/
115-
@[simp]
116-
def eqi [DecidableEq ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n β„š :=
116+
/-- 0/1 random variable representing an quality condition -/
117+
@[simp] def eqi [DecidableEq ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n β„š :=
117118
(fun Ο‰ ↦ if Y Ο‰ = y then 1 else 0)
118119

120+
/-- 0/1 random variable representing an quality condition -/
119121
infix:50 "=α΅’" => FinRV.eqi
120122

121-
@[simp]
122-
def leq [LE ρ] [DecidableLE ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
123+
/-- Boolean random variable represening Y ≀ y inequality -/
124+
@[simp] def leq [LE ρ] [DecidableLE ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
123125
(fun Ο‰ ↦ Y Ο‰ ≀ y)
124126

127+
/-- Boolean random variable represening Y ≀ y inequality -/
125128
infix:50 "≀ᡣ" => FinRV.leq
126129

127-
@[simp]
128-
def gt [LT ρ] [DecidableLT ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
130+
/-- Boolean random variable represening Y > y inequality -/
131+
@[simp] def gt [LT ρ] [DecidableLT ρ] (Y : FinRV n ρ) (y : ρ) : FinRV n Bool :=
129132
fun Ο‰ ↦ Y Ο‰ > y
130133

134+
/-- Boolean random variable represening Y > y inequality -/
131135
infix:50 ">α΅£" => FinRV.gt
132136

133-
example (m n : β„•) : (m < n) ∨ (m = n) ∨ (m > n) := Nat.lt_trichotomy m n
134-
135-
/-- Shows equivalence when extending the random variable to another element. -/
137+
/-- Equivalence when extending the random variable to another element. -/
136138
theorem le_of_le_eq (D : FinRV n β„•) (m : β„•) : ((D ≀ᡣ m) + (D =α΅£ m.succ)) = (D ≀ᡣ m.succ) := by
137139
funext x --extensionality principle for functions
138140
unfold FinRV.leq FinRV.eq instHAdd Add.add Pi.instAdd
@@ -149,6 +151,7 @@ end FinRV
149151
/-- Boolean indicator function -/
150152
def indicator [OfNat ρ 0] [OfNat ρ 1] (cond : Bool) : ρ := cond.rec 0 1
151153

154+
/-- Boolean indicator function -/
152155
abbrev 𝕀 [OfNat ρ 0] [OfNat ρ 1] : Bool β†’ ρ := indicator
153156

154157

@@ -213,16 +216,16 @@ variable {n : β„•} (P : Findist n) (B C : FinRV n Bool)
213216
/-- Probability of B -/
214217
def probability : β„š := P.p ⬝α΅₯ (𝕀 ∘ B)
215218

219+
/-- Probability of B -/
216220
notation "β„™[" B "//" P "]" => probability P B
217221

218222
-- helps to refold is when needed
219223
lemma probability_def : P.p ⬝α΅₯ (𝕀 ∘ B) = β„™[B // P] := rfl
220224

221-
/-- Conditional probability of B -/
225+
/-- Conditional probability of B on C -/
222226
def probability_cnd : β„š := β„™[B * C // P] / β„™[ C // P ]
223227

224-
225-
---- conditional probability
228+
/-- Conditional probability of B on C -/
226229
notation "β„™[" B "|" C "//" P "]" => probability_cnd P B C
227230

228231

@@ -275,34 +278,31 @@ Main results
275278

276279
variable {n : β„•} (P : Findist n) (X Y Z: FinRV n β„š) (B : FinRV n Bool)
277280

281+
/-- Standard expectation operator -/
278282
def expect : β„š := P.p ⬝α΅₯ X
279283

284+
/-- Standard expectation operator -/
280285
notation "𝔼[" X "//" P "]" => expect P X
281286

282-
-- expectation for a joint probability space and random variable
283-
notation "𝔼[" PX "]" => expect PX.1 PX.2
284-
285287
--theorem exp_eq_correct : 𝔼[X // P] = βˆ‘ v ∈ ((List.finRange P.length).map X).toFinset, v * β„™[ X =α΅£ v // P]
286288

287289
@[simp]
288290
theorem prob_eq_exp_ind : β„™[B // P] = 𝔼[𝕀 ∘ B // P] := by simp only [expect, probability]
289291

290-
/-- Conditional expectation -/
292+
/-- Conditional expectation operator -/
291293
def expect_cnd : β„š := 𝔼[ X * (𝕀 ∘ B) // P] / β„™[ B // P]
292294

295+
/-- Conditional expectation operator -/
293296
notation "𝔼[" X "|" B "//" P "]" => expect_cnd P X B
294297

295-
-- expectation for a joint probability space and random variable
296-
notation "𝔼[" PX "|" B "]" => expect_cnd PX.1 PX.2 B
297-
298298
variable {k : β„•} (L : FinRV n (Fin k))
299299

300-
-- creates a random variable
300+
/-- Expectation conditioned on a random variable. It creates a random variable -/
301301
def expect_cnd_rv : Fin n β†’ β„š := fun i ↦ 𝔼[ X | L =α΅£ (L i) // P ]
302302

303+
/-- Expectation conditioned on a random variable. It creates a random variable -/
303304
notation "𝔼[" X "|α΅£" L "//" P "]" => expect_cnd_rv P X L
304305

305-
306306
--- some basic properties
307307

308308
section Expectation_properties
@@ -377,3 +377,5 @@ theorem exp_cond_const : βˆ€ i, β„™[L =α΅£ i // P] β‰  0 β†’ 𝔼[g ∘ L | L
377377
simp only [h, ne_eq, isUnit_iff_ne_zero, not_false_eq_true, IsUnit.mul_div_cancel_right]
378378

379379
end Expectation_properties
380+
381+
#lint

0 commit comments

Comments
Β (0)