OAI/Computability/FourierTransform/BinaryBasis.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Binary orthonormal bases and masks for the fixed saving.

  1. abbrev OAI.PowerSaving.Binary.F line 10
  2. abbrev OAI.PowerSaving.Binary.Space line 11
  3. lemma OAI.PowerSaving.Binary.bit_cases line 13
  4. theorem OAI.PowerSaving.Binary.cancel line 18
  5. theorem OAI.PowerSaving.Binary.binary_cancel line 21
  6. def OAI.PowerSaving.Binary.dot line 26
  7. theorem OAI.PowerSaving.Binary.dot_symm line 28
  8. theorem OAI.PowerSaving.Binary.dot_add_left line 30
  9. theorem OAI.PowerSaving.Binary.dot_add_right line 33
  10. theorem OAI.PowerSaving.Binary.dot_smul_left line 36
  11. theorem OAI.PowerSaving.Binary.dot_smul_right line 38
  12. theorem OAI.PowerSaving.Binary.dot_zero_left line 41
  13. theorem OAI.PowerSaving.Binary.dot_zero_right line 43
  14. theorem OAI.PowerSaving.Binary.dot_sum line 45
  15. def OAI.PowerSaving.Binary.eu line 54
  16. theorem OAI.PowerSaving.Binary.dot_eu_left line 56
  17. theorem OAI.PowerSaving.Binary.dot_eu_right line 58
  18. structure OAI.PowerSaving.Binary.OBase line 64

    Source documentation

    Represent an orthonormal basis with full index set α.

    structure OBase (α : Type*) [Fintype α] [DecidableEq α] where
…
  19. theorem OAI.PowerSaving.Binary.OBase.self line 71
  20. theorem OAI.PowerSaving.Binary.OBase.nz line 74
  21. theorem OAI.PowerSaving.Binary.OBase.cols line 80

    Source documentation

    Orthonormality of columns follows from the square matrix identity.

    theorem cols (A : OBase α) (i j : α) :
    ∑ k, A.v k i * A.v k j = if i=j then 1 else 0 := by
…

    Mentions: OAI.PowerSaving.Binary.OBase

  22. def OAI.PowerSaving.Binary.OBase.canonical line 89
  23. def OAI.PowerSaving.Binary.OBase.mat line 92
  24. theorem OAI.PowerSaving.Binary.OBase.mat_univ line 95
  25. theorem OAI.PowerSaving.Binary.OBase.mat_sub line 99
  26. def OAI.PowerSaving.Binary.OBase.proj line 106

    Source documentation

    Projection action.

    def proj (A : OBase α) (s : Finset α) (x : Space α) : Space α :=
…

    Mentions: OAI.PowerSaving.Binary.OBase, OAI.PowerSaving.Binary.Space

  27. theorem OAI.PowerSaving.Binary.OBase.proj_apply line 109
  28. theorem OAI.PowerSaving.Binary.OBase.proj_congr line 119
  29. theorem OAI.PowerSaving.Binary.OBase.proj_univ line 123
  30. theorem OAI.PowerSaving.Binary.OBase.dot_proj_omit line 126
  31. def OAI.PowerSaving.Binary.OBase.tv line 137

    Source documentation

    Transvection carrying a chosen coordinate vector to a given norm-one t on disjoint support.

    def tv (w x : Space α) := x + dot w x • w
…

    Mentions: OAI.PowerSaving.Binary.Space, OAI.PowerSaving.Binary.dot

  32. theorem OAI.PowerSaving.Binary.OBase.tv_isom line 140
  33. def OAI.PowerSaving.Binary.OBase.acted line 146
  34. def OAI.PowerSaving.Binary.OBase.adapt line 149
  35. theorem OAI.PowerSaving.Binary.OBase.adapt_pivot line 153
  36. theorem OAI.PowerSaving.Binary.OBase.adapt_other line 159
  37. def OAI.PowerSaving.Binary.OBase.pure line 168
  38. def OAI.PowerSaving.Binary.OBase.tensor line 171
  39. theorem OAI.PowerSaving.Binary.OBase.mat_rect line 184