AngularHeckeCharacter.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

The finite factor at 3 required by a fixed angular Hecke character. The archimedean phase is retained separately, including after primitive conductor reduction. Complete ideal sums therefore include every prime at which the primitive character is unramified.

instance OAI.CubicFirstMoment.(instance at line 16) line 16
lemma OAI.CubicFirstMoment.theta_ne_zero line 18
lemma OAI.CubicFirstMoment.star_theta line 24
lemma OAI.CubicFirstMoment.ne_zero_of_three_unit line 29
def OAI.CubicFirstMoment.angularUnitCorrection line 37
Source documentation
On elements prime to 3 this is precisely the unit correction theta_l(primaryNormalize x) / theta_l(x). It vanishes at the ramified prime; it is a finite character, not an additional archimedean phase.
```
def angularUnitCorrection (ℓ : ℤ) (x : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.angularUnitCorrection_one line 41
lemma OAI.CubicFirstMoment.angularUnitCorrection_mul line 44
lemma OAI.CubicFirstMoment.angularUnitCorrection_primary line 54
lemma OAI.CubicFirstMoment.angularUnitCorrection_congr line 59
def OAI.CubicFirstMoment.angularCorrectionChar line 81
Source documentation
The correction is literally a multiplicative residue character modulo 3. Thus its conductor divides 3.
```
def angularCorrectionChar (ℓ : ℤ) : MulChar (Residues (3 : Eisenstein)) ℂ where
…
```
Mentions: OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.angularCorrectionChar_mk line 98
lemma OAI.CubicFirstMoment.angularUnitCorrection_compensates line 103
lemma OAI.CubicFirstMoment.angularCorrectionChar_unit line 109
def OAI.CubicFirstMoment.AngularUnitCompatible line 117
Source documentation
The correct unit condition for infinity type ell. For ell=0 it reduces to triviality on global units.
```
def AngularUnitCompatible (q : Eisenstein) (χ : MulChar (Residues q) ℂ) (ℓ : ℤ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues
lemma OAI.CubicFirstMoment.ResidueCharacterInduces.angular_units line 120
def OAI.CubicFirstMoment.angularResidueIdealChar line 129
Source documentation
Full primitive coefficients, before removing any Euler factor.
```
def angularResidueIdealChar (q : Eisenstein) (χ : MulChar (Residues q) ℂ)
    (ℓ : ℤ) (ν : EisensteinIdealExponent) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.angularResidueIdealChar_add line 133
lemma OAI.CubicFirstMoment.angularResidueIdealChar_norm_le_one line 140
lemma OAI.CubicFirstMoment.star_angularResidueIdealChar line 146
lemma OAI.CubicFirstMoment.angular_character_associated line 153
lemma OAI.CubicFirstMoment.angularResidueIdealChar_at_element line 166
lemma OAI.CubicFirstMoment.induced_angularResidueIdealChar line 173

theorem OAI.CubicFirstMoment.induced_angular_smooth_euler line 184

Source documentation

Primitive reduction preserves the angular factor and restores the actual omitted local Euler factors with their exact rescalings.

theorem induced_angular_smooth_euler {q d : Eisenstein} (hq : q ≠ 0)
    {χ : MulChar (Residues q) ℂ} {ψ : MulChar (Residues d) ℂ}
    (h : ResidueCharacterInduces q d χ ψ) (ℓ : ℤ) (W : ℝ → ℂ)
    (hW : HasCompactSupport W) {Z : ℝ} (hZ : 0 < Z) :
    (∑' ν, angularResidueIdealChar q χ ℓ ν*W (idealExponentNorm ν/Z)) =
      ∑ T ∈ (idealExponentOf q).support.powerset,
        (-1:ℂ)^T.card*angularResidueIdealChar d ψ ℓ (primeSetExponent T)*
          ∑' κ, angularResidueIdealChar d ψ ℓ κ*
            W (idealExponentNorm κ/(Z/idealExponentNorm (primeSetExponent T))) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.ResidueCharacterInduces, OAI.CubicFirstMoment.angularResidueIdealChar, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.primeSetExponent

def OAI.CubicFirstMoment.primaryAngularMixedLift line 201
lemma OAI.CubicFirstMoment.primaryAngularMixedLift_one line 204
lemma OAI.CubicFirstMoment.primaryAngularMixedLift_mul line 208
lemma OAI.CubicFirstMoment.primaryAngularMixedLift_congr line 215
def OAI.CubicFirstMoment.primaryAngularMixedChar line 228
Source documentation
The actual finite part of theta_l * mixedCubic a b, with the necessary unit compensation at 3. Its values on primary elements equal the mixed cubic symbol, but its values on units depend on ell.
```
def primaryAngularMixedChar (ℓ : ℤ) (a b : Eisenstein)
    (ha : primary a) (hb : primary b) : MulChar (Residues (3*(a*b))) ℂ where
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues
lemma OAI.CubicFirstMoment.primaryAngularMixedChar_mk line 248
lemma OAI.CubicFirstMoment.primaryAngularMixedChar_primary line 254
lemma OAI.CubicFirstMoment.primaryAngularMixedChar_compatible line 261
lemma OAI.CubicFirstMoment.primaryAngularMixedIdealChar_at_primary line 271
theorem OAI.CubicFirstMoment.primitive_angular_mixed_exists line 280
Source documentation
Primitive reduction is now applied to the actual compensated finite character. It preserves its infinity type and the conductor norm bound.
```
theorem primitive_angular_mixed_exists (ℓ : ℤ) {a b : Eisenstein}
    (ha : primary a) (hb : primary b) :
    ∃ (d : Eisenstein) (ψ : MulChar (Residues d) ℂ), d ≠ 0 ∧
      ResidueCharacterInduces (3*(a*b)) d (primaryAngularMixedChar ℓ a b ha hb) ψ ∧
      normNat d ≤ normNat (3*(a*b)) ∧ PrimitiveResidueCharacter d ψ ∧
      AngularUnitCompatible d ψ ℓ := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.ResidueCharacterInduces, OAI.CubicFirstMoment.primaryAngularMixedChar, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.PrimitiveResidueCharacter, OAI.CubicFirstMoment.AngularUnitCompatible