AuxiliaryGram.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Auxiliary-column Gram matrices

The functions in manuscript §4 are interpreted, with the same sampled column in all factors. Real Gram forms are nonnegative for any real positive semidefinite coefficient matrix. No numerical certificate is assumed here.

def OAI.MUB6.realGram line 23
Source documentation
Real Gram pairing on a uniformly sampled finite space.
```
def realGram {Ω : Type*} [Fintype Ω] (F G : Ω → ℂ) : ℝ :=
…
```
lemma OAI.MUB6.realGram_sum_left line 29
lemma OAI.MUB6.realGram_sum_right line 33
lemma OAI.MUB6.realGram_smul_left line 37
lemma OAI.MUB6.realGram_smul_right line 41
lemma OAI.MUB6.realGram_weighted_sum line 47
lemma OAI.MUB6.realGram_symm line 61
theorem OAI.MUB6.realGram_psd_nonneg line 69
Source documentation
A real positive semidefinite matrix gives a nonnegative Gram form of any finite family of complex-valued random variables.
```
theorem realGram_psd_nonneg [DecidableEq ι] (Z : Matrix ι ι ℝ) (hZ : Z.PosSemidef)
    (F : ι → Ω → ℂ) : 0 ≤ ∑ i, ∑ j, Z i j * realGram (F i) (F j) := by
…
```
Mentions: OAI.MUB6.realGram
abbrev OAI.MUB6.AuxiliarySample line 94
Source documentation
Reference index, row bijection, nonreference-label bijection, and a column of the matrix assigned label zero.
```
abbrev AuxiliarySample := Fin 7 × (Coord ↪ Coord) × (Coord ↪ Coord) × Coord
```
Mentions: OAI.MUB6.Coord
def OAI.MUB6.auxiliaryCharacter line 97
Source documentation
The character of the shared sampled column, before any Fourier average.
```
def auxiliaryCharacter (B : Fin 7 → Basis) (a : Charge) (ω : AuxiliarySample) : ℂ :=
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.Charge, OAI.MUB6.AuxiliarySample
def OAI.MUB6.elementaryAuxiliary line 102
Source documentation
One Fourier factor, labelled s, multiplied by the inverse character of the same auxiliary column used by all factors.
```
def elementaryAuxiliary (B : Fin 7 → Basis) (s : Coord) (a : Charge)
    (ω : AuxiliarySample) : ℂ :=
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.Coord, OAI.MUB6.Charge, OAI.MUB6.AuxiliarySample
def OAI.MUB6.auxiliaryF line 107
Source documentation
Manuscript F₀ and F₁; the latter averages the five nonzero labels.
```
def auxiliaryF (B : Fin 7 → Basis) (t : Fin 2) (a : Charge) : AuxiliarySample → ℂ :=
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.Charge, OAI.MUB6.AuxiliarySample
def OAI.MUB6.gramCharges line 112
Source documentation
The three charges produced by integrating out the shared column.
```
def gramCharges (a v : Charge) : Matrix Coord (Fin 3) ℤ :=
…
```
Mentions: OAI.MUB6.Charge, OAI.MUB6.Coord
def OAI.MUB6.gramLabels line 115
lemma OAI.MUB6.average_column_re line 117
lemma OAI.MUB6.auxiliaryCharacter_product line 121
lemma OAI.MUB6.elementaryAuxiliary_product line 133
lemma OAI.MUB6.elementaryAuxiliary_column_average line 148
theorem OAI.MUB6.elementaryAuxiliary_gram line 163
Source documentation
Integrating out the common column gives a three-factor mixed moment.
```
theorem elementaryAuxiliary_gram (B : Fin 7 → Basis) (hB : IsMUBFamily B)
    (s t : Coord) (a v : Charge) :
    realGram (elementaryAuxiliary B s a) (elementaryAuxiliary B t v) =
      mixedMoment B (gramCharges a v) (gramLabels s t) := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Coord, OAI.MUB6.Charge, OAI.MUB6.realGram, OAI.MUB6.elementaryAuxiliary, OAI.MUB6.mixedMoment, OAI.MUB6.gramCharges, OAI.MUB6.gramLabels
lemma OAI.MUB6.auxiliaryF_one_source line 182
Source documentation
The literal source formula for F₁, with its shared column factor outside the average over the five other labels.
```
lemma auxiliaryF_one_source (B : Fin 7 → Basis) (a : Charge) (ω : AuxiliarySample) :
    auxiliaryF B 1 a ω =
      ((5 : ℂ)⁻¹ * ∑ s : Fin 5,
        rowFourier (relativeMatrix B ω.1 (ω.2.2.1 s.succ)) ω.2.1 a) *
        auxiliaryCharacter B (-a) ω := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.Charge, OAI.MUB6.AuxiliarySample, OAI.MUB6.auxiliaryF, OAI.MUB6.rowFourier, OAI.MUB6.relativeMatrix, OAI.MUB6.auxiliaryCharacter
def OAI.MUB6.pairLabelEmbedding line 189
def OAI.MUB6.tripleLabelEmbedding line 195
lemma OAI.MUB6.pair_labels_relabel line 201
lemma OAI.MUB6.gramMoment_zero_succ line 208
lemma OAI.MUB6.gramMoment_succ_zero line 220
lemma OAI.MUB6.gramMoment_succ_self line 232
lemma OAI.MUB6.gramMoment_succ_distinct line 244
lemma OAI.MUB6.auxiliaryF_zero line 254
lemma OAI.MUB6.auxiliaryF_one line 257
theorem OAI.MUB6.auxiliaryGram_zero_zero line 263
Source documentation
The (0,0) case of the manuscript Gram formula.
```
theorem auxiliaryGram_zero_zero (B : Fin 7 → Basis) (hB : IsMUBFamily B) (a v : Charge) :
    realGram (auxiliaryF B 0 a) (auxiliaryF B 0 v) =
      mixedMoment B (gramCharges a v) (gramLabels 0 0) := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Charge, OAI.MUB6.realGram, OAI.MUB6.auxiliaryF, OAI.MUB6.mixedMoment, OAI.MUB6.gramCharges, OAI.MUB6.gramLabels
