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/CoupledFormal.lean",
3   "sha256": "18ca2a8c463d83c9402bab3f2c312fd84e1a63fdb21873d669f6d2d0cc4d6c87",
4   "count": 29,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.positive_pair_recovery",
8       "line": 33
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.defect_factor",
12       "line": 100
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.defect_eq_zero_iff",
16       "line": 106
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.positive_square_injective",
20       "line": 125
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.seven_jet_injective",
24       "line": 132
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_solution",
28       "line": 204
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_congr",
32       "line": 211
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_solution_unique",
36       "line": 219
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_solution_exists_unique",
40       "line": 231
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_zero",
44       "line": 236
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_one",
48       "line": 238
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_two",
52       "line": 241
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_three",
56       "line": 247
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_positive",
60       "line": 253
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_positive",
64       "line": 267
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_le_geometric",
68       "line": 282
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficients_le_geometric",
72       "line": 322
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_bound",
76       "line": 343
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_summable",
80       "line": 355
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_summable",
84       "line": 364
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_absolutely_convergent",
88       "line": 372
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_tail_bound",
92       "line": 387
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.sameJet_of_coefficients_eq",
96       "line": 408
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_jet_through_degree_seven",
100       "line": 419
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.parameters_of_formal_pair_eq",
104       "line": 425
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.workedScales_positive",
108       "line": 435
109     },
110     {
111       "name": "Komorebi.SpecialFunctions.Coupled.Scales.workedScales_defect",
112       "line": 438
113     },
114     {
115       "name": "Komorebi.SpecialFunctions.Coupled.Scales.workedScales_recoverable",
116       "line": 441
117     },
118     {
119       "name": "Komorebi.SpecialFunctions.Coupled.Scales.boundary_collision",
120       "line": 451
121     }
122   ]
123 }

Back to source controls

Back to Special Functions