ProbabilityAtoms.lean`

GitHub source file

142 declarations, 0 contain sorry, 0 declared as axioms

Rank cutoffs, bounded row atoms, and their Lipschitz estimates.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

def OAI.ExactDerandomization.Analysis.clip line 19
def OAI.ExactDerandomization.Analysis.sat line 20
lemma OAI.ExactDerandomization.Analysis.clip_ic line 22
lemma OAI.ExactDerandomization.Analysis.clip_lip line 23
lemma OAI.ExactDerandomization.Analysis.clip_bounds line 24
lemma OAI.ExactDerandomization.Analysis.sandwich line 25
lemma OAI.ExactDerandomization.Analysis.Lip.raise line 28
lemma OAI.ExactDerandomization.Analysis.Lip.chain line 31
structure OAI.ExactDerandomization.Analysis.Frag line 41
Source documentation
Building block with bounded fourth-root Lipschitz norm and bounded sensitivity range. The constants here need not be the algorithmic clamp coefficients.
```
structure Frag (c : ℝ) (f : ℝ → ℝ) : Prop where
…
```
lemma OAI.ExactDerandomization.Analysis.Frag.raise line 48
lemma OAI.ExactDerandomization.Analysis.Frag.lipprod line 56
lemma OAI.ExactDerandomization.Analysis.Frag.mul line 66
lemma OAI.ExactDerandomization.Analysis.Frag.scale_clip line 88
lemma OAI.ExactDerandomization.Analysis.Frag.cnst line 107
lemma OAI.ExactDerandomization.Analysis.rootSlope line 112
Source documentation
convenient sufficient condition for bounded-away-from-zero leaves
```
lemma rootSlope {z x y : ℝ} (h:0<z) (hx:z≤x) (hy:z≤y) :
    |fourth y-fourth x| ≤ |y-x|/(fourth z)^3 := by
