OAI/NumberTheory/SiegelZeros/Structure/PrimeCutBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W22.distinct_selected_factor_weight_le line 15
2. theorem OAI.SiegelZeros.WeightedTorusJets.W22.grouped_count_weighted_sum_eq line 41
3. theorem OAI.SiegelZeros.WeightedTorusJets.W22.component_multiplicity_sum_bound line 52
4. def OAI.SiegelZeros.WeightedTorusJets.W22.actualLocalLength line 159
5. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualLocalLength_spec line 164
6. theorem OAI.SiegelZeros.WeightedTorusJets.W22.primeCut_isHomogeneous line 182
7. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_prime_cut_degree_multiplicity line 195
8. theorem OAI.SiegelZeros.WeightedTorusJets.W22.prime_cut_component_budget line 215
9. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualHP_natDegree_of_prime_dimension line 242