OAI/NumberTheory/SiegelZeros/EntireFunctions/FiniteNormalizationGrowth.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W24.totalDegree_aeval_le line 25
2. def OAI.SiegelZeros.WeightedTorusJets.W24.quotientDegreeFiltration line 55
3. instance OAI.SiegelZeros.WeightedTorusJets.W24.quotientDegreeFiltration_finite line 59
4. theorem OAI.SiegelZeros.WeightedTorusJets.W24.normalization_mem_quotientDegreeFiltration line 65
5. theorem OAI.SiegelZeros.WeightedTorusJets.W24.normalization_lower_growth line 81
6. def OAI.SiegelZeros.WeightedTorusJets.W29.boundedCoefficientMap line 121
7. def OAI.SiegelZeros.WeightedTorusJets.W29.generatorPiece line 128
8. lemma OAI.SiegelZeros.WeightedTorusJets.W29.mem_generatorPiece line 133
9. lemma OAI.SiegelZeros.WeightedTorusJets.W29.generatorPiece_mono line 144
10. instance OAI.SiegelZeros.WeightedTorusJets.W29.generatorPiece_finite line 150
11. lemma OAI.SiegelZeros.WeightedTorusJets.W29.finrank_generatorPiece_le line 155
12. lemma OAI.SiegelZeros.WeightedTorusJets.W29.mul_mem_generatorPiece line 168
13. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finite_multiplication_matrices line 200
14. lemma OAI.SiegelZeros.WeightedTorusJets.W29.variable_pow_mem_generatorPiece line 245
15. lemma OAI.SiegelZeros.WeightedTorusJets.W29.monomial_mem_generatorPiece line 261
16. lemma OAI.SiegelZeros.WeightedTorusJets.W29.polynomial_mem_generatorPiece line 288
17. theorem OAI.SiegelZeros.WeightedTorusJets.W29.finite_normalization_upper_growth line 311