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/CoupledCharacteristic.lean",
3   "sha256": "bba339b502ee9582dda88e226d3544e367cfce8a6153e14345d6c8e86a62eb84",
4   "count": 23,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_zero",
8       "line": 27
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rpow_contraction_bounds",
12       "line": 30
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_continuous",
16       "line": 35
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_strictMono",
20       "line": 41
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_tendsto",
24       "line": 63
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_exponent_exists_unique",
28       "line": 77
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicExponent_spec",
32       "line": 103
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicVector_positive",
36       "line": 127
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicLeftVector_positive",
40       "line": 134
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_right_eigenvector",
44       "line": 141
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_left_eigenvector",
48       "line": 150
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicNormalizer_positive",
52       "line": 159
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_positive",
56       "line": 163
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_max",
60       "line": 169
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.normalized_characteristic_eigenvector",
64       "line": 177
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_second_eigenvalue_bound",
68       "line": 183
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum",
72       "line": 191
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectralRadius",
76       "line": 207
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_mem_spectrum_iff",
80       "line": 227
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum_real",
84       "line": 234
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum_norm_attained",
88       "line": 251
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectralRadius_iff",
92       "line": 267
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectral_exponent_exists_unique",
96       "line": 303
97     }
98   ]
99 }

Back to source controls

Back to Special Functions