OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Shape.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.NumericalSubtrees.Shape line 18
2. def OAI.OrdinaryCorrelations.NumericalSubtrees.shapeEquiv line 22
3. instance OAI.OrdinaryCorrelations.NumericalSubtrees.(instance at line 29) line 29
4. instance OAI.OrdinaryCorrelations.NumericalSubtrees.(instance at line 30) line 30
5. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.sum_shapes line 32
6. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.core_shape_sum line 43
7. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.center_shape_sum line 53
8. def OAI.OrdinaryCorrelations.NumericalSubtrees.TokenType line 60
9. def OAI.OrdinaryCorrelations.NumericalSubtrees.tokenWeight line 62
10. def OAI.OrdinaryCorrelations.NumericalSubtrees.tokenMass line 66
11. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.tokenWeight_nonneg line 69
12. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.total_token_exponent line 73
13. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.untagged_exponential_bound line 86
14. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.tokenWeight_representative line 114