OAI/NumberTheory/SiegelZeros/Selection/GreedyPivotsWeightLowSpan.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.greedyPivots_weight_le_of_low_span line 13
2. theorem OAI.SiegelZeros.WeightedTorusJets.span_low_sequence_eq_top_of_coverage line 33
3. theorem OAI.SiegelZeros.WeightedTorusJets.finite_sorted_greedy_weight_le_of_spanning_cutoff line 52
4. theorem OAI.SiegelZeros.WeightedTorusJets.finiteGreedyPivots_weight_le_of_spanning_cutoff line 87
5. theorem OAI.SiegelZeros.WeightedTorusJets.fixed_first_greedy_rectangle_weight_bound line 104
6. theorem OAI.SiegelZeros.WeightedTorusJets.finiteGreedyPivots_restrictWeightSortedEquiv_map line 133
7. theorem OAI.SiegelZeros.WeightedTorusJets.finiteGreedyPivots_restrictWeightSortedEquiv line 150
8. theorem OAI.SiegelZeros.WeightedTorusJets.sum_embedding_eq_sum_finset_of_range line 162