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/CoupledNormalization.lean",
3   "sha256": "907fd0fa37a59dff472088a2afa6cc4f9bb22663ce9d153378560cfdeaa549f8",
4   "count": 30,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_ne_zero",
8       "line": 25
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_zero",
12       "line": 29
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddFactorial_succ",
16       "line": 32
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.binomial_factorial_product",
20       "line": 39
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.binomial_factorial_quotient",
24       "line": 48
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_zero",
28       "line": 80
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_succ",
32       "line": 83
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_solution",
36       "line": 91
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_solution_unique",
40       "line": 95
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivativeRow_factorialScale",
44       "line": 113
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.factorial_scaled_coefficients_solution",
48       "line": 128
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_factorial",
52       "line": 147
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivativeNext_congr",
56       "line": 153
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_eq",
60       "line": 169
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_length",
64       "line": 185
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_array_entry",
68       "line": 189
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_component_factorial",
72       "line": 197
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_component_normalized",
76       "line": 202
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_normalized_cast",
80       "line": 207
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_eq",
84       "line": 215
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_length",
88       "line": 224
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_array_entry",
92       "line": 228
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_polynomial_eq",
96       "line": 236
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.array_polynomial_eq",
100       "line": 244
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.array_polynomial_cast",
104       "line": 256
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_polynomial_cast",
108       "line": 260
109     },
110     {
111       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_endpoint_enclosure",
112       "line": 264
113     },
114     {
115       "name": "Komorebi.SpecialFunctions.Coupled.Scales.array_endpoint_enclosure",
116       "line": 275
117     },
118     {
119       "name": "Komorebi.SpecialFunctions.Coupled.Scales.rational_derivatives_one",
120       "line": 286
121     },
122     {
123       "name": "Komorebi.SpecialFunctions.Coupled.Scales.derivative_normalization_first",
124       "line": 291
125     }
126   ]
127 }

Back to source controls

Back to Special Functions