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/CoupledUniqueness.lean",
3   "sha256": "40ce00b496300eff1cefd1204918e43661b9487273d90e13c6b8352c305f5e21",
4   "count": 16,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_scale_at_zero",
8       "line": 21
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_scale_ge",
12       "line": 27
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_mul_ge_left",
16       "line": 41
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_order_mul_ge_right",
20       "line": 49
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_row_order_ge",
24       "line": 58
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_difference_germ",
28       "line": 73
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_pair_germ_unique",
32       "line": 92
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_differentiable",
36       "line": 136
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_unique",
40       "line": 141
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_eq",
44       "line": 158
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_exists_unique",
48       "line": 163
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_germ_eq",
52       "line": 173
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_hasSum",
56       "line": 186
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_hasSum",
60       "line": 199
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.entire_solution_odd",
64       "line": 209
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_F1_contract",
68       "line": 220
69     }
70   ]
71 }

Back to source controls

Back to Special Functions