CyclicNorm.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CirculantHadamard.CyclicSignRow line 13
Source documentation
Every literal integer coefficient is a sign.
```
def CyclicSignRow {n : ℕ} (f : CyclicRing.Elem ℤ n) : Prop :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem
def OAI.CirculantHadamard.cyclicRow line 21
Source documentation
The cyclic group-ring element whose coefficients are the given first row.
```
def cyclicRow (h : Fin n → ℤ) : CyclicRing.Elem ℤ n :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem
def OAI.CirculantHadamard.integerRow line 25
Source documentation
Recover the integer first row without changing the cyclic orientation.
```
def integerRow (f : CyclicRing.Elem ℤ n) : Fin n → ℤ :=
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem
theorem OAI.CirculantHadamard.cyclicRow_apply line 28
theorem OAI.CirculantHadamard.integerRow_apply line 32
theorem OAI.CirculantHadamard.cyclicRow_integerRow line 35
theorem OAI.CirculantHadamard.integerRow_cyclicRow line 42
theorem OAI.CirculantHadamard.sum_cyclicRow line 47
theorem OAI.CirculantHadamard.cyclicSignRow_cyclicRow_iff line 53
theorem OAI.CirculantHadamard.cyclicRow_norm_apply line 62
Source documentation
The norm coefficient uses the same j - a orientation as the row Gram.
```
theorem cyclicRow_norm_apply (h : Fin n → ℤ) (a : Fin n) :
    (cyclicRow h * CyclicRing.ringStar (cyclicRow h)).coeff (ZMod.finEquiv n a) =
      ∑ j : Fin n, h j * h (j - a) := by
…
```
Mentions: OAI.CirculantHadamard.cyclicRow, OAI.CirculantHadamard.CyclicRing.ringStar
theorem OAI.CirculantHadamard.cyclicRow_norm_iff_autocorrelation line 72
theorem OAI.CirculantHadamard.cyclicRow_norm_iff_gram line 91
theorem OAI.CirculantHadamard.integerSignRow_iff_cyclicSignNorm line 98
theorem OAI.CirculantHadamard.exists_cyclicSignRow_iff_real line 107
Source documentation
The literal sign norm equation is equivalent to the public real-matrix existence predicate. Neither direction assumes a mathematical bridge.
```
theorem exists_cyclicSignRow_iff_real :
    (∃ f : CyclicRing.Elem ℤ n,
      CyclicSignRow f ∧ f * CyclicRing.ringStar f = CyclicRing.scalar n (n : ℤ)) ↔
      ExistsRealCirculantHadamard n := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicSignRow, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar, OAI.CirculantHadamard.ExistsRealCirculantHadamard
theorem OAI.CirculantHadamard.cyclicNorm_identity_coeff line 120
Source documentation
The identity coefficient is the sum of the actual coefficient squares.
```
theorem cyclicNorm_identity_coeff (f : CyclicRing.Elem ℤ n) :
    (f * CyclicRing.ringStar f).coeff 0 = ∑ a : ZMod n, f.coeff a ^ 2 := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar
theorem OAI.CirculantHadamard.cyclicSignRow_identity_coeff line 124
theorem OAI.CirculantHadamard.augmentation_sum_sq_of_norm line 136
Source documentation
Evaluating the actual cyclic norm at the trivial character gives the square of the coefficient sum.
```
theorem augmentation_sum_sq_of_norm (f : CyclicRing.Elem ℤ n)
    (hf : f * CyclicRing.ringStar f = CyclicRing.scalar n (n : ℤ)) :
    (∑ a : ZMod n, f.coeff a) ^ 2 = (n : ℤ) := by
…
```
Mentions: OAI.CirculantHadamard.CyclicRing.Elem, OAI.CirculantHadamard.CyclicRing.ringStar, OAI.CirculantHadamard.CyclicRing.scalar