OAI/Computability/FourierTransform/PrimeSelection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.Selection.stackN line 10
2. lemma OAI.PowerSaving.Selection.stack_pos line 12
3. lemma OAI.PowerSaving.Selection.stack_above line 14
4. lemma OAI.PowerSaving.Selection.stack_pow line 18
5. lemma OAI.PowerSaving.Selection.stack_le line 23
6. def OAI.PowerSaving.Selection.silo line 26
7. lemma OAI.PowerSaving.Selection.silo_big line 28
8. lemma OAI.PowerSaving.Selection.harvest line 32
9. def OAI.PowerSaving.Selection.Bar line 72

   Source comment

   odd primes up to and excluding limit

   def Bar (i : ℕ) := Nat.Prime i ∧ i>2

10. instance OAI.PowerSaving.Selection.(instance at line 73) line 73
11. def OAI.PowerSaving.Selection.bars line 74
12. lemma OAI.PowerSaving.Selection.bars_step line 75
13. lemma OAI.PowerSaving.Selection.bars_zero line 76
14. lemma OAI.PowerSaving.Selection.bars_count line 78
15. lemma OAI.PowerSaving.Selection.bar_bounds line 100