FiniteLaws.lean`

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Finite Laws

abbrev OAI.HadwigerCounterexample.Wgt line 21
def OAI.HadwigerCounterexample.ind line 26
Source documentation
Real indicator.
```
def ind (p : Prop) : ℝ := @ite ℝ p (Classical.propDecidable _) 1 0
```
theorem OAI.HadwigerCounterexample.ind_eq line 28
theorem OAI.HadwigerCounterexample.ind_one line 32
theorem OAI.HadwigerCounterexample.ind_zero line 33
theorem OAI.HadwigerCounterexample.ind_true line 34
theorem OAI.HadwigerCounterexample.ind_false line 35
theorem OAI.HadwigerCounterexample.ind_nonneg line 37
theorem OAI.HadwigerCounterexample.ind_le_one line 42
theorem OAI.HadwigerCounterexample.ind_mono line 48
theorem OAI.HadwigerCounterexample.ind_not line 54
theorem OAI.HadwigerCounterexample.ind_and line 57
theorem OAI.HadwigerCounterexample.ind_or_le line 60
def OAI.HadwigerCounterexample.tot line 68
Source documentation
Total weight.
```
def tot [Fintype α] (w : Wgt α) : ℝ := ∑ x, w x
```
Mentions: OAI.HadwigerCounterexample.Wgt
def OAI.HadwigerCounterexample.avg line 70
Source documentation
Weighted average (not normalized if the weights are not a probability law).
```
def avg [Fintype α] (w f : Wgt α) : ℝ := ∑ x, w x * f x
```
Mentions: OAI.HadwigerCounterexample.Wgt
def OAI.HadwigerCounterexample.pr line 72
Source documentation
Weight of an event.
```
def pr [Fintype α] (w : Wgt α) (p : α → Prop) := avg w (fun x => ind (p x))
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.avg, OAI.HadwigerCounterexample.ind
structure OAI.HadwigerCounterexample.SubLaw line 74
structure OAI.HadwigerCounterexample.IsLaw line 77
theorem OAI.HadwigerCounterexample.IsLaw.sub line 81
def OAI.HadwigerCounterexample.carried line 87
Source documentation
All positive mass is supported on p. We use the equivalent contrapositive with zero mass (and supply nonnegativity wherever we speak of a law).
```
def carried (w : Wgt α) (p : α → Prop) := ∀ x : α, ¬ p x → w x = 0
…
```
Mentions: OAI.HadwigerCounterexample.Wgt
theorem OAI.HadwigerCounterexample.tot_nonneg line 92
theorem OAI.HadwigerCounterexample.tot_mono line 94
theorem OAI.HadwigerCounterexample.weight_le_tot line 97
theorem OAI.HadwigerCounterexample.SubLaw.weight_le_one line 100
theorem OAI.HadwigerCounterexample.IsLaw.weight_le_one line 103
theorem OAI.HadwigerCounterexample.avg_comm line 105
theorem OAI.HadwigerCounterexample.avg_mono line 107
theorem OAI.HadwigerCounterexample.avg_mono_left line 110
theorem OAI.HadwigerCounterexample.avg_nonneg line 114
theorem OAI.HadwigerCounterexample.avg_zero line 117
theorem OAI.HadwigerCounterexample.avg_const line 119
theorem OAI.HadwigerCounterexample.IsLaw.avg_const line 122
theorem OAI.HadwigerCounterexample.SubLaw.avg_le line 125
theorem OAI.HadwigerCounterexample.IsLaw.avg_le line 131
theorem OAI.HadwigerCounterexample.IsLaw.le_avg line 134
theorem OAI.HadwigerCounterexample.abs_avg_le line 137
theorem OAI.HadwigerCounterexample.avg_add line 142
theorem OAI.HadwigerCounterexample.avg_sub line 145
theorem OAI.HadwigerCounterexample.avg_mul line 148
theorem OAI.HadwigerCounterexample.avg_mul' line 151
theorem OAI.HadwigerCounterexample.avg_div line 154
theorem OAI.HadwigerCounterexample.avg_congr line 158
theorem OAI.HadwigerCounterexample.avg_sum line 165
theorem OAI.HadwigerCounterexample.avg_avg line 170
theorem OAI.HadwigerCounterexample.pr_nonneg line 176
theorem OAI.HadwigerCounterexample.pr_le_tot line 179
theorem OAI.HadwigerCounterexample.pr_mono line 184
theorem OAI.HadwigerCounterexample.pr_mono_left line 187
theorem OAI.HadwigerCounterexample.pr_not line 190
theorem OAI.HadwigerCounterexample.pr_point line 193
theorem OAI.HadwigerCounterexample.pr_point' line 196
theorem OAI.HadwigerCounterexample.pr_true line 199
theorem OAI.HadwigerCounterexample.pr_false line 200
theorem OAI.HadwigerCounterexample.pr_or_le line 202
theorem OAI.HadwigerCounterexample.pr_union_le line 206
theorem OAI.HadwigerCounterexample.pr_exists_le line 222
theorem OAI.HadwigerCounterexample.weight_le_pr line 226
theorem OAI.HadwigerCounterexample.exists_of_pr_pos line 230
theorem OAI.HadwigerCounterexample.carried_iff_pr line 241
theorem OAI.HadwigerCounterexample.le_avg_markov line 253
def OAI.HadwigerCounterexample.subW line 265
Source documentation
Restrict weights; not renormalized.
```
def subW (w : Wgt α) (p : α → Prop) := fun x => w x * ind (p x)
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.ind
def OAI.HadwigerCounterexample.normW line 268
Source documentation
Divide a finite weight function by its total, giving zero if total is zero.
```
def normW [Fintype α] (w : Wgt α) := fun x => w x / tot w
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.tot
def OAI.HadwigerCounterexample.unif line 270
def OAI.HadwigerCounterexample.unifOn line 271
theorem OAI.HadwigerCounterexample.subW_nonneg line 277
theorem OAI.HadwigerCounterexample.subW_tot line 280
theorem OAI.HadwigerCounterexample.subW_le line 283
theorem OAI.HadwigerCounterexample.subW_carried line 287
theorem OAI.HadwigerCounterexample.subLaw_sub line 290
theorem OAI.HadwigerCounterexample.pr_sub line 293
theorem OAI.HadwigerCounterexample.normW_nonneg line 297
theorem OAI.HadwigerCounterexample.avg_norm line 300
theorem OAI.HadwigerCounterexample.tot_norm line 304
theorem OAI.HadwigerCounterexample.normW_law line 307
theorem OAI.HadwigerCounterexample.normW_subLaw line 310
theorem OAI.HadwigerCounterexample.normW_carried line 315
theorem OAI.HadwigerCounterexample.unif_apply line 318
theorem OAI.HadwigerCounterexample.unif_subLaw line 321
theorem OAI.HadwigerCounterexample.unif_law line 324
theorem OAI.HadwigerCounterexample.unifOn_law line 328
def OAI.HadwigerCounterexample.pairW line 338
def OAI.HadwigerCounterexample.mixW line 339
def OAI.HadwigerCounterexample.mapW line 340
theorem OAI.HadwigerCounterexample.pairW_avg line 345
theorem OAI.HadwigerCounterexample.pairW_separate line 349
theorem OAI.HadwigerCounterexample.pairW_pr line 353
theorem OAI.HadwigerCounterexample.pairW_tot line 358
theorem OAI.HadwigerCounterexample.pairW_law line 361
theorem OAI.HadwigerCounterexample.mixW_avg line 364
theorem OAI.HadwigerCounterexample.mixW_tot line 370
theorem OAI.HadwigerCounterexample.mixW_law line 374
theorem OAI.HadwigerCounterexample.mapW_avg line 381
theorem OAI.HadwigerCounterexample.mapW_law line 388
theorem OAI.HadwigerCounterexample.mapW_pr line 392