theorem OAI.MUB6.auxiliaryGram_zero_one line 269
Source documentation
The (0,1) case of the manuscript Gram formula.
```
theorem auxiliaryGram_zero_one (B : Fin 7 → Basis) (hB : IsMUBFamily B) (a v : Charge) :
    realGram (auxiliaryF B 0 a) (auxiliaryF B 1 v) =
      mixedMoment B (gramCharges a v) (gramLabels 0 1) := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Charge, OAI.MUB6.realGram, OAI.MUB6.auxiliaryF, OAI.MUB6.mixedMoment, OAI.MUB6.gramCharges, OAI.MUB6.gramLabels
theorem OAI.MUB6.auxiliaryGram_one_zero line 278
Source documentation
The (1,0) case of the manuscript Gram formula.
```
theorem auxiliaryGram_one_zero (B : Fin 7 → Basis) (hB : IsMUBFamily B) (a v : Charge) :
    realGram (auxiliaryF B 1 a) (auxiliaryF B 0 v) =
      mixedMoment B (gramCharges a v) (gramLabels 1 0) := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Charge, OAI.MUB6.realGram, OAI.MUB6.auxiliaryF, OAI.MUB6.mixedMoment, OAI.MUB6.gramCharges, OAI.MUB6.gramLabels
lemma OAI.MUB6.five_by_five_same_different line 286
theorem OAI.MUB6.auxiliaryGram_one_one line 296
Source documentation
Five diagonal and twenty off-diagonal choices produce the exact 1/5 and 4/5 coefficients in the (1,1) Gram entry.
```
theorem auxiliaryGram_one_one (B : Fin 7 → Basis) (hB : IsMUBFamily B) (a v : Charge) :
    realGram (auxiliaryF B 1 a) (auxiliaryF B 1 v) =
      (1 / 5 : ℝ) * mixedMoment B (gramCharges a v) (gramLabels 1 1) +
      (4 / 5 : ℝ) * mixedMoment B (gramCharges a v) (gramLabels 1 2) := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Charge, OAI.MUB6.realGram, OAI.MUB6.auxiliaryF, OAI.MUB6.mixedMoment, OAI.MUB6.gramCharges, OAI.MUB6.gramLabels

theorem OAI.MUB6.auxiliaryGram_other line 317

Source documentation

A uniform statement of all three entries other than (1,1).

theorem auxiliaryGram_other (B : Fin 7 → Basis) (hB : IsMUBFamily B)
    (s t : Fin 2) (hst : ¬ (s = 1 ∧ t = 1)) (a v : Charge) :
    realGram (auxiliaryF B s a) (auxiliaryF B t v) =
      mixedMoment B (gramCharges a v)
        (gramLabels (Fin.castLE (by decide : 2 ≤ 6) s) (Fin.castLE (by decide : 2 ≤ 6) t)) := by
…

Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Charge, OAI.MUB6.realGram, OAI.MUB6.auxiliaryF, OAI.MUB6.mixedMoment, OAI.MUB6.gramCharges, OAI.MUB6.gramLabels

def OAI.MUB6.auxiliaryMixedEntry line 329
Source documentation
The exact mixed-moment expression for a pair of auxiliary functions.
```
def auxiliaryMixedEntry (B : Fin 7 → Basis) (s t : Fin 2) (a v : Charge) : ℝ :=
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.Charge
theorem OAI.MUB6.auxiliaryGram_eq line 336

theorem OAI.MUB6.auxiliaryGram_psd_nonneg line 349

Source documentation

Every real positive semidefinite quadratic form in the auxiliary functions is nonnegative; arbitrary finite real linear combinations are covered by realGram_weighted_sum.

theorem auxiliaryGram_psd_nonneg {ι : Type*} [Fintype ι] [DecidableEq ι]
    (B : Fin 7 → Basis) (tag : ι → Fin 2) (charge : ι → Charge)
    (Z : Matrix ι ι ℝ) (hZ : Z.PosSemidef) :
    0 ≤ ∑ i, ∑ j, Z i j * realGram (auxiliaryF B (tag i) (charge i))
      (auxiliaryF B (tag j) (charge j)) :=
…

Mentions: OAI.MUB6.Basis, OAI.MUB6.Charge, OAI.MUB6.realGram, OAI.MUB6.auxiliaryF