Special Functions

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 {
2   "source": "lean/CoupledGuardedMajorant.lean",
3   "sha256": "349f0d3ae54d93aa5035cee180e26c8d8ba30169c478511136af20cc6d421b0c",
4   "count": 30,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ladder_terminal",
8       "line": 39
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ladder_terminal_small",
12       "line": 47
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ladder_adequate",
16       "line": 52
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ladder_fold_eq",
20       "line": 57
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_ok",
24       "line": 67
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_of_trace",
28       "line": 93
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_ok_iff",
32       "line": 104
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_not_bits",
36       "line": 108
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.build_ladder_exists_of_adequate",
40       "line": 122
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_not_steps",
44       "line": 145
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_ok_iff",
48       "line": 155
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_fold_bits_iff",
52       "line": 175
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_success",
56       "line": 195
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_small",
60       "line": 207
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_zero",
64       "line": 211
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_no_steps",
68       "line": 215
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_disk_bound",
72       "line": 219
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_endpoint_enclosure",
76       "line": 229
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_step_failure",
80       "line": 239
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.guarded_majorant_bit_failure",
84       "line": 244
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.size_fits_iff",
88       "line": 256
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_scales",
92       "line": 290
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_negative_radius",
96       "line": 294
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_zero_before_resources",
100       "line": 298
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_steps",
104       "line": 302
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_invalid_bits",
108       "line": 306
109     },
110     {
111       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_valid_inputs",
112       "line": 312
113     },
114     {
115       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_small_seed_unchecked",
116       "line": 321
117     },
118     {
119       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_success_core",
120       "line": 326
121     },
122     {
123       "name": "Komorebi.SpecialFunctions.Coupled.Scales.checked_endpoint_enclosure",
124       "line": 335
125     }
126   ]
127 }

Back to source controls

Back to Special Functions