OAI/Computability/FourierTransform/LengthSelection.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PowerSaving.Selection.Cart line 10
  2. def OAI.PowerSaving.Selection.Cart.empty line 17
  3. def OAI.PowerSaving.Selection.Cart.pushQ line 18
  4. structure OAI.PowerSaving.Selection.Cart.Square line 21
  5. lemma OAI.PowerSaving.Selection.Cart.Square.empty line 25
  6. lemma OAI.PowerSaving.Selection.Cart.push_eq line 30
  7. lemma OAI.PowerSaving.Selection.Cart.push_ext line 33
  8. lemma OAI.PowerSaving.Selection.Cart.at_push line 39
  9. lemma OAI.PowerSaving.Selection.Cart.Square.pushQ line 42
  10. def OAI.PowerSaving.Selection.reap line 65
  11. structure OAI.PowerSaving.Selection.Baler line 71
  12. lemma OAI.PowerSaving.Selection.Baler.empty line 83
  13. lemma OAI.PowerSaving.Selection.Baler.push line 87
  14. lemma OAI.PowerSaving.Selection.Baler.pass line 114
  15. lemma OAI.PowerSaving.Selection.reap_baler line 126
  16. def OAI.PowerSaving.Selection.harvestN line 134
  17. def OAI.PowerSaving.Selection.bed line 135
  18. def OAI.PowerSaving.Selection.fill line 138

    Source comment

    choose dyad by doubling until ≥N
    def fill (N p : ℕ) : ℕ→ℕ
  | 0 => 1
  | k+1 => let q := fill N p k
…
  19. lemma OAI.PowerSaving.Selection.Fill.capacity line 145
  20. lemma OAI.PowerSaving.Selection.Fill.fills line 151
  21. lemma OAI.PowerSaving.Selection.Fill.radius line 159
  22. lemma OAI.PowerSaving.Selection.Fill.dyad line 166
  23. def OAI.PowerSaving.Selection.bead line 176
  24. def OAI.PowerSaving.Selection.barge line 178
  25. def OAI.PowerSaving.Selection.orderE line 180
  26. lemma OAI.PowerSaving.Selection.orderE_big line 182
  27. lemma OAI.PowerSaving.Selection.orderE_small line 187
  28. structure OAI.PowerSaving.Selection.Harbor line 195
  29. theorem OAI.PowerSaving.Selection.barge_spec line 202
  30. def OAI.PowerSaving.Selection.Ports line 257

    Source comment

    explicitly chosen root-order depending on size branch
    def Ports (n : ℕ) := 2^orderE n ≤ n

    Mentions: OAI.PowerSaving.Selection.orderE

  31. instance OAI.PowerSaving.Selection.(instance at line 258) line 258
  32. def OAI.PowerSaving.Selection.express line 259
  33. def OAI.PowerSaving.Selection.receipt line 260
  34. theorem OAI.PowerSaving.Selection.receipt_bound line 262
  35. lemma OAI.PowerSaving.Selection.express_eta line 284
  36. lemma OAI.PowerSaving.Selection.express_volume line 285
  37. lemma OAI.PowerSaving.Selection.express_halo line 286
  38. lemma OAI.PowerSaving.Selection.express_I line 288