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/CoupledTypeProportions.lean",
3   "sha256": "c6b3d8dfb786730a7b0ed456992dd87af160016841bfd7195596017b42a16194",
4   "count": 26,
5   "declarations": [
6     {
7       "name": "Komorebi.SpecialFunctions.Coupled.Scales.affine_scale_tendsto",
8       "line": 18
9     },
10     {
11       "name": "Komorebi.SpecialFunctions.Coupled.Scales.affine_power_ratio_tendsto",
12       "line": 27
13     },
14     {
15       "name": "Komorebi.SpecialFunctions.Coupled.Scales.lower_comparison_of_tendsto",
16       "line": 41
17     },
18     {
19       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upper_comparison_of_tendsto",
20       "line": 48
21     },
22     {
23       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_envelopes",
24       "line": 55
25     },
26     {
27       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scaled_log_factorization",
28       "line": 69
29     },
30     {
31       "name": "Komorebi.SpecialFunctions.Coupled.Scales.scaled_type_envelopes",
32       "line": 81
33     },
34     {
35       "name": "Komorebi.SpecialFunctions.Coupled.Scales.log_power_correction_tendsto",
36       "line": 116
37     },
38     {
39       "name": "Komorebi.SpecialFunctions.Coupled.Scales.lower_type_row",
40       "line": 122
41     },
42     {
43       "name": "Komorebi.SpecialFunctions.Coupled.Scales.upper_type_row",
44       "line": 157
45     },
46     {
47       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_type_superinvariant",
48       "line": 194
49     },
50     {
51       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_type_subinvariant",
52       "line": 219
53     },
54     {
55       "name": "Komorebi.SpecialFunctions.Coupled.Scales.positive_dot_rigidity",
56       "line": 248
57     },
58     {
59       "name": "Komorebi.SpecialFunctions.Coupled.Scales.left_eigenvector_preserves_dot",
60       "line": 264
61     },
62     {
63       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_fixed_vectors",
64       "line": 272
65     },
66     {
67       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_fixed_proportion",
68       "line": 287
69     },
70     {
71       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_proportions",
72       "line": 329
73     },
74     {
75       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_positive_type_proportions",
76       "line": 345
77     },
78     {
79       "name": "Komorebi.SpecialFunctions.Coupled.Scales.characteristic_fixed_ratios",
80       "line": 355
81     },
82     {
83       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_ratios",
84       "line": 378
85     },
86     {
87       "name": "Komorebi.SpecialFunctions.Coupled.Scales.ordinary_type_limit_iff",
88       "line": 394
89     },
90     {
91       "name": "Komorebi.SpecialFunctions.Coupled.Scales.type_equality_iff_scalar_equality",
92       "line": 405
93     },
94     {
95       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_limit_equivalence",
96       "line": 421
97     },
98     {
99       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_limit_vector",
100       "line": 429
101     },
102     {
103       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_proportions",
104       "line": 444
105     },
106     {
107       "name": "Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_limit_equivalence",
108       "line": 462
109     }
110   ]
111 }

Back to source controls

Back to Special Functions