OAI/NumberTheory/Jacobsthal/Siegel/GreedyPivotsWeightLowSpan.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.greedyPivots_weight_le_of_low_span line 15
2. theorem OAI.Erdos970.WeightedTorusJets.span_low_sequence_eq_top_of_coverage line 35
3. theorem OAI.Erdos970.WeightedTorusJets.finite_sorted_greedy_weight_le_of_spanning_cutoff line 54
4. theorem OAI.Erdos970.WeightedTorusJets.finiteGreedyPivots_weight_le_of_spanning_cutoff line 89
5. theorem OAI.Erdos970.WeightedTorusJets.fixed_first_greedy_rectangle_weight_bound line 106
6. theorem OAI.Erdos970.WeightedTorusJets.finiteGreedyPivots_restrictWeightSortedEquiv_map line 135
7. theorem OAI.Erdos970.WeightedTorusJets.finiteGreedyPivots_restrictWeightSortedEquiv line 152
8. theorem OAI.Erdos970.WeightedTorusJets.sum_embedding_eq_sum_finset_of_range line 164