OAI/NumberTheory/Jacobsthal/Sieve/DivisorLogGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosDivisorBounds.prime_factor_product line 13
2. theorem OAI.Erdos970.ErdosDivisorBounds.small_factor_product line 30
3. theorem OAI.Erdos970.ErdosDivisorBounds.divisor_subpower line 42
4. theorem OAI.Erdos970.ErdosDivisorBounds.divisor_power_subpower line 70
5. theorem OAI.Erdos970.ErdosUniformMobiusRemainder.totient_ratio_le_divisors line 98
6. theorem OAI.Erdos970.ErdosUniformMobiusRemainder.divisor_totient_quarter line 110
7. theorem OAI.Erdos970.ErdosUniformMobiusRemainder.divisor_totient_length_bound line 122
8. theorem OAI.Erdos970.ErdosHyperbolaWeighted.divisor_log_square_subpower line 153