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/CoupledScalarReduction.lean",
3   "sha256": "4ca29da51d06096d34b8e85d62018d2c8c03329f1378f7e57d69926f62119c00",
4   "count": 43,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.positive_pair_from_product_and_square_sum",
8       "line": 19
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_coefficients",
12       "line": 37
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_product",
16       "line": 45
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_square_sum",
20       "line": 52
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.equal_components_unordered_rows",
24       "line": 63
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scalar_pair_solution",
28       "line": 69
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unordered_rows_scalar_representation",
32       "line": 78
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.components_equal_iff_unordered_rows",
36       "line": 84
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.components_equal_iff_scale_pair_set",
40       "line": 92
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristicExponent_eq_of_balance",
44       "line": 98
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scalar_characteristic_balance_iff",
48       "line": 104
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scalar_characteristic_order",
52       "line": 125
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_order_invariant",
56       "line": 133
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.complex_sinh_hasDerivAt",
60       "line": 143
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.sinh_half_derivative_identity",
64       "line": 149
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scaled_sinh_half_equation",
68       "line": 163
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.halfScales_positive",
72       "line": 176
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.halfScales_strict",
76       "line": 178
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scaled_sinh_half_solution",
80       "line": 182
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.sqrt_two_complex_square",
84       "line": 189
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_half_sinh",
88       "line": 192
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.half_characteristic_order",
92       "line": 200
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.half_radial_order",
96       "line": 206
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequalScales_positive",
100       "line": 211
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequalScales_strict",
104       "line": 213
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_characteristic_order",
108       "line": 217
109     },
110     {
111       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_radial_order",
112       "line": 223
113     },
114     {
115       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_normalized_vector",
116       "line": 227
117     },
118     {
119       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_type_proportions",
120       "line": 235
121     },
122     {
123       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_components_different",
124       "line": 250
125     },
126     {
127       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_coefficients_through_seven",
128       "line": 256
129     },
130     {
131       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_row_sums",
132       "line": 264
133     },
134     {
135       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_lower_constants",
136       "line": 270
137     },
138     {
139       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_explicit_lower_growth",
140       "line": 277
141     },
142     {
143       "name": "Komorebi.SpecialFunctions.Coupled.Scales.surface_cross_scale_contract",
144       "line": 292
145     },
146     {
147       "name": "Komorebi.SpecialFunctions.Coupled.Scales.order_surface_realization",
148       "line": 314
149     },
150     {
151       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_oddSum",
152       "line": 336
153     },
154     {
155       "name": "Komorebi.SpecialFunctions.Coupled.Scales.component_coefficient_majorant",
156       "line": 340
157     },
158     {
159       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_truncation_eq_tail",
160       "line": 350
161     },
162     {
163       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_complex_truncation_bound",
164       "line": 359
165     },
166     {
167       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_four_term_remainder",
168       "line": 370
169     },
170     {
171       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_degree_seven_polynomials",
172       "line": 386
173     },
174     {
175       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unequal_degree_seven_error",
176       "line": 397
177     }
178   ]
179 }

Back to source controls

Back to Special Functions