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/CoupledUpperGrowth.lean",
3   "sha256": "0b899b5d8639a9fe6a957af7ceffc7a3e173557c0bc7f347c92dc92fec344f1d",
4   "count": 34,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.full_radius_upper_from_deriv",
8       "line": 14
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_full_upper",
12       "line": 37
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_at_one_le_two",
16       "line": 54
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperRadius_ge_one",
20       "line": 75
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperRadius_child",
24       "line": 81
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperSeed_ge_one",
28       "line": 91
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_upper_ladder",
32       "line": 102
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperLogSeed_recurrence",
36       "line": 137
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperSeed_log_le",
40       "line": 143
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scaleDelay_positive",
44       "line": 179
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scaleDelay_bounds",
48       "line": 183
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperCorrection_positive",
52       "line": 193
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperCorrection_rows",
56       "line": 203
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.exp_one_lt_three",
60       "line": 214
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.exists_upper_seed_index",
64       "line": 226
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upper_seed_exp_radius",
68       "line": 233
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_upper_log_seed",
72       "line": 248
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.log_upper_from_full",
76       "line": 268
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_full_upper",
80       "line": 281
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperSeedBudget_positive",
84       "line": 299
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperPowerConstant_positive",
88       "line": 311
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upper_power_seed",
92       "line": 318
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.exp_sub_scaleDelay",
96       "line": 354
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_delayed_upper",
100       "line": 361
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.exp_weight_shift",
104       "line": 382
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_log_delay_induction",
108       "line": 389
109     },
110     {
111       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upper_power_step",
112       "line": 404
113     },
114     {
115       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_upper_log_power",
116       "line": 435
117     },
118     {
119       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_log_power",
120       "line": 446
121     },
122     {
123       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upperSeedIndex_spec",
124       "line": 478
125     },
126     {
127       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonicalUpperCoefficient_positive",
128       "line": 489
129     },
130     {
131       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_growth_ratio",
132       "line": 496
133     },
134     {
135       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_two_sided_growth_ratio",
136       "line": 524
137     },
138     {
139       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_norm_power",
140       "line": 540
141     }
142   ]
143 }

Back to source controls

Back to Special Functions