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/CoupledOperator.lean",
3   "sha256": "743c863d39fccb19ea88e09e49671ffddaea40030ad867a8902c4169e9e1a047",
4   "count": 27,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_iff_scalar_functional",
8       "line": 51
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_differentiable",
12       "line": 70
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_zero",
16       "line": 73
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nodePolynomial_values",
20       "line": 76
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_scalar_fibers",
24       "line": 85
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_row_sum_zero",
28       "line": 100
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nonzero_row_first_ne_zero",
32       "line": 116
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_scale_products",
36       "line": 126
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_ordered_rows",
40       "line": 160
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ordered_rows_field_zero",
44       "line": 169
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ordered_rows_autonomous",
48       "line": 179
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.zero_row_autonomous",
52       "line": 185
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_iff_zero_or_ordered",
56       "line": 190
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_nonzero_classification",
60       "line": 202
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_projected_field_zero",
64       "line": 218
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.no_nonzero_autonomous_if_rows_differ",
68       "line": 224
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.autonomous_matrix_det_zero",
72       "line": 228
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.no_invertible_constant_decoupling",
76       "line": 235
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.local_projection_analytic",
80       "line": 251
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.local_field_analytic",
84       "line": 255
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.local_field_respects_component_germs",
88       "line": 264
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_iff_scalar_functional",
92       "line": 279
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.entire_field_differentiable",
96       "line": 289
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_implies_entire",
100       "line": 298
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_iff_entire",
104       "line": 311
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.germ_autonomous_nonzero_classification",
108       "line": 319
109     },
110     {
111       "name": "Komorebi.SpecialFunctions.Coupled.Scales.no_invertible_constant_germ_decoupling",
112       "line": 324
113     }
114   ]
115 }

Back to source controls

Back to Special Functions