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/CoupledEvaluation.lean",
3   "sha256": "59bf338f4b10672501ebf1a6dd0e2e02c74b86750adef2cc679fabc735dc1cd9",
4   "count": 36,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_real_hasSum",
8       "line": 14
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_norm_summable",
12       "line": 22
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_real_nonneg",
16       "line": 30
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_real_mono",
20       "line": 38
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_at_real",
24       "line": 46
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_le_pairMax",
28       "line": 56
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.realPairMax_nonneg",
32       "line": 62
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.realPairMax_recurrence",
36       "line": 67
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_coefficient_le_one",
40       "line": 91
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_small_disk_bound",
44       "line": 97
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.pair_small_disk_bound",
48       "line": 110
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.diskMajorant_of_small",
52       "line": 120
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.pair_le_diskMajorant",
56       "line": 123
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.exists_diskMajorant_fuel",
60       "line": 144
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_disk_majorant",
64       "line": 152
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.disk_majorant_exists",
68       "line": 163
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.outer_power_comparison",
72       "line": 170
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.positive_odd_outer_remainder",
76       "line": 181
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddPolynomial_at_real",
80       "line": 218
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_outer_remainder",
84       "line": 223
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_ladder_remainder",
88       "line": 234
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_polynomial_le_component",
92       "line": 243
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_evaluation_enclosure",
96       "line": 250
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_ladder_enclosure",
100       "line": 264
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rationalDiskMajorant_cast",
104       "line": 278
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_disk_majorant_sound",
108       "line": 292
109     },
110     {
111       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_outer_remainder",
112       "line": 301
113     },
114     {
115       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_real_enclosure",
116       "line": 313
117     },
118     {
119       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_coefficients_cast",
120       "line": 343
121     },
122     {
123       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_component_coefficient_cast",
124       "line": 368
125     },
126     {
127       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_polynomial_cast",
128       "line": 378
129     },
130     {
131       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_maxScale_cast",
132       "line": 385
133     },
134     {
135       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_fuel_exists",
136       "line": 389
137     },
138     {
139       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_endpoint_enclosure",
140       "line": 397
141     },
142     {
143       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_last_thirty_tail_rational",
144       "line": 409
145     },
146     {
147       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_last_thirty_error",
148       "line": 413
149     }
150   ]
151 }

Back to source controls

Back to Special Functions