…
```
Mentions: OAI.ExactDerandomization.Analysis.fourth
lemma OAI.ExactDerandomization.Analysis.frag_positive line 135
lemma OAI.ExactDerandomization.Analysis.frag_switch line 151
abbrev OAI.ExactDerandomization.At.cut line 182
lemma OAI.ExactDerandomization.At.cut_low line 183
lemma OAI.ExactDerandomization.At.cut_high line 184
def OAI.ExactDerandomization.At.highcut line 186
def OAI.ExactDerandomization.At.sw line 187
def OAI.ExactDerandomization.At.bin line 188
lemma OAI.ExactDerandomization.At.high_mem line 189
lemma OAI.ExactDerandomization.At.sw_mem line 195
lemma OAI.ExactDerandomization.At.bin_mem line 199
lemma OAI.ExactDerandomization.At.sw_bot line 203
lemma OAI.ExactDerandomization.At.sw_top line 204
lemma OAI.ExactDerandomization.At.sw_succ line 207
lemma OAI.ExactDerandomization.At.rate_step line 213
lemma OAI.ExactDerandomization.At.rate0 line 215
lemma OAI.ExactDerandomization.At.rate_small line 216
lemma OAI.ExactDerandomization.At.telescope line 221
lemma OAI.ExactDerandomization.At.discarded line 229
def OAI.ExactDerandomization.At.cap line 240
lemma OAI.ExactDerandomization.At.cap_hi line 241
def OAI.ExactDerandomization.At.tone line 242
def OAI.ExactDerandomization.At.dirShare line 243
def OAI.ExactDerandomization.At.bfrag line 247
lemma OAI.ExactDerandomization.At.tone_mem line 250
lemma OAI.ExactDerandomization.At.bfrag_low line 252
lemma OAI.ExactDerandomization.At.bexact line 256
lemma OAI.ExactDerandomization.At.hiRatio line 278
lemma OAI.ExactDerandomization.At.dir_regular line 291
lemma OAI.ExactDerandomization.At.bin_reg line 337
def OAI.ExactDerandomization.At.Qc line 367
lemma OAI.ExactDerandomization.At.shoulder_reg line 368
lemma OAI.ExactDerandomization.At.Qc_low line 380
abbrev OAI.ExactDerandomization.At.small line 396
abbrev OAI.ExactDerandomization.At.zeta line 397
lemma OAI.ExactDerandomization.At.zp line 399
lemma OAI.ExactDerandomization.At.dp line 400
def OAI.ExactDerandomization.At.den line 403
Source documentation
use identically clipped denominators on any input
```
def den (x : ℝ) := clip (zeta/2) zeta x/zeta
```
Mentions: OAI.ExactDerandomization.At.zeta
def OAI.ExactDerandomization.At.divisor line 404
lemma OAI.ExactDerandomization.At.within_den line 405
lemma OAI.ExactDerandomization.At.inv_den line 411
lemma OAI.ExactDerandomization.At.den_reg line 417
structure OAI.ExactDerandomization.At.Trio line 446
Source documentation
Uniform finite list of pre-incoming figures; product of independent scalar pieces.
```
structure Trio where
…
```
def OAI.ExactDerandomization.At.Trio.eval line 451
structure OAI.ExactDerandomization.At.TS line 453
lemma OAI.ExactDerandomization.At.TS.nn line 461
lemma OAI.ExactDerandomization.At.TS.base line 463
lemma OAI.ExactDerandomization.At.TS.flat line 467
lemma OAI.ExactDerandomization.At.TS.rootub line 470
lemma OAI.ExactDerandomization.At.TS.comparison line 476
lemma OAI.ExactDerandomization.At.TS.extend line 502
def OAI.ExactDerandomization.At.mainT line 505
def OAI.ExactDerandomization.At.prep line 507
def OAI.ExactDerandomization.At.prepT line 508
def OAI.ExactDerandomization.At.suppT line 511
Source documentation
auxiliary and all-purpose witness.
```
def suppT (t : ℝ) (b : Bool) : Trio :=
…
```
Mentions: OAI.ExactDerandomization.At.Trio
lemma OAI.ExactDerandomization.At.main_ts line 515
lemma OAI.ExactDerandomization.At.supp_ts0 line 530
lemma OAI.ExactDerandomization.At.supp_ts line 543
abbrev OAI.ExactDerandomization.At.Pt line 565
structure OAI.ExactDerandomization.At.Blob line 566
def OAI.ExactDerandomization.At.Blob.rk line 572
def OAI.ExactDerandomization.At.Blob.val line 574
lemma OAI.ExactDerandomization.At.Blob.thin line 577
lemma OAI.ExactDerandomization.At.Blob.support_size line 589
structure OAI.ExactDerandomization.At.Blob.Guess line 601
Source documentation
Consistency with deterministic finite approximations for access.
```
structure Guess where
…
```
def OAI.ExactDerandomization.At.Blob.acc line 605
def OAI.ExactDerandomization.At.Blob.expose line 611
Source documentation
b=false exposes main, true exposes the first (precursor) witness (for purposes of rank).
```
def expose (t : ℝ) (g : Guess) (b : Bool) (S : Domain) :=
…
```
Mentions: OAI.ExactDerandomization.At.Blob.Guess
lemma OAI.ExactDerandomization.At.Blob.expose_subset line 615
lemma OAI.ExactDerandomization.At.Blob.has_room line 618
lemma OAI.ExactDerandomization.At.Blob.protects line 629
lemma OAI.ExactDerandomization.At.Blob.exposure_count line 637
lemma OAI.ExactDerandomization.At.Blob.exposed_main line 644
lemma OAI.ExactDerandomization.At.Blob.exposed_supp line 660
lemma OAI.ExactDerandomization.At.Blob.missing_baseline line 674
def OAI.ExactDerandomization.At.clim line 695
Source documentation
choose incoming cap after pilot column thresholds. Use ranking with same convention (zero-based; cap at c, c+1st score gate).
```
def clim (p : Const) := (1+32*(128 + 4*(p.J+1)))*128
```
lemma OAI.ExactDerandomization.At.clim_bound line 696
structure OAI.ExactDerandomization.At.Grid line 699
def OAI.ExactDerandomization.At.shutoff line 707
lemma OAI.ExactDerandomization.At.shutoff_mem line 708
lemma OAI.ExactDerandomization.At.shutoff_full line 711
lemma OAI.ExactDerandomization.At.shutoff_zero line 713
def OAI.ExactDerandomization.At.Grid.pre line 720
def OAI.ExactDerandomization.At.Grid.witness line 724
def OAI.ExactDerandomization.At.Grid.rankin line 725
def OAI.ExactDerandomization.At.Grid.incG line 726
def OAI.ExactDerandomization.At.Grid.result line 727
def OAI.ExactDerandomization.At.Grid.present line 730
def OAI.ExactDerandomization.At.Grid.inc line 732
def OAI.ExactDerandomization.At.Grid.paired line 734
def OAI.ExactDerandomization.At.Grid.Agree line 737
lemma OAI.ExactDerandomization.At.Grid.incG_bounds line 740
lemma OAI.ExactDerandomization.At.Grid.pres_range line 745
lemma OAI.ExactDerandomization.At.Grid.pres_card line 750
lemma OAI.ExactDerandomization.At.Grid.protect line 755
lemma OAI.ExactDerandomization.At.Grid.has_main line 762
lemma OAI.ExactDerandomization.At.Grid.has_witness line 772
lemma OAI.ExactDerandomization.At.Grid.paired_sub line 780
lemma OAI.ExactDerandomization.At.Grid.degree line 785
lemma OAI.ExactDerandomization.At.Grid.degree_in line 788
lemma OAI.ExactDerandomization.At.Grid.nonzero_present line 799
lemma OAI.ExactDerandomization.At.Grid.pre_support line 819
lemma OAI.ExactDerandomization.At.Grid.pre_count line 824
structure OAI.ExactDerandomization.At.Ask line 844
def OAI.ExactDerandomization.At.Ask.hand line 858
def OAI.ExactDerandomization.At.Ask.d line 860
def OAI.ExactDerandomization.At.Ask.raw line 861
def OAI.ExactDerandomization.At.Ask.botRow line 863
def OAI.ExactDerandomization.At.Ask.bath line 864
def OAI.ExactDerandomization.At.Ask.two line 868
Source documentation
two independent retentions at rates u and t
```
def two (x y : ℕ) (f : Channel n → Channel n → ℝ) :=
…
```
def OAI.ExactDerandomization.At.Ask.tooth line 871
def OAI.ExactDerandomization.At.Ask.rawplus line 874
def OAI.ExactDerandomization.At.Ask.atomTrue line 877
lemma OAI.ExactDerandomization.At.Ask.hth line 880
lemma OAI.ExactDerandomization.At.Ask.gate1 line 884
lemma OAI.ExactDerandomization.At.Ask.base_bath line 893
lemma OAI.ExactDerandomization.At.Ask.bath_mem line 901
lemma OAI.ExactDerandomization.At.Ask.tooth_mem line 911
lemma OAI.ExactDerandomization.At.Ask.two_mono line 914
lemma OAI.ExactDerandomization.At.Ask.two_rw line 919
lemma OAI.ExactDerandomization.At.Ask.valid_broad line 925
lemma OAI.ExactDerandomization.At.Ask.premask line 932
lemma OAI.ExactDerandomization.At.Ask.tooth0 line 944
structure OAI.ExactDerandomization.At.Ask.Valid line 952
lemma OAI.ExactDerandomization.At.Ask.row_fail line 963
def OAI.ExactDerandomization.At.Ask.lbad line 973
lemma OAI.ExactDerandomization.At.Ask.col_fail line 976
lemma OAI.ExactDerandomization.At.Ask.normalized_mean line 1029