OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedPairDerivativeCounts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.diagonal_prior_cells_card_le line 14
2. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.diagonal_prime_cells_card_le line 23
3. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.diagonal_mixed_cells_card_le line 29
4. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.diagonal_cells_card_le line 35
5. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.all_level_cells_add_two_le line 43
6. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.pair_key_sum_le_real line 61
7. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.counterpartWidths_le line 68
8. theorem OAI.Ostmann.Arithmetic.HistorySelectedPairDerivativeCounts.counterpartWidths_le_linear line 76