OAI/LinearAlgebra/CirculantHadamard/BinaryLocalFamily.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CirculantHadamard.BinaryLocalFamily.evaluationUnit line 19

   Source documentation

   The actual local unit attached to one evaluated Gaussian norm element.

   def evaluationUnit (x : Elem GaussianRing (u ^ 2))
       (hx : x * ringStar x = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
       (S : Finset (PrimeIndex u)) : (O u)ˣ :=
   …

2. theorem OAI.CirculantHadamard.BinaryLocalFamily.evaluationUnit_val line 25
3. theorem OAI.CirculantHadamard.BinaryLocalFamily.contradiction_of_evaluated_data line 34

   Source documentation

   The concrete local argument. In particular, neither local units nor a nonzero residue sum are assumptions of this theorem.

   theorem contradiction_of_evaluated_data
       (C D G : Elem GaussianRing (u ^ 2))
       (hC : C * ringStar C = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
       (hD : D * ringStar D = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
       (hG : G * ringStar G = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
       (a b U : Finset (PrimeIndex u) → B u)
       (hc : ∀ S, subsetEvaluation u hu S C = a S + b S)
       (hd : ∀ S, subsetEvaluation u hu S D = a S - b S)
       (hg : ∀ S, subsetEvaluation u hu S G =
         a S + gaussianToB u gaussianI * b S -
           ((1 + gaussianToB u gaussianI) *
             subsetEvaluation u hu S (AddMonoidAlgebra.ofCoeff (BinaryCoefficients.JOver GaussianRing)) + 2 * U S))
   …

   Mentions: OAI.CirculantHadamard.BinaryCoefficients.JOver