OAI/Computability/FourierTransform/DirectionalWords.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

A word whose directional steps will become recursive tensor calls. The frame-path bookkeeping suffices to prove it at every amplification.

  1. abbrev OAI.PowerSaving.Binary.Sky line 11
  2. abbrev OAI.PowerSaving.Binary.Data line 12
  3. def OAI.PowerSaving.Binary.matAct line 17
  4. theorem OAI.PowerSaving.Binary.matAct_mul line 21
  5. theorem OAI.PowerSaving.Binary.matAct_one line 25
  6. def OAI.PowerSaving.Binary.multiAct line 28
  7. def OAI.PowerSaving.Binary.roleAct line 31
  8. lemma OAI.PowerSaving.Binary.roleAct_mul line 34
  9. def OAI.PowerSaving.Binary.point line 39
  10. inductive OAI.PowerSaving.Binary.Move line 47
  11. def OAI.PowerSaving.Binary.toll line 52
  12. abbrev OAI.PowerSaving.Binary.PWord line 56
  13. def OAI.PowerSaving.Binary.tally line 58
  14. theorem OAI.PowerSaving.Binary.tally_append line 60
  15. def OAI.PowerSaving.Binary.actPoint line 64
  16. def OAI.PowerSaving.Binary.Move.go line 66
  17. def OAI.PowerSaving.Binary.walk line 71
  18. theorem OAI.PowerSaving.Binary.walk_append line 74
  19. def OAI.PowerSaving.Binary.mass line 78

    Source documentation

    Frame mass.

    def mass (s : ρ → Finset α) := ∑ r, (s r).card
  20. def OAI.PowerSaving.Binary.loss line 79
  21. def OAI.PowerSaving.Binary.withFrame line 81
  22. def OAI.PowerSaving.Binary.Path line 86

    Source documentation

    A point map surrounded by frame changes. The path identity applies to arbitrary initial arrays. losses accounts for decreases in dimension (shifts free).

    def Path (A : ρ → OBase α) (s t : ρ → Finset α)
    (g : (ρ→ℂ) → (ρ→ℂ)) (losses : ℕ) : Prop :=
…

    Mentions: OAI.PowerSaving.Binary.OBase

  23. theorem OAI.PowerSaving.Binary.Path.refl line 96
  24. theorem OAI.PowerSaving.Binary.Path.trans line 100
  25. theorem OAI.PowerSaving.Binary.Path.gate line 109

    Source documentation

    Move through a gate. Its nonzero entries must stay within a common frame.

    theorem gate (g : Matrix ρ ρ ℚ)
    (cond : ∀ i j, g i j ≠ 0 → frame (A i) (s i) = frame (A j) (s j)) :
    Path A s s (actPoint g) 0 := by
…

    Mentions: OAI.PowerSaving.Binary.frame, OAI.PowerSaving.Binary.Path, OAI.PowerSaving.Binary.actPoint

  26. theorem OAI.PowerSaving.Binary.Path.change_one line 132

    Source documentation

    One new line both upwards and downwards.

    theorem change_one (s : ρ → Finset α) (r : ρ) (i : α) (hi : i ∉ s r) :
    let t := fun j => if j=r then insert i (s j) else s j
…
  27. theorem OAI.PowerSaving.Binary.Path.reframe_le line 181

    Source documentation

    Comparable mask sets.

    private theorem reframe_le (x y : ρ → Finset α) (h : ∀ r, x r ⊆ y r) :
    Path A x y id 0 ∧ Path A y x id (loss y x) := by
…

    Mentions: OAI.PowerSaving.Binary.Path, OAI.PowerSaving.Binary.loss

  28. theorem OAI.PowerSaving.Binary.Path.reframe line 234
  29. theorem OAI.PowerSaving.Binary.Path.inc line 246