OAI/LinearAlgebra/CirculantHadamard/BinaryEvaluation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of the actual binary coefficient construction

The integral c,d are mapped coefficientwise into the Gaussian subring, with their proved convolution norms preserved. All values are taken by the constructed prime-subset character map into the actual cyclotomic ring B u. The norm equations follow from the original cyclic sign row.

  1. def OAI.CirculantHadamard.BinaryEvaluation.gaussianScale line 35

    Source documentation

    The canonical coefficient action, with its group-algebra result type fixed.

    def gaussianScale {n : ℕ} (r : GaussianRing) (x : Elem GaussianRing n) :
    Elem GaussianRing n :=
…
  2. theorem OAI.CirculantHadamard.BinaryEvaluation.gaussianScale_apply line 41
  3. theorem OAI.CirculantHadamard.BinaryEvaluation.castCoeffs_add line 49
  4. theorem OAI.CirculantHadamard.BinaryEvaluation.castCoeffs_sub line 60
  5. theorem OAI.CirculantHadamard.BinaryEvaluation.castCoeffs_mul line 70
  6. theorem OAI.CirculantHadamard.BinaryEvaluation.castCoeffs_ringStar line 84
  7. theorem OAI.CirculantHadamard.BinaryEvaluation.castCoeffs_scalar line 93
  8. theorem OAI.CirculantHadamard.BinaryEvaluation.castCoeffs_norm line 103

    Source documentation

    Coefficient maps preserve the norm equation.

    theorem castCoeffs_norm [StarRing R] (f : Elem ℤ n) (r : ℕ)
    (hf : f * ringStar f = scalar n (r : ℤ)) :
    Mul.mul (α := Elem R n) (AddMonoidAlgebra.ofCoeff (castCoeffs f.coeff))
…
  9. def OAI.CirculantHadamard.BinaryEvaluation.aG line 118
  10. def OAI.CirculantHadamard.BinaryEvaluation.bG line 120
  11. def OAI.CirculantHadamard.BinaryEvaluation.cG line 122
  12. def OAI.CirculantHadamard.BinaryEvaluation.dG line 124
  13. def OAI.CirculantHadamard.BinaryEvaluation.gG line 126
  14. def OAI.CirculantHadamard.BinaryEvaluation.UG line 128
  15. def OAI.CirculantHadamard.BinaryEvaluation.JG line 130
  16. theorem OAI.CirculantHadamard.BinaryEvaluation.cG_eq line 132
  17. theorem OAI.CirculantHadamard.BinaryEvaluation.dG_eq line 136
  18. theorem OAI.CirculantHadamard.BinaryEvaluation.gG_eq line 140
  19. theorem OAI.CirculantHadamard.BinaryEvaluation.cG_norm line 163
  20. theorem OAI.CirculantHadamard.BinaryEvaluation.dG_norm line 171
  21. def OAI.CirculantHadamard.BinaryEvaluation.iB line 185
  22. def OAI.CirculantHadamard.BinaryEvaluation.aValue line 187
  23. def OAI.CirculantHadamard.BinaryEvaluation.bValue line 189
  24. def OAI.CirculantHadamard.BinaryEvaluation.cValue line 191
  25. def OAI.CirculantHadamard.BinaryEvaluation.dValue line 193
  26. def OAI.CirculantHadamard.BinaryEvaluation.gValue line 195
  27. def OAI.CirculantHadamard.BinaryEvaluation.UValue line 197
  28. def OAI.CirculantHadamard.BinaryEvaluation.JValue line 199
  29. theorem OAI.CirculantHadamard.BinaryEvaluation.subsetEvaluation_smul line 201
  30. theorem OAI.CirculantHadamard.BinaryEvaluation.cValue_eq line 215
  31. theorem OAI.CirculantHadamard.BinaryEvaluation.dValue_eq line 219
  32. theorem OAI.CirculantHadamard.BinaryEvaluation.gValue_eq line 223
  33. theorem OAI.CirculantHadamard.BinaryEvaluation.evaluated_norms line 231
  34. theorem OAI.CirculantHadamard.BinaryEvaluation.gaussian_norms_of_cyclic_norm line 246

    Source documentation

    All three Gaussian norm equations come from the original cyclic sign row.

    theorem gaussian_norms_of_cyclic_norm {u : ℕ} [NeZero u] (hu : Odd u)
    (f : Elem ℤ (4 * u ^ 2)) (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * ringStar f = scalar (4 * u ^ 2) ((4 * u ^ 2 : ℕ) : ℤ)) :
    let H := BinaryBlocks.blocks (BinaryBlocks.crt ℤ u hu f)
…

    Mentions: OAI.CirculantHadamard.IsSign, OAI.CirculantHadamard.BinaryBlocks.blocks, OAI.CirculantHadamard.BinaryBlocks.crt

  35. theorem OAI.CirculantHadamard.BinaryEvaluation.binary_evaluation_of_cyclic_norm line 258

    Source documentation

    Actual subset evaluations of c,d,g all have star norm u², without independent binary-element norm assumptions.

    theorem binary_evaluation_of_cyclic_norm {u : ℕ} [NeZero u] (hu : Odd u)
    (f : Elem ℤ (4 * u ^ 2)) (hsign : ∀ a, IsSign (f.coeff a))
    (hnorm : f * ringStar f = scalar (4 * u ^ 2) ((4 * u ^ 2 : ℕ) : ℤ))
    (S : Finset (PrimeIndex u)) :
    let hp : 0 < u := Nat.pos_of_ne_zero (NeZero.ne u)
…

    Mentions: OAI.CirculantHadamard.IsSign