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/CoupledGrowthTypes.lean",
3   "sha256": "1363c216cfd64706fce14bc8fece963f3313ecc3b4e393a7486c89b09b313c7a",
4   "count": 22,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.realComponent_positive",
8       "line": 29
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_bounds",
12       "line": 37
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_eventually",
16       "line": 47
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_bounded",
20       "line": 54
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_type_sandwich",
24       "line": 62
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_bounds",
28       "line": 73
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_types_positive",
32       "line": 80
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.loglog_ratio_sandwich",
36       "line": 87
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.tendsto_loglog_of_ratio_bounds",
40       "line": 108
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_radial_exponent_limit",
44       "line": 124
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_radial_order",
48       "line": 131
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_spherical_maximum",
52       "line": 138
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_real_norm",
56       "line": 148
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.norm_growth_ratio_eventually_eq",
60       "line": 156
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.norm_type_identification",
64       "line": 164
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_norm_radial_limit",
68       "line": 173
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.maximumModulus_eq",
72       "line": 185
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.maximum_growth_ratio_eventually_eq",
76       "line": 191
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.maximum_type_identification",
80       "line": 199
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_bounds",
84       "line": 208
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_radial_limit",
88       "line": 223
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_order",
92       "line": 232
93     }
94   ]
95 }

Back to source controls

Back to Special Functions