OAI/LinearAlgebra/CirculantHadamard/BinaryCoefficients.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CirculantHadamard.BinaryCoefficients.halfSum line 17
  2. def OAI.CirculantHadamard.BinaryCoefficients.halfDiff line 19
  3. def OAI.CirculantHadamard.BinaryCoefficients.signOffset line 21
  4. theorem OAI.CirculantHadamard.BinaryCoefficients.two_halfSum line 23
  5. theorem OAI.CirculantHadamard.BinaryCoefficients.two_halfDiff line 27
  6. theorem OAI.CirculantHadamard.BinaryCoefficients.halfDiff_eq line 31
  7. theorem OAI.CirculantHadamard.BinaryCoefficients.two_signOffset line 35
  8. theorem OAI.CirculantHadamard.BinaryCoefficients.sign_eq_one_add line 39
  9. def OAI.CirculantHadamard.BinaryCoefficients.castCoeffs line 46

    Source documentation

    The canonical coefficient map, with no change to the index.

    noncomputable def castCoeffs {R : Type uR} [Ring R] (f : G →₀ ℤ) : G →₀ R :=
…
  10. theorem OAI.CirculantHadamard.BinaryCoefficients.castCoeffs_apply line 49
  11. def OAI.CirculantHadamard.BinaryCoefficients.complexify line 52
  12. theorem OAI.CirculantHadamard.BinaryCoefficients.complexify_apply line 54
  13. theorem OAI.CirculantHadamard.BinaryCoefficients.complexify_add line 57
  14. theorem OAI.CirculantHadamard.BinaryCoefficients.complexify_sub line 62
  15. theorem OAI.CirculantHadamard.BinaryCoefficients.complexify_int_smul line 67
  16. def OAI.CirculantHadamard.BinaryCoefficients.liftPair line 74

    Source documentation

    Integer real and imaginary parts interpreted in any coefficient ring. The linear identities do not require an equation such as i^2 = -1.

    noncomputable def liftPair {R : Type uR} [CommRing R] (i : R) (f h : G →₀ ℤ) : G →₀ R :=
…
  17. def OAI.CirculantHadamard.BinaryCoefficients.ofCoeffs line 79
  18. theorem OAI.CirculantHadamard.BinaryCoefficients.ofCoeffs_apply line 82
  19. def OAI.CirculantHadamard.BinaryCoefficients.Signs line 86

    Source documentation

    Literal sign hypotheses for the four blocks, without a norm premise.

    def Signs (H : Fin 4 → (G →₀ ℤ)) : Prop := ∀ j x, IsSign (H j x)

    Mentions: OAI.CirculantHadamard.IsSign

  20. def OAI.CirculantHadamard.BinaryCoefficients.a line 88
  21. def OAI.CirculantHadamard.BinaryCoefficients.b line 91
  22. def OAI.CirculantHadamard.BinaryCoefficients.c line 94
  23. def OAI.CirculantHadamard.BinaryCoefficients.d line 96
  24. def OAI.CirculantHadamard.BinaryCoefficients.gReal line 98
  25. def OAI.CirculantHadamard.BinaryCoefficients.gImag line 101
  26. def OAI.CirculantHadamard.BinaryCoefficients.gOver line 104
  27. def OAI.CirculantHadamard.BinaryCoefficients.g line 107
  28. def OAI.CirculantHadamard.BinaryCoefficients.UReal line 109
  29. def OAI.CirculantHadamard.BinaryCoefficients.UImag line 112
  30. def OAI.CirculantHadamard.BinaryCoefficients.UOver line 115
  31. def OAI.CirculantHadamard.BinaryCoefficients.U line 118
  32. def OAI.CirculantHadamard.BinaryCoefficients.JOver line 122

    Source documentation

    This is the sum of all group elements (every coefficient is one), not the scalar one in a convolution ring.

    noncomputable def JOver (R : Type uR) [CommRing R] : G →₀ R := ofCoeffs fun _ => 1

    Mentions: OAI.CirculantHadamard.BinaryCoefficients.ofCoeffs

  33. theorem OAI.CirculantHadamard.BinaryCoefficients.JOver_apply line 124
  34. def OAI.CirculantHadamard.BinaryCoefficients.J line 127
  35. theorem OAI.CirculantHadamard.BinaryCoefficients.J_apply line 129
  36. theorem OAI.CirculantHadamard.BinaryCoefficients.two_a line 131
  37. theorem OAI.CirculantHadamard.BinaryCoefficients.two_b line 137
  38. theorem OAI.CirculantHadamard.BinaryCoefficients.two_c line 143
  39. theorem OAI.CirculantHadamard.BinaryCoefficients.two_d line 148
  40. theorem OAI.CirculantHadamard.BinaryCoefficients.gOver_eq_ab line 153
  41. theorem OAI.CirculantHadamard.BinaryCoefficients.two_gOver line 164
  42. theorem OAI.CirculantHadamard.BinaryCoefficients.binary_identity_over line 180

    Source documentation

    The binary identity with an explicitly constructed integral-pair U.

    theorem binary_identity_over {R : Type uR} [CommRing R] (i : R)
    {H : Fin 4 → (G →₀ ℤ)} (hH : Signs H) :
    castCoeffs (H 2) + i • castCoeffs (H 3) =
      (1 + i) • (JOver R : G →₀ R) + (2 : R) • UOver i H := by
…

    Mentions: OAI.CirculantHadamard.BinaryCoefficients.Signs, OAI.CirculantHadamard.BinaryCoefficients.castCoeffs, OAI.CirculantHadamard.BinaryCoefficients.JOver, OAI.CirculantHadamard.BinaryCoefficients.UOver

  43. theorem OAI.CirculantHadamard.BinaryCoefficients.g_eq_ab line 193
  44. theorem OAI.CirculantHadamard.BinaryCoefficients.two_g line 198
  45. theorem OAI.CirculantHadamard.BinaryCoefficients.binary_identity line 203