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/CoupledPositiveReal.lean",
3   "sha256": "a1e1b4f42efbffd0dcb0acf1a8b9ab23fe9fd775397219ad2c7961789414a8d7",
4   "count": 22,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_series_hasSum",
8       "line": 24
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_identification",
12       "line": 35
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_zero",
16       "line": 46
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_nonneg",
20       "line": 49
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_lower_linear",
24       "line": 59
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_hasDerivAt",
28       "line": 69
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_differentiable",
32       "line": 86
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_deriv_ge_one",
36       "line": 92
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_strictMono",
40       "line": 105
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_positive",
44       "line": 119
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_le_real_sum",
48       "line": 125
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.complex_norm_le_real_axis",
52       "line": 134
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_norm",
56       "line": 144
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.sphere_norm_isGreatest",
60       "line": 152
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.maximum_modulus_real_axis",
64       "line": 162
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.unit_shift_lower_from_deriv",
68       "line": 171
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_unit_lower",
72       "line": 197
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_unit_lower",
76       "line": 212
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.minScale_bounds",
80       "line": 237
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.minScale_positive",
84       "line": 244
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.lowerThreshold_gt_one",
88       "line": 247
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.lower_child_radii",
92       "line": 252
93     }
94   ]
95 }

Back to source controls

Back to Special Functions