ProjectionCoefficients.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Coefficients of cyclic quotient maps

The coefficient at an element of the quotient is the sum over its entire fiber. For the quotient of order 2 * m onto order m, the fiber consists of the two representatives j.val and j.val + m.

theorem OAI.CirculantHadamard.mapDomain_apply_sum line 25

Source documentation

Mapping the domain adds precisely the coefficients in a quotient fiber.

theorem mapDomain_apply_sum (q : A → B) (f : A →₀ R) (b : B) :
    Finsupp.mapDomain q f b = ∑ a ∈ Finset.univ.filter (fun a => q a = b), f a := by
…

theorem OAI.CirculantHadamard.mapDomain_apply_fiber line 36

Source documentation

The same coefficient formula, indexed by the subtype of the fiber.

theorem mapDomain_apply_fiber (q : A → B) (f : A →₀ R) (b : B) :
    Finsupp.mapDomain q f b = ∑ a : {a : A // q a = b}, f a.val := by
…

theorem OAI.CirculantHadamard.cyclicProjection_apply_sum line 49

Source documentation

Coefficients of the actual cyclic group-ring quotient as a finite filter sum.

theorem cyclicProjection_apply_sum {m n : ℕ} [NeZero n] (h : m ∣ n)
    (f : CyclicRing.Elem R n) (a : ZMod m) :
    (cyclicProjection R h f).coeff a =
      ∑ x ∈ Finset.univ.filter (fun x : ZMod n =>
        ZMod.castHom h (ZMod m) x = a), f.coeff x := by
…

Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.cyclicProjection

theorem OAI.CirculantHadamard.cyclicProjection_apply_fiber line 58
Source documentation
Coefficients of the actual cyclic group-ring quotient as a fiber subtype sum.
```
theorem cyclicProjection_apply_fiber {m n : ℕ} [NeZero n] (h : m ∣ n)
    (f : CyclicRing.Elem R n) (a : ZMod m) :
    (cyclicProjection R h f).coeff a =
      ∑ x : {x : ZMod n // ZMod.castHom h (ZMod m) x = a}, f.coeff x.val := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.cyclicProjection

theorem OAI.CirculantHadamard.cyclicProjection_double_apply line 66

Source documentation

A quotient by the subgroup of order two adds opposite coefficients.

theorem cyclicProjection_double_apply {m : ℕ} (hm : 0 < m) (h : m ∣ 2 * m)
    (f : CyclicRing.Elem R (2 * m)) (j : ZMod m) :
    (cyclicProjection R h f).coeff j =
      f.coeff (j.val : ZMod (2 * m)) + f.coeff ((j.val + m : ℕ) : ZMod (2 * m)) := by
…

Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.cyclicProjection