PrimeCharacterEvaluations.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

Actual prime-component character evaluations

The partial-evaluation homomorphism retains one cyclic coordinate and evaluates the others. Its multiplication and subsequent evaluation laws follow from its construction, rather than assumptions attached to the factors of a norm equation.

def OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedCharacter line 33
Source documentation
A character with values in the actual residual cyclic group algebra.
```
def weightedCharacter (f : ZMod n →+ ZMod m)
    (χ : Multiplicative (ZMod n) →* S) :
    Multiplicative (ZMod n) →* Elem S m where
…
```
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedCharacter_apply line 44
def OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedProjection line 51
Source documentation
Coefficients are mapped by φ, the coordinate f is kept as a variable, and all other character values become coefficients.
```
def weightedProjection (φ : R →+* S) (f : ZMod n →+ ZMod m)
    (χ : Multiplicative (ZMod n) →* S) : Elem R n →+* Elem S m :=
…
```
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedProjection_single line 55
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedProjection_scalar line 65
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.toMultiplicative_apply line 72

theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.evaluate_weightedProjection line 77

Source documentation

Subsequent evaluation is exactly the product of the evaluated coefficients and the character of the retained coordinate.

theorem evaluate_weightedProjection (φ : R →+* S) (ψ : S →+* T)
    (f : ZMod n →+ ZMod m) (χ : Multiplicative (ZMod n) →* S)
    (θ : Multiplicative (ZMod m) →* T) :
    (evaluate ψ θ).comp (weightedProjection φ f χ) =
      evaluate (ψ.comp φ)
        ((ψ.toMonoidHom.comp χ) * (θ.comp f.toMultiplicative)) := by
…

Mentions: OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedProjection

theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedProjection_product line 97
Source documentation
Norm preservation is a consequence of the constructed ring homomorphism. In particular it does not require the residual group algebra to be a domain.
```
theorem weightedProjection_product (φ : R →+* S) (f : ZMod n →+ ZMod m)
    (χ : Multiplicative (ZMod n) →* S) (x y : Elem R n) (r : R)
    (hxy : x * y = scalar n r) :
    weightedProjection φ f χ x * weightedProjection φ f χ y = scalar m (φ r) := by
…
```
Mentions: OAI.CirculantHadamard.PrimeCharacterEvaluations.weightedProjection
def OAI.CirculantHadamard.PrimeCharacterEvaluations.coordinate line 108
Source documentation
The actual CRT coordinate, without a chosen-decomposition hypothesis.
```
def coordinate (u : ℕ) (hu : 0 < u) (p : PrimeIndex u) :
    ZMod (u ^ 2) →+ Component u p where
…
```
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.coordinate_generator line 114
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.coordinate_generator_ne line 118
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.root_order_pow line 126
def OAI.CirculantHadamard.PrimeCharacterEvaluations.componentCharacter line 131
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.componentCharacter_apply line 136
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.componentCharacter_generator line 141
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.componentCharacter_generator_ne line 148

def OAI.CirculantHadamard.PrimeCharacterEvaluations.rootsCharacter line 155

Source documentation

A finite product of the actual primary-coordinate characters.

def rootsCharacter (u : ℕ) (hu : 0 < u) (r : PrimeIndex u → A)
    (hr : ∀ p, r p ^ p.val = 1) (S : Finset (PrimeIndex u)) :
    Multiplicative (ZMod (u ^ 2)) →* A :=
…

theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.rootsCharacter_apply line 160
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.rootsCharacter_empty line 166
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.rootsCharacter_generator line 170
def OAI.CirculantHadamard.PrimeCharacterEvaluations.rhoB line 189
Source documentation
The chosen primitive prime root in the literal global coefficient ring.
```
def rhoB (u : ℕ) (p : PrimeIndex u) : B u :=
…
```
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.coe_rhoB line 192
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.rhoB_pow line 195
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.rhoB_ne_one line 198
def OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetCharacter line 203
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetCharacter_empty line 207
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetCharacter_generator line 210
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetCharacter_nonempty line 215
def OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetEvaluation line 223
def OAI.CirculantHadamard.PrimeCharacterEvaluations.rhoAway line 228
Source documentation
The omitted root is replaced by one; all remaining roots lie in the actual away ring.
```
def rhoAway (u : ℕ) (p q : PrimeIndex u) : awayRing u p.val := by
…
```
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.rhoAway_pow line 234
def OAI.CirculantHadamard.PrimeCharacterEvaluations.awayCharacter line 241

def OAI.CirculantHadamard.PrimeCharacterEvaluations.partialEvaluation line 246

Source documentation

Leave precisely the full p-primary cyclic coordinate unevaluated.

def partialEvaluation (u : ℕ) (hu : 0 < u) (p : PrimeIndex u)
    (S : Finset (PrimeIndex u)) :
    Elem GaussianRing (u ^ 2) →+* Elem (awayRing u p.val) (order u p.val) :=
…

theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.partialEvaluation_product line 252
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.awayCharacter_map line 262
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetCharacter_insert line 282
def OAI.CirculantHadamard.PrimeCharacterEvaluations.partialAtOne line 298
Source documentation
Evaluate the remaining p-primary variable at one.
```
def partialAtOne (u : ℕ) (p : PrimeIndex u) :
    Elem (awayRing u p.val) (order u p.val) →+* B u :=
…
```
def OAI.CirculantHadamard.PrimeCharacterEvaluations.partialAtRoot line 303
Source documentation
Evaluate the remaining full p-primary variable at the selected pth root.
```
def partialAtRoot (u : ℕ) (hu : 0 < u) (p : PrimeIndex u) :
    Elem (awayRing u p.val) (order u p.val) →+* B u :=
…
```
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.gaussian_away_comp line 309
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.partialEvaluation_at_one line 318
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.partialEvaluation_at_root line 330
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.partialEvaluation_at_one_apply line 343
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.partialEvaluation_at_root_apply line 350
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.rhoB_mul_star line 357
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetCharacter_mul_star line 360
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetCharacter_neg line 370
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetEvaluation_star line 387
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetEvaluation_norm line 393
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetEvaluation_ne_zero line 401
theorem OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetEvaluation_map_norm line 412
Source documentation
Every complex embedding has the required norm. Compatibility with conjugation is derived from the actual adjoined roots in map_star_B.
```
theorem subsetEvaluation_map_norm (u : ℕ) [NeZero (u ^ 2)] (hu : 0 < u)
    (S : Finset (PrimeIndex u)) (x : Elem GaussianRing (u ^ 2))
    (hx : x * ringStar x = scalar (u ^ 2) ((u ^ 2 : ℕ) : GaussianRing))
    (σ : B u →+* ℂ) : ‖σ (subsetEvaluation u hu S x)‖ = (u : ℝ) := by
…
```
Mentions: OAI.CirculantHadamard.PrimeCharacterEvaluations.subsetEvaluation