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/CoupledAnalytic.lean",
3   "sha256": "4317cc45436eb5434b0ddd1418bd4096b3865cf4e9a92e32f2e5b23eeb1a247f",
4   "count": 21,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_zero",
8       "line": 26
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_neg",
12       "line": 29
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_uniform_bound",
16       "line": 33
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn_ball",
20       "line": 47
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.exists_local_radius",
24       "line": 61
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableAt",
28       "line": 74
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn",
32       "line": 81
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddTerm_hasDerivAt",
36       "line": 87
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv",
40       "line": 94
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasDerivAt",
44       "line": 108
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_bounds_left",
48       "line": 120
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_bounds_right",
52       "line": 125
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_differentiableOn",
56       "line": 130
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.mul_mem_localDisk",
60       "line": 136
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_mul_eq",
64       "line": 144
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_mul_denominator",
68       "line": 176
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_deriv_eq_of_recurrence",
72       "line": 183
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_local_equations",
76       "line": 208
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_local_solution",
80       "line": 231
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_initial_derivatives",
84       "line": 244
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_odd",
88       "line": 250
89     }
90   ]
91 }

Back to source controls

Back to Special Functions