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/CoupledEntire.lean",
3   "sha256": "48359369ee25322fb301a060d239c2f688f46ac59098394a22fd7a3f6272cb64",
4   "count": 19,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddConvolution_eq",
8       "line": 24
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.next_term_mul_denominator",
12       "line": 43
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.next_term_norm_le",
16       "line": 55
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_bootstrap",
20       "line": 73
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_bootstrap",
24       "line": 95
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.maxScale_bounds",
28       "line": 111
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.maxScale_lt_one",
32       "line": 118
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_on_ladder",
36       "line": 124
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_entire",
40       "line": 148
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_term_norm_le_radius",
44       "line": 160
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn_of_radius",
48       "line": 168
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv_of_radius",
52       "line": 178
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_entire_of_norm_summable",
56       "line": 191
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire",
60       "line": 199
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv_entire",
64       "line": 205
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.next_derivative_term_eq",
68       "line": 212
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.oddSum_entire_equation",
72       "line": 223
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_equations",
76       "line": 246
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_solution",
80       "line": 265
81     }
82   ]
83 }

Back to source controls

Back to Special Functions