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/CoupledGermInverse.lean",
3   "sha256": "92a0a2fa8fa33a9f6d602e73d8714c645d57b8bcee4d89205f87ad9dfb56bb2b",
4   "count": 13,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.denseOdd_odd",
8       "line": 23
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.denseOdd_even",
12       "line": 29
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_hasSum_dense",
16       "line": 34
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_hasFPowerSeriesAt",
20       "line": 52
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_coefficients_eq_of_germ_eq",
24       "line": 61
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_Taylor_coefficients",
28       "line": 74
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coupled_hasFPowerSeriesAt",
32       "line": 83
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_eq_of_analytic_germs",
36       "line": 94
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.sameJet_of_analytic_germs",
40       "line": 109
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_analytic_germs",
44       "line": 119
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_entire_pair_eq",
48       "line": 128
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.analytic_solution_Taylor_coefficients",
52       "line": 137
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_shared_solution_germ",
56       "line": 148
57     }
58   ]
59 }

Back to source controls

Back to Special Functions