OAI/Computability/FourierTransform/TensorCertificate.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PowerSaving.Binary.shift_zero line 9
  2. theorem OAI.PowerSaving.Binary.terminal_calc line 13

    Source documentation

    Terminal exceptional ratio.

    theorem terminal_calc {α : Type*} [Fintype α] [DecidableEq α]
    (A : OBase α) (p : α) :
    kernel α * frame A {p} = shift (A.v p) * frame A (univ \ {p}) := by
…

    Mentions: OAI.PowerSaving.Binary.OBase, OAI.PowerSaving.Binary.kernel, OAI.PowerSaving.Binary.frame, OAI.PowerSaving.Binary.shift

  3. theorem OAI.PowerSaving.Binary.translateAll line 25
  4. theorem OAI.PowerSaving.Binary.framed_surj line 46
  5. def OAI.PowerSaving.Cluster.sink line 60
  6. lemma OAI.PowerSaving.Cluster.region_zero line 64
  7. lemma OAI.PowerSaving.Cluster.region_full line 68
  8. lemma OAI.PowerSaving.Cluster.border_inx line 73
  9. lemma OAI.PowerSaving.Cluster.border_iny line 74
  10. lemma OAI.PowerSaving.Cluster.border_inr line 77
  11. lemma OAI.PowerSaving.Cluster.border_le_sink line 79
  12. def OAI.PowerSaving.Cluster.exchange line 82
  13. lemma OAI.PowerSaving.Cluster.all_stages line 87
  14. lemma OAI.PowerSaving.Cluster.mass_groups line 98
  15. lemma OAI.PowerSaving.Cluster.mass_border line 112
  16. lemma OAI.PowerSaving.Cluster.mass_sink line 122
  17. def OAI.PowerSaving.Cluster.correction line 130
  18. def OAI.PowerSaving.Cluster.recover line 134
  19. def OAI.PowerSaving.Cluster.pull line 140

    Source comment

    monomial point move witnessing recovery
    def pull : Role → Role
  | .inl (.inl k) => gy k
  | .inl (.inr k) => gx k
  | r => r

    Mentions: OAI.PowerSaving.Cluster.Role, OAI.PowerSaving.Cluster.gy, OAI.PowerSaving.Cluster.gx

  20. def OAI.PowerSaving.Cluster.flipSign line 144
  21. def OAI.PowerSaving.Cluster.recoverM line 147
  22. lemma OAI.PowerSaving.Cluster.recover_eq line 150
  23. theorem OAI.PowerSaving.Cluster.netEffect line 158
  24. def OAI.PowerSaving.Cluster.nMoves line 180
  25. lemma OAI.PowerSaving.Cluster.c_tally line 182
  26. theorem OAI.PowerSaving.Cluster.certificate line 189

    Source documentation

    Finite certificate. No operation count for point work here: the word and matrices in the point moves have fixed size. It holds on arbitrary values in all roles, for any f columns of bits.

    theorem certificate :
    ∃ p : PWord Blocks Role,
    tally p = nMoves ∧
      ∀ f (x : Data Blocks Role f), walk f p x = multiAct f (fun _ => kernel Blocks) x := by
…

    Mentions: OAI.PowerSaving.Cluster.Blocks, OAI.PowerSaving.Cluster.Role, OAI.PowerSaving.Cluster.nMoves