OAI/Computability/FourierTransform/ChineseRemainder.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

CRT permutations. Using the same scaled index for input and output, and the appropriate primitive root on each axis.

  1. structure OAI.PowerSaving.Grove.Isles line 10
  2. lemma OAI.PowerSaving.Grove.Isles.cut line 14
  3. lemma OAI.PowerSaving.Grove.Isles.axis_dvd line 17
  4. def OAI.PowerSaving.Grove.tide line 27
  5. def OAI.PowerSaving.Grove.ford line 30

    Source documentation

    Recursively mixed-radix → one-dimensional index.

    def ford (r : Axes) : ℕ → ℕ → ℕ
  | 0 => fun _ => 0
  | l+1 => fun i =>
    tide (extent r l) (r l) (ford r l (i/r l)) (i%r l)

    Mentions: OAI.PowerSaving.Grove.Axes, OAI.PowerSaving.Grove.tide, OAI.PowerSaving.Grove.extent

  6. def OAI.PowerSaving.Grove.spray line 35
  7. def OAI.PowerSaving.Grove.gale line 37
  8. lemma OAI.PowerSaving.Grove.spray_here line 39
  9. lemma OAI.PowerSaving.Grove.spray_tide line 42
  10. lemma OAI.PowerSaving.Grove.spray_sec line 49
  11. lemma OAI.PowerSaving.Grove.spray_axis line 56
  12. lemma OAI.PowerSaving.Grove.gale_mod line 76
  13. lemma OAI.PowerSaving.Grove.gale_tide line 83
  14. lemma OAI.PowerSaving.Grove.canopy_gale line 92
  15. lemma OAI.PowerSaving.Grove.tide_left line 114
  16. lemma OAI.PowerSaving.Grove.tide_right line 120
  17. lemma OAI.PowerSaving.Grove.tide_inj line 125
  18. theorem OAI.PowerSaving.Grove.ford_rel line 133
  19. lemma OAI.PowerSaving.Grove.graft_ford line 149