OAI/NumberTheory/SiegelZeros/Hilbert/PrimeHilbertComparison.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.W25.quotientDegreeProjection line 30
  2. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientDegreeProjection_mk line 43
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientDegreeProjection_of_mem line 50
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientSection_iSupIndep line 65
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientSection_iSup_eq_top line 83
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientSection_isInternal line 91
  7. def OAI.SiegelZeros.WeightedTorusJets.W25.homogeneousQuotientDirectSumEquiv line 97
  8. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientSection_bounded_iSup_eq_top line 103
  9. def OAI.SiegelZeros.WeightedTorusJets.W25.boundedHomogeneousQuotientEquiv line 116
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W25.homogeneousQuotient_finite line 128
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W25.homogeneousQuotient_finrank_eq_sum line 134
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W27.prime_quotientSection_finrank_pos line 156
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W27.polynomial_leadingCoeff_nonneg_of_eventually_nonneg line 171
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W27.polynomial_leadingCoeff_pos_of_eventually_pos line 191
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W27.factorial_leadingCoeff_is_integer line 202
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W27.eventual_hilbert_degree_ge_one line 218
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W27.prime_eventual_hilbert_degree_ge_one line 235
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W27.prime_eventual_hilbert_coefficient_ge_one line 245
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W25.restrictTotalDegree_eq_iSup_homogeneous line 270
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientDegreeFiltration_eq_iSup_sections line 292
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W25.cumulativeSectionMap_injective line 299
  22. theorem OAI.SiegelZeros.WeightedTorusJets.W25.cumulativeSectionMap_range line 305
  23. def OAI.SiegelZeros.WeightedTorusJets.W25.cumulativeHomogeneousQuotientEquiv line 311
  24. theorem OAI.SiegelZeros.WeightedTorusJets.W25.cumulativeHomogeneousQuotientEquiv_apply line 320
  25. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientDegreeFiltration_finrank_eq_sum_fin line 329
  26. theorem OAI.SiegelZeros.WeightedTorusJets.W25.quotientDegreeFiltration_finrank_eq_sum line 337
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W24.natDegree_le_of_eventual_polynomial_le line 356
  28. theorem OAI.SiegelZeros.WeightedTorusJets.W24.natDegree_affine_comp_le line 367
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W24.natDegree_eq_of_polynomial_growth_bounds line 374
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W24.normalization_binomial_lower_bound line 407
  31. theorem OAI.SiegelZeros.WeightedTorusJets.W24.normalization_binomial_lower_growth line 426
  32. theorem OAI.SiegelZeros.WeightedTorusJets.W24.prime_quotientDegreeFiltration_finrank_pos line 441
  33. theorem OAI.SiegelZeros.WeightedTorusJets.W24.prime_hilbert_natDegree_add_one_eq_krullDim line 452
  34. theorem OAI.SiegelZeros.WeightedTorusJets.W24.exists_prime_hilbert_polynomial_with_dimension line 496